diff --git a/jbmc/regression/jbmc/exception-cleanup/test.desc b/jbmc/regression/jbmc/exception-cleanup/test.desc index a3787221ff2..a3a271c9941 100644 --- a/jbmc/regression/jbmc/exception-cleanup/test.desc +++ b/jbmc/regression/jbmc/exception-cleanup/test.desc @@ -4,8 +4,11 @@ Test.class ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -0 remaining after simplification$ +1 remaining after simplification$ -- ^warning: ignoring -- -The function "unreachable" should be successfully noted as unreachable by symex. +The function "unreachable" should be successfully noted as unreachable by symex, +but the final uncaught-exception test in __CPROVER__start is not yet decidable +in symex, as it requires symex to note that within a catch block +@inflight_exception is definitely *not* null, which it can't just yet. diff --git a/jbmc/regression/jbmc/exception-cleanup/vccs.desc b/jbmc/regression/jbmc/exception-cleanup/vccs.desc index 83b698bdd53..4dd86b143ae 100644 --- a/jbmc/regression/jbmc/exception-cleanup/vccs.desc +++ b/jbmc/regression/jbmc/exception-cleanup/vccs.desc @@ -3,6 +3,8 @@ Test.class --function Test.main --show-vcc ^EXIT=0$ ^SIGNAL=0$ +file Test\.java line 6 function java::Test.main:\(I\)V +no uncaught exception -- file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5 assertion at file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5 diff --git a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c b/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c deleted file mode 100644 index 40219aa82f8..00000000000 --- a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c +++ /dev/null @@ -1,181 +0,0 @@ -#include - -static void noop() -{ -} - -int test(int nondet_int_array[]) -{ - int a = 1, b = 2, c = 3; - int *ptr_to_a = &a, *ptr_to_b = &b, *ptr_to_c = &c, *ptr_to_null = 0; - - // Symex knows the value of ptr_to_a, ptr_to_b, ptr_to_c and ptr_to_null, so - // it should be able to evaluate simple conditions involving them. - - // Equality "==" - - // A non-null pointer and a matching value - int unconditionally_reachable_1; - if(ptr_to_a == &a) - unconditionally_reachable_1 = 7; - - // A non-null pointer and a non-matching value (not a null pointer) - int unreachable_1; - if(ptr_to_a == &c) - unreachable_1 = 7; - - // A non-null pointer and a non-matching value (a null pointer) - int unreachable_2; - if(ptr_to_a == 0) - unreachable_2 = 7; - - // A null pointer and a matching value - int unconditionally_reachable_2; - if(ptr_to_null == 0) - unconditionally_reachable_2 = 7; - - // A null pointer and a non-matching value - int unreachable_3; - if(ptr_to_null == &a) - unreachable_3 = 7; - - // Disequality "!=" - - // A non-null pointer and a matching value - int unreachable_4; - if(ptr_to_a != &a) - unreachable_4 = 7; - - // A non-null pointer and a non-matching value (not a null pointer) - int unconditionally_reachable_3; - if(ptr_to_a != &c) - unconditionally_reachable_3 = 7; - - // A non-null pointer and a non-matching value (a null pointer) - int unconditionally_reachable_4; - if(ptr_to_a != 0) - unconditionally_reachable_4 = 7; - - // A null pointer and a matching value - int unreachable_5; - if(ptr_to_null != 0) - unreachable_5 = 7; - - // A null pointer and a non-matching value - int unconditionally_reachable_5; - if(ptr_to_null != &a) - unconditionally_reachable_5 = 7; - - // Symex can't tell what ptr_to_a_or_b points to, but we can tell that it - // doesn't point to some things - int *ptr_to_a_or_b = nondet_int_array[0] == 0 ? &a : &b; - int *ptr_to_a_or_b_or_null = - nondet_int_array[1] == 0 ? &a : nondet_int_array[1] == 1 ? &b : 0; - - // Equality "==" - - // A non-null pointer and a matching value - int possibly_reachable_1; - if(ptr_to_a_or_b == &a) - possibly_reachable_1 = 7; - - // A non-null pointer and a non-matching value (not a null pointer) - int unreachable_6; - if(ptr_to_a_or_b == &c) - unreachable_6 = 7; - - // A non-null pointer and a non-matching value (a null pointer) - int unreachable_7; - if(ptr_to_a_or_b == 0) - unreachable_7 = 7; - - // A possibly-null pointer and a matching value (not a null pointer) - int possibly_reachable_2; - if(ptr_to_a_or_b_or_null == &a) - possibly_reachable_2 = 7; - - // A possibly-null pointer and a matching value (a null pointer) - int possibly_reachable_3; - if(ptr_to_a_or_b_or_null == 0) - possibly_reachable_3 = 7; - - // A possibly-null pointer and a non-matching value - int unreachable_8; - if(ptr_to_a_or_b_or_null == &c) - unreachable_8 = 7; - - // Disequality "!=" - - // A non-null pointer and a matching value - int possibly_reachable_4; - if(ptr_to_a_or_b != &a) - possibly_reachable_4 = 7; - - // A non-null pointer and a non-matching value (not a null pointer) - int unconditionally_reachable_6; - if(ptr_to_a_or_b != &c) - unconditionally_reachable_6 = 7; - - // A non-null pointer and a non-matching value (a null pointer) - int unconditionally_reachable_7; - if(ptr_to_a_or_b != 0) - unconditionally_reachable_7 = 7; - - // A possibly-null pointer and a matching value (not a null pointer) - int possibly_reachable_5; - if(ptr_to_a_or_b_or_null != &a) - possibly_reachable_5 = 7; - - // A possibly-null pointer and a matching value (a null pointer) - int possibly_reachable_6; - if(ptr_to_a_or_b_or_null != 0) - possibly_reachable_6 = 7; - - // A possibly-null pointer and a non-matching value - int unconditionally_reachable_8; - if(ptr_to_a_or_b_or_null != &c) - unconditionally_reachable_8 = 7; - - // We should also be able to do all of the above in compound expressions which - // use logical operators like AND, OR and NOT, or even ternary expressions. - - int unconditionally_reachable_9; - if(!(ptr_to_a == &c) && ptr_to_a_or_b != 0) - unconditionally_reachable_9 = 7; - - int unreachable_9; - if(!(ptr_to_null == 0) || ptr_to_a_or_b == 0) - unreachable_9 = 7; - - int unconditionally_reachable_10; - if((ptr_to_a == &a && !(ptr_to_a_or_b == 0)) || ptr_to_a_or_b_or_null == &c) - unconditionally_reachable_10 = 7; - - int unreachable_10; - if(ptr_to_a_or_b_or_null != 0 ? ptr_to_null != 0 : ptr_to_a_or_b == &c) - unreachable_10 = 7; - - // And everything should work with the symbol on the left or the right - - int unconditionally_reachable_11; - if(!(&c == ptr_to_a) && 0 != ptr_to_a_or_b) - unconditionally_reachable_11 = 7; - - int unreachable_11; - if(!(0 == ptr_to_null) || 0 == ptr_to_a_or_b) - unreachable_11 = 7; - - int unconditionally_reachable_12; - if((&a == ptr_to_a && !(0 == ptr_to_a_or_b)) || &c == ptr_to_a_or_b_or_null) - unconditionally_reachable_12 = 7; - - int unreachable_12; - if(0 != ptr_to_a_or_b_or_null ? 0 != ptr_to_null : &c == ptr_to_a_or_b) - unreachable_12 = 7; - - int possibly_reachable_7; - if(0 != ptr_to_a_or_b_or_null) - possibly_reachable_7 = 7; - - assert(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 deleted file mode 100644 index d8f0a0e31c7..00000000000 --- a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc +++ /dev/null @@ -1,60 +0,0 @@ -CORE paths-lifo-expected-failure -test.c ---function test --show-vcc -^EXIT=0$ -^SIGNAL=0$ -test::1::unconditionally_reachable_1[^\s]+ = 7$ -test::1::unconditionally_reachable_2[^\s]+ = 7$ -test::1::unconditionally_reachable_3[^\s]+ = 7$ -test::1::unconditionally_reachable_4[^\s]+ = 7$ -test::1::unconditionally_reachable_5[^\s]+ = 7$ -test::1::unconditionally_reachable_6[^\s]+ = 7$ -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::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::unreachable_1[^\s]+ = 7$ -test::1::unreachable_2[^\s]+ = 7$ -test::1::unreachable_3[^\s]+ = 7$ -test::1::unreachable_4[^\s]+ = 7$ -test::1::unreachable_5[^\s]+ = 7$ -test::1::unreachable_6[^\s]+ = 7$ -test::1::unreachable_7[^\s]+ = 7$ -test::1::unreachable_8[^\s]+ = 7$ -test::1::unreachable_9[^\s]+ = 7$ -test::1::unreachable_10[^\s]+ = 7$ -test::1::unreachable_11[^\s]+ = 7$ -test::1::unreachable_12[^\s]+ = 7$ -^warning: ignoring -unreachable_1[3-9] -unreachable[2-9][0-9] -unconditionally_reachable_1[3-9] -unconditionally_reachable[2-9][0-9] -possibly_reachable_[8-9] -possibly_reachable_[1-9][0-9] --- -Pointer comparisons will be resolved in symex by a mixture of constant -propagation and value-set filtering in try_evaluate_pointer_comparisons. - -The expected failure for path-symex is because the lines we check for -possibly_reachable_* would only appear when there is convergence behaviour. diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h index 5c9af1c513c..8096ca37cf0 100644 --- a/src/goto-symex/renaming_level.h +++ b/src/goto-symex/renaming_level.h @@ -15,9 +15,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include -#include #include -#include #include #include #include @@ -89,9 +87,6 @@ class renamedt : private underlyingt (void)::simplify(value(), ns); } - using mutator_functiont = - std::function(const renamedt &)>; - private: underlyingt &value() { @@ -103,51 +98,12 @@ class renamedt : private underlyingt friend struct symex_level2t; friend class goto_symex_statet; - template - friend renamedt - make_renamed(constant_exprt constant); - - template - friend void selectively_mutate( - renamedt &renamed, - typename renamedt::mutator_functiont - get_mutated_expr); - /// Only the friend classes can create renamedt objects explicit renamedt(underlyingt value) : underlyingt(std::move(value)) { } }; -template -renamedt make_renamed(constant_exprt constant) -{ - return renamedt(std::move(constant)); -} - -/// This permits replacing subexpressions of the renamed value, so long as -/// each replacement is consistent with our current renaming level (for -/// example, replacing subexpressions of L2 expressions with ones which are -/// themselves L2 renamed). -/// The passed function will be called with each expression node in preorder -/// (i.e. parent expressions before children), and should return an empty -/// optional to make no change or a renamed expression to make a change. -template -void selectively_mutate( - renamedt &renamed, - typename renamedt::mutator_functiont get_mutated_expr) -{ - for(auto it = renamed.depth_begin(), itend = renamed.depth_end(); it != itend; - ++it) - { - optionalt> replacement = - get_mutated_expr(static_cast &>(*it)); - - if(replacement) - it.mutate() = std::move(replacement->value()); - } -} - /// Functor to set the level 0 renaming of SSA expressions. /// Level 0 corresponds to threads. /// The renaming is built for one particular interleaving. diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 30f19f0adf0..0fdfcbbe938 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com /// Symbolic Execution #include "goto_symex.h" -#include "goto_symex_is_constant.h" #include @@ -20,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include void goto_symext::apply_goto_condition( @@ -67,161 +65,6 @@ void goto_symext::apply_goto_condition( } } -/// Try to evaluate a simple pointer comparison. -/// \param operation: ID_equal or ID_not_equal -/// \param symbol_expr: The symbol expression in the condition -/// \param other_operand: The other expression in the condition - must pass -/// goto_symex_is_constant, and since it is pointer-typed it must therefore -/// be an address of expression, a typecast of an address of expression or a -/// null pointer -/// \param value_set: The value-set for looking up what the symbol can point to -/// \param language_mode: The language mode -/// \param ns: A namespace -/// \return If we were able to evaluate the condition as true or false then we -/// return that, otherwise we return an empty optionalt -static optionalt> try_evaluate_pointer_comparison( - const irep_idt &operation, - const symbol_exprt &symbol_expr, - const exprt &other_operand, - const value_sett &value_set, - const irep_idt language_mode, - const namespacet &ns) -{ - const constant_exprt *constant_expr = - expr_try_dynamic_cast(other_operand); - - INVARIANT( - skip_typecast(other_operand).id() == ID_address_of || - (constant_expr && constant_expr->get_value() == ID_NULL), - "An expression that passes goto_symex_is_constant and has " - "pointer-type must be an address of expression (possibly with some " - "typecasts) or a null pointer"); - - const ssa_exprt *ssa_symbol_expr = - expr_try_dynamic_cast(symbol_expr); - - value_setst::valuest value_set_elements; - value_set.get_value_set( - ssa_symbol_expr->get_l1_object(), value_set_elements, ns); - - bool constant_found = false; - - for(const auto &value_set_element : value_set_elements) - { - if( - value_set_element.id() == ID_unknown || - value_set_element.id() == ID_invalid) - { - // If ID_unknown or ID_invalid are in the value-set then we can't - // conclude anything about it - return {}; - } - - if(!constant_found) - { - if(value_set_dereferencet::should_ignore_value( - value_set_element, false, language_mode)) - { - continue; - } - - value_set_dereferencet::valuet value = - value_set_dereferencet::build_reference_to( - value_set_element, symbol_expr, ns); - - if(value.pointer == other_operand) - { - constant_found = true; - // We can't break because we have to make sure we find any instances of - // ID_unknown or ID_invalid - } - } - } - - if(!constant_found) - { - // The symbol cannot possibly have the value \p other_operand because it - // isn't in the symbol's value-set - return operation == ID_equal ? make_renamed(false_exprt{}) - : make_renamed(true_exprt{}); - } - else if(value_set_elements.size() == 1) - { - // The symbol must have the value \p other_operand because it is the only - // thing in the symbol's value-set - return operation == ID_equal ? make_renamed(true_exprt{}) - : make_renamed(false_exprt{}); - } - else - { - return {}; - } -} - -/// Check if we have a simple pointer comparison, and if so try to evaluate it. -/// \param renamed_expr: The L2-renamed expression to check -/// \param value_set: The value-set for looking up what the symbol can point to -/// \param language_mode: The language mode -/// \param ns: A namespace -/// \return If we were able to evaluate the condition as true or false then we -/// return that, otherwise we return an empty optionalt -static optionalt> try_evaluate_pointer_comparison( - const renamedt &renamed_expr, - const value_sett &value_set, - const irep_idt &language_mode, - const namespacet &ns) -{ - const exprt &expr = renamed_expr.get(); - - if(expr.id() != ID_equal && expr.id() != ID_notequal) - return {}; - - if(!can_cast_type(expr.op0().type())) - return {}; - - exprt lhs = expr.op0(), rhs = expr.op1(); - if(can_cast_expr(rhs)) - std::swap(lhs, rhs); - - const symbol_exprt *symbol_expr_lhs = - expr_try_dynamic_cast(lhs); - - if(!symbol_expr_lhs) - return {}; - - if(!goto_symex_is_constantt()(rhs)) - return {}; - - return try_evaluate_pointer_comparison( - expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns); -} - -/// Try to evaluate pointer comparisons where they can be trivially determined -/// using the value-set. This is optional as all it does is allow symex to -/// resolve some comparisons itself and therefore create a simpler formula for -/// the SAT solver. -/// \param [in,out] condition: An L2-renamed expression with boolean type -/// \param value_set: The value-set for determining what pointer-typed symbols -/// might possibly point to -/// \param language_mode: The language mode -/// \param ns: A namespace -/// \return The possibly modified condition -static renamedt try_evaluate_pointer_comparisons( - renamedt condition, - const value_sett &value_set, - const irep_idt &language_mode, - const namespacet &ns) -{ - selectively_mutate( - condition, - [&value_set, &language_mode, &ns](const renamedt &expr) { - return try_evaluate_pointer_comparison( - expr, value_set, language_mode, ns); - }); - - return condition; -} - void goto_symext::symex_goto(statet &state) { const goto_programt::instructiont &instruction=*state.source.pc; @@ -230,8 +73,6 @@ void goto_symext::symex_goto(statet &state) clean_expr(new_guard, state, false); renamedt renamed_guard = state.rename(std::move(new_guard), ns); - renamed_guard = try_evaluate_pointer_comparisons( - std::move(renamed_guard), state.value_set, language_mode, ns); if(symex_config.simplify_opt) renamed_guard.simplify(ns); new_guard = renamed_guard.get(); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index ac4270a6634..b9bf3b4d32e 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -721,11 +721,9 @@ void goto_symext::try_filter_value_sets( // one of its possible values in turn. If that leads to a true for some // value_set_element then we can delete it from the value set that will be // used if the condition is false, and vice versa. - for(const exprt &value_set_element : value_set_elements) + for(const auto &value_set_element : value_set_elements) { - if( - value_set_element.id() == ID_unknown || - value_set_element.id() == ID_invalid) + if(value_set_element.id() == ID_unknown) { continue; } @@ -737,17 +735,19 @@ void goto_symext::try_filter_value_sets( continue; } - value_set_dereferencet::valuet value = + value_set_dereferencet::valuet possible_value = value_set_dereferencet::build_reference_to( value_set_element, *symbol_expr, ns); - if(value.pointer.is_nil()) - continue; + exprt replacement_expr = + possible_value.value.is_nil() + ? static_cast(null_pointer_exprt{symbol_type}) + : static_cast(address_of_exprt{possible_value.value}); exprt modified_condition(condition); address_of_aware_replace_symbolt replace_symbol{}; - replace_symbol.insert(*symbol_expr, value.pointer); + replace_symbol.insert(*symbol_expr, replacement_expr); replace_symbol(modified_condition); // This do_simplify() is needed for the following reason: if `condition` is diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 9d9c7d5efe4..66186c8d134 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -23,7 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -362,9 +361,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( const exprt &pointer_expr, const namespacet &ns) { - const pointer_typet &pointer_type = - type_checked_cast(pointer_expr.type()); - const typet &dereference_type = pointer_type.subtype(); + const typet &dereference_type = pointer_expr.type().subtype(); if(what.id()==ID_unknown || what.id()==ID_invalid) @@ -388,7 +385,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( if(root_object.id() == ID_null_object) { - result.pointer = null_pointer_exprt{pointer_type}; } else if(root_object.id()==ID_dynamic_object) { @@ -398,7 +394,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // can't remove here, turn into *p result.value = dereference_exprt{pointer_expr}; - result.pointer = pointer_expr; } else if(root_object.id()==ID_integer_address) { @@ -419,7 +414,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( memory_symbol.type.subtype()); result.value=index_expr; - result.pointer = address_of_exprt{index_expr}; } else if( dereference_type_compare( @@ -430,8 +424,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( pointer_offset(pointer_expr), memory_symbol.type.subtype()); result.value=typecast_exprt(index_expr, dereference_type); - result.pointer = - typecast_exprt{address_of_exprt{index_expr}, pointer_type}; } else { @@ -448,7 +440,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( symbol_expr, pointer_offset(pointer_expr), dereference_type); - result.pointer = address_of_exprt{result.value}; } } } @@ -481,8 +472,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // This is great, we are almost done. result.value = typecast_exprt::conditional_cast(object, dereference_type); - result.pointer = - typecast_exprt::conditional_cast(object_pointer, pointer_type); } else if( root_object_type.id() == ID_array && @@ -526,12 +515,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // TODO: need to assert well-alignedness } - const index_exprt &index_expr = - index_exprt(root_object, adjusted_offset, root_object_type.subtype()); - result.value = - typecast_exprt::conditional_cast(index_expr, dereference_type); - result.pointer = typecast_exprt::conditional_cast( - address_of_exprt{index_expr}, pointer_type); + result.value = typecast_exprt::conditional_cast( + index_exprt(root_object, adjusted_offset, root_object_type.subtype()), + dereference_type); } else { @@ -545,15 +531,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // Successfully found a member, array index, or combination thereof // that matches the desired type and offset: result.value = subexpr.value(); - result.pointer = typecast_exprt::conditional_cast( - address_of_exprt{skip_typecast(subexpr.value())}, pointer_type); return result; } // we extract something from the root object result.value=o.root_object(); - result.pointer = typecast_exprt::conditional_cast( - address_of_exprt{skip_typecast(o.root_object())}, pointer_type); // this is relative to the root object exprt offset; diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index 4889a7cb362..d1488be443b 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/src/pointer-analysis/value_set_dereference.h @@ -59,11 +59,9 @@ class value_set_dereferencet final { public: exprt value; - exprt pointer; exprt pointer_guard; - valuet() - : value{nil_exprt{}}, pointer{nil_exprt{}}, pointer_guard{false_exprt{}} + valuet() : value(nil_exprt()), pointer_guard(false_exprt()) { } };