diff --git a/regression/cbmc/empty_compound_type1/main.c b/regression/cbmc/empty_compound_type1/main.c new file mode 100644 index 00000000000..ba4d3c0f0cc --- /dev/null +++ b/regression/cbmc/empty_compound_type1/main.c @@ -0,0 +1,19 @@ +union a { +}; +struct +{ + union a; +} b; +struct c +{ + int cli; +}; +void e(struct c *f) +{ + int a = f->cli; +} +main() +{ + // pass a pointer to an incompatible type + e(&b); +} diff --git a/regression/cbmc/empty_compound_type1/test.desc b/regression/cbmc/empty_compound_type1/test.desc new file mode 100644 index 00000000000..f43a3475b59 --- /dev/null +++ b/regression/cbmc/empty_compound_type1/test.desc @@ -0,0 +1,14 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +First observed on SV-COMP's +linux-4.2-rc1.tar.xz-32_7a-drivers--staging--lustre--lustre--mdc--mdc.ko-entry_point.cil.out.i: +accessing an empty union (or struct) in pointer dereferencing involving +incompatible pointers resulted in a segmentation fault. This test was generated +using C-Reduce plus some further manual simplification. diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index b47d5e22ffa..58ebd889a9f 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -425,14 +425,17 @@ optionalt value_sett::get_index_of_symbol( const struct_union_typet &struct_union_type = to_struct_union_type(followed_type); - const irep_idt &first_component_name = - struct_union_type.components().front().get_name(); - - index = - id2string(identifier) + "." + id2string(first_component_name) + suffix; - entry = find_entry(index); - if(entry) - return std::move(index); + if(!struct_union_type.components().empty()) + { + const irep_idt &first_component_name = + struct_union_type.components().front().get_name(); + + index = + id2string(identifier) + "." + id2string(first_component_name) + suffix; + entry = find_entry(index); + if(entry) + return std::move(index); + } } // not found? try without suffix