diff --git a/regression/cbmc-cover/pointer-function-parameters/test.desc b/regression/cbmc-cover/pointer-function-parameters/test.desc index 3f159e8234b5..d945ab4bb7cc 100644 --- a/regression/cbmc-cover/pointer-function-parameters/test.desc +++ b/regression/cbmc-cover/pointer-function-parameters/test.desc @@ -5,7 +5,7 @@ main.c ^Test suite:$ ^(tmp(\$\d+)?=[^,]*, a=\(\(signed int \*\)NULL\))|(a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*)$ ^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0@1)$ -^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0@1)$ +^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=(-?[012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=(-?[012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0@1)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc b/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc index 6711345bfd4a..2e95545bd08c 100644 --- a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc +++ b/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc @@ -13,26 +13,26 @@ test::1::unconditionally_reachable_7[^\s]+ = 7$ test::1::unconditionally_reachable_8[^\s]+ = 7$ test::1::unconditionally_reachable_9[^\s]+ = 7$ test::1::unconditionally_reachable_10[^\s]+ = 7$ -test::1::possibly_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_1[^\s]+\)$ -test::1::possibly_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_2[^\s]+\)$ -test::1::possibly_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_3[^\s]+\)$ -test::1::possibly_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_4[^\s]+\)$ -test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_5[^\s]+\)$ -test::1::possibly_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_6[^\s]+\)$ -test::1::possibly_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_7[^\s]+\)$ +test::1::possibly_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_1[^\s]+ : 7\)$ +test::1::possibly_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_2[^\s]+ : 7\)$ +test::1::possibly_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_3[^\s]+ : 7\)$ +test::1::possibly_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_4[^\s]+ : 7\)$ +test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_5[^\s]+ : 7\)$ +test::1::possibly_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_6[^\s]+ : 7\)$ +test::1::possibly_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_7[^\s]+ : 7\)$ -- -test::1::unconditionally_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_1[^\s]+\)$ -test::1::unconditionally_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_2[^\s]+\)$ -test::1::unconditionally_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_3[^\s]+\)$ -test::1::unconditionally_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_4[^\s]+\)$ -test::1::unconditionally_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_5[^\s]+\)$ -test::1::unconditionally_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_6[^\s]+\)$ -test::1::unconditionally_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_7[^\s]+\)$ -test::1::unconditionally_reachable_8[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_8[^\s]+\)$ -test::1::unconditionally_reachable_9[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_9[^\s]+\)$ -test::1::unconditionally_reachable_10[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_10[^\s]+\)$ -test::1::unconditionally_reachable_11[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_11[^\s]+\)$ -test::1::unconditionally_reachable_12[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_12[^\s]+\)$ +test::1::unconditionally_reachable_1[^\s]+ = .+ \? +test::1::unconditionally_reachable_2[^\s]+ = .+ \? +test::1::unconditionally_reachable_3[^\s]+ = .+ \? +test::1::unconditionally_reachable_4[^\s]+ = .+ \? +test::1::unconditionally_reachable_5[^\s]+ = .+ \? +test::1::unconditionally_reachable_6[^\s]+ = .+ \? +test::1::unconditionally_reachable_7[^\s]+ = .+ \? +test::1::unconditionally_reachable_8[^\s]+ = .+ \? +test::1::unconditionally_reachable_9[^\s]+ = .+ \? +test::1::unconditionally_reachable_10[^\s]+ = .+ \? +test::1::unconditionally_reachable_11[^\s]+ = .+ \? +test::1::unconditionally_reachable_12[^\s]+ = .+ \? test::1::unreachable_1[^\s]+ = 7$ test::1::unreachable_2[^\s]+ = 7$ test::1::unreachable_3[^\s]+ = 7$ diff --git a/regression/cbmc/unreachable-goto2/test-vccs.desc b/regression/cbmc/unreachable-goto2/test-vccs.desc index d18e596fd5f9..441a0303e488 100644 --- a/regression/cbmc/unreachable-goto2/test-vccs.desc +++ b/regression/cbmc/unreachable-goto2/test-vccs.desc @@ -2,7 +2,7 @@ CORE paths-lifo-expected-failure test.c --show-vcc ^Generated 1 VCC\(s\), 1 remaining after simplification$ -^\{1\} goto_symex::\\guard#1$ +^\{1\} ¬goto_symex::\\guard#1$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index b0f82868f6e4..b9214bf9eca3 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -490,12 +490,11 @@ void goto_symext::symex_goto(statet &state) { symbol_exprt guard_symbol_expr = symbol_exprt(statet::guard_identifier(), bool_typet()); - exprt new_rhs = boolean_negate(new_guard); ssa_exprt new_lhs = state.rename_ssa(ssa_exprt{guard_symbol_expr}, ns).get(); new_lhs = - state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get(); + state.assignment(std::move(new_lhs), new_guard, ns, true, false).get(); guardt guard{true_exprt{}, guard_manager}; @@ -509,12 +508,14 @@ void goto_symext::symex_goto(statet &state) target.assignment( guard.as_expr(), - new_lhs, new_lhs, guard_symbol_expr, - new_rhs, + new_lhs, + new_lhs, + guard_symbol_expr, + new_guard, original_source, symex_targett::assignment_typet::GUARD); - guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get(); + guard_expr = state.rename(guard_symbol_expr, ns).get(); } if(state.has_saved_jump_target)