diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp index 8a97ef48fd0..072e20b8efe 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp @@ -110,8 +110,8 @@ void dfcc_contract_clauses_codegent::encode_assignable_target_group( new_vars = cleaner.clean(condition, dest, language_mode); // Jump target if condition is false - auto goto_instruction = dest.add( - goto_programt::make_incomplete_goto(not_exprt{condition}, source_location)); + auto goto_instruction = dest.add(goto_programt::make_incomplete_goto( + boolean_negate(condition), source_location)); for(const auto &target : group.targets()) encode_assignable_target(language_mode, target, dest); @@ -199,8 +199,8 @@ void dfcc_contract_clauses_codegent::encode_freeable_target_group( new_vars = cleaner.clean(condition, dest, language_mode); // Jump target if condition is false - auto goto_instruction = dest.add( - goto_programt::make_incomplete_goto(not_exprt{condition}, source_location)); + auto goto_instruction = dest.add(goto_programt::make_incomplete_goto( + boolean_negate(condition), source_location)); for(const auto &target : group.targets()) encode_freeable_target(language_mode, target, dest); diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp index 346fbe6e78f..b820ce321f1 100644 --- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp @@ -68,7 +68,7 @@ void havoc_assigns_clause_targetst::havoc_if_valid( skip_program.add(goto_programt::make_skip(source_location_no_checks)); dest.add(goto_programt::make_goto( - skip_target, not_exprt{car.valid_var()}, source_location_no_checks)); + skip_target, boolean_negate(car.valid_var()), source_location_no_checks)); if(car.havoc_method == car_havoc_methodt::HAVOC_OBJECT) { @@ -142,7 +142,7 @@ void havoc_assigns_clause_targetst::havoc_static_local( skip_program.add(goto_programt::make_skip(source_location_no_checks)); dest.add(goto_programt::make_goto( - skip_target, not_exprt{car.valid_var()}, source_location_no_checks)); + skip_target, boolean_negate(car.valid_var()), source_location_no_checks)); const auto &target_type = car.target().type(); side_effect_expr_nondett nondet(target_type, source_location); diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index fc273e46259..b620714c78e 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -656,9 +656,9 @@ exprt instrument_spec_assignst::target_validity_expr( // (or is NULL if we allow it explicitly). // This assertion will be falsified whenever `start_address` is invalid or // not of the right size (or is NULL if we do not allow it explicitly). - auto result = - or_exprt{not_exprt{car.condition()}, - w_ok_exprt{car.target_start_address(), car.target_size()}}; + auto result = or_exprt{ + boolean_negate(car.condition()), + w_ok_exprt{car.target_start_address(), car.target_size()}}; if(allow_null_target) result.add_to_operands(null_object(car.target_start_address())); diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index a33319509b2..79e48791ec2 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -41,7 +41,9 @@ static void append_safe_havoc_code_for_expr( // skip havocing only if all pointer derefs in the expression are valid // (to avoid spurious pointer deref errors) dest.add(goto_programt::make_goto( - skip_target, not_exprt{all_dereferences_are_valid(expr, ns)}, location)); + skip_target, + boolean_negate(all_dereferences_are_valid(expr, ns)), + location)); havoc_code_impl(); @@ -433,8 +435,8 @@ static void replace_history_parameter_rec( // 2.2. Skip storing the history if the expression is invalid auto goto_instruction = history.add(goto_programt::make_incomplete_goto( - not_exprt{ - all_dereferences_are_valid(parameter, namespacet(symbol_table))}, + boolean_negate( + all_dereferences_are_valid(parameter, namespacet(symbol_table))), location)); // 2.3. Add an assignment such that the value pointed to by the new diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp index fb8e382f437..8cbe0038a13 100644 --- a/src/goto-symex/goto_state.cpp +++ b/src/goto-symex/goto_state.cpp @@ -145,11 +145,7 @@ void goto_statet::apply_condition( if(!is_ssa_expr(lhs) || !goto_symex_can_forward_propagatet(ns)(rhs)) return; - if(rhs.is_true()) - apply_condition(equal_exprt{lhs, false_exprt{}}, previous_state, ns); - else if(rhs.is_false()) - apply_condition(equal_exprt{lhs, true_exprt{}}, previous_state, ns); - else - UNREACHABLE; + PRECONDITION(rhs.is_constant()); + apply_condition(equal_exprt{lhs, boolean_negate(rhs)}, previous_state, ns); } } diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 4e8d8523d68..8dcd92c6078 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -279,7 +279,7 @@ void goto_symext::symex_goto(statet &state) { // generate assume(false) or a suitable negation if this // instruction is a conditional goto - exprt negated_guard = not_exprt{new_guard}; + exprt negated_guard = boolean_negate(new_guard); do_simplify(negated_guard); log.statistics() << "replacing self-loop at " << state.source.pc->source_location() << " by assume(" @@ -929,12 +929,7 @@ void goto_symext::loop_bound_exceeded( { const std::string loop_number = std::to_string(state.source.pc->loop_number); - exprt negated_cond; - - if(guard.is_true()) - negated_cond=false_exprt(); - else - negated_cond=not_exprt(guard); + exprt negated_cond = boolean_negate(guard); if(symex_config.unwinding_assertions) {