diff --git a/regression/cbmc/Linking7/member-name-mismatch.desc b/regression/cbmc/Linking7/member-name-mismatch.desc index ff30eee14c6..603d759e8d8 100644 --- a/regression/cbmc/Linking7/member-name-mismatch.desc +++ b/regression/cbmc/Linking7/member-name-mismatch.desc @@ -1,11 +1,11 @@ -KNOWNBUG +CORE main.c module2.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ +line 21 assertion \*g\.a == 42: SUCCESS +line 22 assertion \*g\.c == 41: FAILURE ^\*\* 1 of 2 failed -- ^warning: ignoring --- -This is either a bug in goto-symex or value_sett (where the invariant fails). diff --git a/regression/cbmc/Linking7/test.desc b/regression/cbmc/Linking7/test.desc index 4eaef880405..7e8989049b8 100644 --- a/regression/cbmc/Linking7/test.desc +++ b/regression/cbmc/Linking7/test.desc @@ -5,5 +5,7 @@ module.c ^SIGNAL=0$ ^VERIFICATION FAILED$ ^\*\* 1 of 2 failed +line 21 assertion \*g\.a == 42: SUCCESS +line 22 assertion \*g\.b == 41: FAILURE -- ^warning: ignoring diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests index f20aa252c73..1051bdc108d 100755 --- a/scripts/delete_failing_smt2_solver_tests +++ b/scripts/delete_failing_smt2_solver_tests @@ -36,6 +36,7 @@ rm Float6/test.desc rm Float8/test.desc rm Linking4/test.desc rm Linking7/test.desc +rm Linking7/member-name-mismatch.desc rm Malloc19/test.desc rm Malloc23/test.desc rm Malloc24/test.desc diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index f8ba7a82ce3..bfad48312d8 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1630,37 +1630,10 @@ exprt value_sett::make_member( const struct_union_typet &struct_union_type= to_struct_union_type(ns.follow(src.type())); - if(src.id()==ID_struct || - src.id()==ID_constant) - { - std::size_t no=struct_union_type.component_number(component_name); - assert(no