File tree Expand file tree Collapse file tree 3 files changed +44
-8
lines changed
regression/cbmc/empty_compound_type1 Expand file tree Collapse file tree 3 files changed +44
-8
lines changed Original file line number Diff line number Diff line change 1+ union a {
2+ };
3+ struct
4+ {
5+ union a ;
6+ } b ;
7+ struct c
8+ {
9+ int cli ;
10+ };
11+ void e (struct c * f )
12+ {
13+ int a = f -> cli ;
14+ }
15+ main ()
16+ {
17+ // pass a pointer to an incompatible type
18+ e (& b );
19+ }
Original file line number Diff line number Diff line change 1+ CORE
2+ main.c
3+
4+ ^EXIT=0$
5+ ^SIGNAL=0$
6+ ^VERIFICATION SUCCESSFUL$
7+ --
8+ ^warning: ignoring
9+ --
10+ First observed on SV-COMP's
11+ linux-4.2-rc1.tar.xz-32_7a-drivers--staging--lustre--lustre--mdc--mdc.ko-entry_point.cil.out.i:
12+ accessing an empty union (or struct) in pointer dereferencing involving
13+ incompatible pointers resulted in a segmentation fault. This test was generated
14+ using C-Reduce plus some further manual simplification.
Original file line number Diff line number Diff line change @@ -425,14 +425,17 @@ optionalt<irep_idt> value_sett::get_index_of_symbol(
425425 const struct_union_typet &struct_union_type =
426426 to_struct_union_type (followed_type);
427427
428- const irep_idt &first_component_name =
429- struct_union_type.components ().front ().get_name ();
430-
431- index =
432- id2string (identifier) + " ." + id2string (first_component_name) + suffix;
433- entry = find_entry (index);
434- if (entry)
435- return std::move (index);
428+ if (!struct_union_type.components ().empty ())
429+ {
430+ const irep_idt &first_component_name =
431+ struct_union_type.components ().front ().get_name ();
432+
433+ index =
434+ id2string (identifier) + " ." + id2string (first_component_name) + suffix;
435+ entry = find_entry (index);
436+ if (entry)
437+ return std::move (index);
438+ }
436439 }
437440
438441 // not found? try without suffix
You can’t perform that action at this time.
0 commit comments