diff --git a/lib/cbmc b/lib/cbmc index 1ecfc4889..ddf6447b6 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit 1ecfc4889b92942e8fb7158b105efd5aede0f363 +Subproject commit ddf6447b6e1e14e3ed9a564682d174d1a9aa5926 diff --git a/regression/kiki/hard2_unwindbound5/main.c b/regression/kiki/hard2_unwindbound5/main.c new file mode 100644 index 000000000..00b3177e7 --- /dev/null +++ b/regression/kiki/hard2_unwindbound5/main.c @@ -0,0 +1,61 @@ +/* + hardware integer division program, by Manna + returns q==A//B + */ + +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); +void reach_error() { __assert_fail("0", "hard2.c", 8, "reach_error"); } +extern int __VERIFIER_nondet_int(void); +extern void abort(void); +void assume_abort_if_not(int cond) { + if(!cond) {abort();} +} +void __VERIFIER_assert(int cond) { + if (!(cond)) { + ERROR: + {reach_error();} + } + return; +} + +int counter = 0; +int main() { + int A, B; + int r, d, p, q; + A = __VERIFIER_nondet_int(); + B = 1; + + r = A; + d = B; + p = 1; + q = 0; + + while (counter++<5) { + __VERIFIER_assert(q == 0); + __VERIFIER_assert(r == A); + __VERIFIER_assert(d == B * p); + if (!(r >= d)) break; + + d = 2 * d; + p = 2 * p; + } + + while (counter++<5) { + __VERIFIER_assert(A == q*B + r); + __VERIFIER_assert(d == B*p); + + if (!(p != 1)) break; + + d = d / 2; + p = p / 2; + if (r >= d) { + r = r - d; + q = q + p; + } + } + + __VERIFIER_assert(A == d*q + r); + __VERIFIER_assert(B == d); + return 0; +} diff --git a/regression/kiki/hard2_unwindbound5/test.desc b/regression/kiki/hard2_unwindbound5/test.desc new file mode 100644 index 000000000..de523f99a --- /dev/null +++ b/regression/kiki/hard2_unwindbound5/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--heap --values-refine --k-induction --competition-mode +^EXIT=10$ +^SIGNAL=0$ +^.*FAILURE$ +-- +-- +This is a past incorrect true benchmark from SV-comp which was caused by a bug +in SSA unwinder where the generated constraints made the analysis unsound. diff --git a/regression/memsafety/built_from_end/test.desc b/regression/memsafety/built_from_end/test.desc index c9a5cf964..a9c706a24 100644 --- a/regression/memsafety/built_from_end/test.desc +++ b/regression/memsafety/built_from_end/test.desc @@ -1,35 +1,6 @@ -KNOWNBUG +CORE main.c --heap --intervals --pointer-check --no-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ --- --- -CBMC 5.9 introduced changes to its implementation of some built-in functions, -the ones affecting this test are malloc and free. Malloc changes have been -already accounted for in 2LS codebase, however the control flow of free -is most likely causing problems in this test making one of the asserts fail: - -[main.pointer_dereference.27] dereference failure: deallocated dynamic object in *p: UNKNOWN - -This may be related to double free assertion, where GOTO changed from: - -... - IF !(__CPROVER_deallocated == ptr) THEN GOTO 6 - // 144 file line 18 function free - ASSERT 0 != 0 // double free - // 145 no location - ASSUME 0 != 0 - // 146 file line 29 function free - 6: _Bool record; -... - -to: - ASSERT ptr == NULL || __CPROVER_deallocated != ptr // double free - -Note the new ptr == NULL condition, this could be the root cause of -the problem. However further investigation is required -and will be done once the CBMC rebase is completed. According to the -C standard, free(NULL) is a valid construct (no operation) but 2LS doesn't -seem to handle this case correctly. diff --git a/regression/memsafety/double_free/main.c b/regression/memsafety/double_free/main.c new file mode 100644 index 000000000..ee5589bd0 --- /dev/null +++ b/regression/memsafety/double_free/main.c @@ -0,0 +1,9 @@ +void *my_malloc(unsigned int size) { + return malloc(size); +} + +int main() { + void *a = my_malloc(sizeof(int)); + free(a); + free(a); +} diff --git a/regression/memsafety/double_free/test.desc b/regression/memsafety/double_free/test.desc new file mode 100644 index 000000000..7af3e2e02 --- /dev/null +++ b/regression/memsafety/double_free/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--pointer-check --inline +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +\[free.precondition.6\] free argument must be NULL or valid pointer: FAILURE diff --git a/regression/memsafety/simple_true/test.desc b/regression/memsafety/simple_true/test.desc index 8975589cd..a9c706a24 100644 --- a/regression/memsafety/simple_true/test.desc +++ b/regression/memsafety/simple_true/test.desc @@ -1,36 +1,6 @@ -KNOWNBUG +CORE main.c --heap --intervals --pointer-check --no-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ --- --- -CBMC 5.9 introduced changes to its implementation of some built-in functions, -the ones affecting this test are malloc and free. Malloc changes have been -already accounted for in 2LS codebase, however the control flow of free -is most likely causing problems in this test making one of the asserts fail: - -[main.pointer_dereference.27] dereference failure: deallocated dynamic object in *p: UNKNOWN - -This may be related to double free assertion, where GOTO changed from: - -... - IF !(__CPROVER_deallocated == ptr) THEN GOTO 6 - // 144 file line 18 function free - ASSERT 0 != 0 // double free - // 145 no location - ASSUME 0 != 0 - // 146 file line 29 function free - 6: _Bool record; -... - -to: - ASSERT ptr == NULL || __CPROVER_deallocated != ptr // double free - -Note the new ptr == NULL condition, this could be the root cause of -the problem. However further investigation is required -and will be done once the CBMC rebase is completed. According to the -C standard, free(NULL) is a valid construct (no operation) but 2LS doesn't -seem to handle this case correctly. - diff --git a/regression/preconditions/precond_contextsensitive1/test.desc b/regression/preconditions/precond_contextsensitive1/test.desc index b7e6db72f..ccfbfba68 100644 --- a/regression/preconditions/precond_contextsensitive1/test.desc +++ b/regression/preconditions/precond_contextsensitive1/test.desc @@ -3,4 +3,4 @@ main.c --context-sensitive --preconditions ^EXIT=5$ ^SIGNAL=0$ -^\[sign\]: sign#return_value#phi20 <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)sign#return_value#phi20\) <= 0 ==> x <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)x\) <= 0$ +^\[sign\]: sign#return_value#phi21 <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)sign#return_value#phi21\) <= 0 ==> x <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)x\) <= 0$ diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index be3e30fee..d8704d71a 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include #include #include @@ -396,6 +397,14 @@ int twols_parse_optionst::doit() register_languages(); + // configure gcc, if required + if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC) + { + gcc_versiont gcc_version; + gcc_version.get("gcc"); + configure_gcc(gcc_version); + } + if(get_goto_program(options)) return 6; @@ -1141,6 +1150,12 @@ bool twols_parse_optionst::process_goto_program( remove_dead_goto(goto_model); + // There's a bug in SSA creation that causes problems when a single SKIP + // instruction is a target of both a forward and a backward GOTO. + // This transformation fixes that by splitting such SKIPs into two. + // TODO: fix this properly in SSA, if possible. + fix_goto_targets(goto_model); + if(cmdline.isset("competition-mode")) { limit_array_bounds(goto_model); diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h index c1d60ec26..1fbd95ddc 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -197,6 +197,7 @@ class twols_parse_optionst: void handle_freed_ptr_compare(goto_modelt &goto_model); void assert_no_builtin_functions(goto_modelt &goto_model); void assert_no_atexit(goto_modelt &goto_model); + void fix_goto_targets(goto_modelt &goto_model); }; #endif diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp index a281a7101..5ed1e714b 100644 --- a/src/2ls/preprocessing_util.cpp +++ b/src/2ls/preprocessing_util.cpp @@ -674,7 +674,7 @@ void twols_parse_optionst::limit_array_bounds(goto_modelt &goto_model) if(size_expr.id()==ID_constant) { int size=std::stoi( - id2string(to_constant_expr(size_expr).get_value()), nullptr, 2); + id2string(to_constant_expr(size_expr).get_value()), nullptr, 16); // @TODO temporary solution - there seems to be a bug in the solver assert(size<=50000); } @@ -856,3 +856,51 @@ void twols_parse_optionst::assert_no_atexit(goto_modelt &goto_model) } } } + +/// Searches for SKIP instructions that are a target of both a forward and +/// a backward GOTO. Such instructions are split into 2 - the first one is +/// made the target of forward GOTOs and the second one is made the target of +/// backward GOTOs. +void twols_parse_optionst::fix_goto_targets(goto_modelt &goto_model) +{ + for (auto &f_it : goto_model.goto_functions.function_map) + { + Forall_goto_program_instructions(i_it, f_it.second.body) + { + if (i_it->incoming_edges.size() <= 1) + continue; + if (!i_it->is_skip()) + continue; + + bool has_backwards_goto = false; + bool has_forward_goto = false; + for (auto &incoming : i_it->incoming_edges) + { + if (incoming->location_number < i_it->location_number) + has_forward_goto = true; + if (incoming->location_number > i_it->location_number) + has_backwards_goto = true; + } + if (has_forward_goto && has_backwards_goto) + { + auto new_skip = f_it.second.body.insert_after( + i_it, + goto_programt::make_skip(i_it->source_location)); + + for (auto &incoming : i_it->incoming_edges) + { + if (incoming->location_number > i_it->location_number) + { + // Redirect backward GOTOs to the new skip + for (auto &target : incoming->targets) + { + if (target == i_it) + target = new_skip; + } + } + } + } + } + goto_model.goto_functions.update(); + } +} diff --git a/src/domains/heap_domain.cpp b/src/domains/heap_domain.cpp index d5b4b4513..d04f38968 100644 --- a/src/domains/heap_domain.cpp +++ b/src/domains/heap_domain.cpp @@ -216,6 +216,8 @@ const exprt heap_domaint::get_points_to_dest( { // Value from the solver must be converted into an expression exprt ptr_value=value_to_ptr_exprt(solver_value); + if(ptr_value.id()==ID_typecast) + ptr_value=to_typecast_expr(ptr_value).op(); if((ptr_value.id()==ID_constant && to_constant_expr(ptr_value).get_value()==ID_NULL) || @@ -228,18 +230,30 @@ const exprt heap_domaint::get_points_to_dest( { // Template row pointer points to the heap (p = &obj) assert(ptr_value.id()==ID_address_of); - if(to_address_of_expr(ptr_value).object().id()!=ID_symbol) + exprt obj=to_address_of_expr(ptr_value).object(); + if(obj.id()==ID_member) + { + // &(X.field) where field has offset 0 is equal to &X + auto &member=to_member_expr(obj); + auto field=member.get_component_name(); + auto struct_type=ns.follow(member.compound().type()); + if(struct_type.id()==ID_struct && + to_struct_type(struct_type).component_number(field)==0) + { + obj=member.compound(); + } + } + if(obj.id()!=ID_symbol) { // If solver did not return address of a symbol, it is considered // as nondet value. return nil_exprt(); } - symbol_exprt obj=to_symbol_expr( - to_address_of_expr(ptr_value).object()); + symbol_exprt symbol_obj=to_symbol_expr(obj); - if(obj.type()!=templ_row_expr.type() && - ns.follow(templ_row_expr.type().subtype())!=ns.follow(obj.type())) + if(symbol_obj.type()!=templ_row_expr.type() && + ns.follow(templ_row_expr.type().subtype())!=ns.follow(symbol_obj.type())) { if(!is_cprover_symbol(templ_row_expr)) { @@ -249,7 +263,7 @@ const exprt heap_domaint::get_points_to_dest( } // Add equality p == &obj - return std::move(obj); + return std::move(symbol_obj); } else return nil_exprt(); diff --git a/src/ssa/dynobj_instance_analysis.cpp b/src/ssa/dynobj_instance_analysis.cpp index ca92b5331..f0e9cae25 100644 --- a/src/ssa/dynobj_instance_analysis.cpp +++ b/src/ssa/dynobj_instance_analysis.cpp @@ -213,6 +213,7 @@ bool dynobj_instance_domaint::merge( trace_ptrt trace_to) { bool result=has_values.is_false() && !other.has_values.is_false(); + has_values=tvt::unknown(); for(auto &obj : other.must_alias_relations) { if(must_alias_relations.find(obj.first)==must_alias_relations.end()) diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp index 151267c78..0328ce1bb 100644 --- a/src/ssa/local_ssa.cpp +++ b/src/ssa/local_ssa.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -50,6 +51,9 @@ void local_SSAt::build_SSA() build_function_call(i_it); // build_unknown_objs(i_it); collect_record_frees(i_it); + + if (options.get_bool_option("competition-mode")) + disable_unsupported_instructions(i_it); } // collect custom templates in loop heads @@ -883,17 +887,18 @@ exprt local_SSAt::read_rhs_rec(const exprt &expr, locationt loc) const { // If the last definition of an object is at its allocation, we can only use // the corresponding symbol if the object has truly been allocated - // (allocation guard holds). Otherwise we need to use the last definition - // before the allocation. + // (allocation guard holds). After the rebase to a newer version of CBMC, + // the last definition may also be a PHI node at the end of malloc ( + // which covers the case-split whether malloc can fail). + // Otherwise we need to use the last definition before the allocation. auto def_it=ssa_analysis[loc].def_map.find(object.get_identifier()); - if(def_it!=ssa_analysis[loc].def_map.end() && - def_it->second.def.kind==ssa_domaint::deft::ALLOCATION) + auto maybe_alloc_def=get_recent_object_alloc_def(loc, def_it); + if(maybe_alloc_def.has_value()) { - locationt alloc_loc=def_it->second.def.loc; return if_exprt( - read_rhs(def_it->second.def.guard, alloc_loc), + read_rhs(maybe_alloc_def->guard, maybe_alloc_def->loc), read_rhs(object, loc), - read_rhs(object, alloc_loc)); + read_rhs(object, maybe_alloc_def->loc)); } else return read_rhs(object, loc); @@ -904,6 +909,32 @@ exprt local_SSAt::read_rhs_rec(const exprt &expr, locationt loc) const } } +/// Checks whether the last definition of the object is its allocation and +/// if so, return the allocation def. Otherwise returns nullopt. +optionalt local_SSAt::get_recent_object_alloc_def( + locationt loc, + const ssa_domaint::def_mapt::const_iterator &def) const +{ + if(def==ssa_analysis[loc].def_map.end()) + return nullopt; + + if(def->second.def.is_allocation()) + return def->second.def; + + // Not a direct allocation, follow the split if it is a phi node and add + // guard if at least one of the branches is an allocation. + if(def->second.def.is_phi()) + { + const auto &phi_branches= + ssa_analysis[def->second.def.loc].phi_nodes.find(def->first); + if(phi_branches!=ssa_analysis[def->second.def.loc].phi_nodes.end()) + for(const auto &phi_branch : phi_branches->second) + if(phi_branch.second.is_allocation()) + return phi_branch.second; + } + return nullopt; +} + void local_SSAt::replace_side_effects_rec( exprt &expr, locationt loc, unsigned &counter) const { @@ -1110,40 +1141,8 @@ void local_SSAt::assign_rec( { const if_exprt &if_expr=to_if_expr(lhs); - exprt::operandst other_cond_conj; - if(if_expr.true_case().get_bool("#heap_access") && - if_expr.cond().id()==ID_equal) - { - const exprt heap_object=if_expr.true_case(); - const ssa_objectt ptr_object(to_equal_expr(if_expr.cond()).lhs(), ns); - if(ptr_object) - { - const irep_idt ptr_id=ptr_object.get_identifier(); - const exprt cond=read_rhs(if_expr.cond(), loc); - - for(const dyn_obj_assignt &do_assign : dyn_obj_assigns[heap_object]) - { - if(!alias_analysis[loc].aliases.same_set( - ptr_id, do_assign.pointer_id)) - { - other_cond_conj.push_back(do_assign.cond); - } - } - - dyn_obj_assigns[heap_object].emplace_back(ptr_id, cond); - } - } - - exprt cond=if_expr.cond(); - if(!other_cond_conj.empty()) - { - const exprt other_cond=or_exprt( - not_exprt(conjunction(other_cond_conj)), - name(guard_symbol(), OBJECT_SELECT, loc)); - cond=and_exprt(cond, other_cond); - } exprt orig_rhs=fresh_rhs ? name(ssa_objectt(rhs, ns), OUT, loc) : rhs; - exprt new_rhs=if_exprt(cond, orig_rhs, if_expr.true_case()); + exprt new_rhs=if_exprt(if_expr.cond(), orig_rhs, if_expr.true_case()); assign_rec( if_expr.true_case(), new_rhs, @@ -1545,10 +1544,10 @@ void local_SSAt::collect_allocation_guards( void local_SSAt::collect_record_frees(local_SSAt::locationt loc) { - if(loc->is_decl()) + if(loc->is_assign()) { - const code_declt &code_decl=code_declt{loc->decl_symbol()}; - const exprt &symbol=code_decl.symbol(); + const code_assignt &code_assign=to_code_assign(loc->get_code()); + const exprt &symbol=code_assign.lhs(); if(symbol.id()!=ID_symbol) return; @@ -1648,3 +1647,13 @@ bool local_SSAt::can_reuse_symderef( return true; } + +void local_SSAt::disable_unsupported_instructions(locationt loc) +{ + if (loc->is_other()) + { + auto st = loc->get_code().get_statement(); + if(st=="array_copy" || st=="array_replace") + assert(false); + } +} diff --git a/src/ssa/local_ssa.h b/src/ssa/local_ssa.h index 846350d88..268f14060 100644 --- a/src/ssa/local_ssa.h +++ b/src/ssa/local_ssa.h @@ -51,7 +51,6 @@ class local_SSAt options, ssa_objects, ssa_value_ai), - alias_analysis(_function_identifier, _goto_function, ns), guard_map(_goto_function.body), function_identifier(_function_identifier), ssa_analysis(assignments), @@ -148,20 +147,6 @@ class local_SSAt // unknown heap objects var_sett unknown_objs; - // Maps members of dynamic object to a set of pointers used to access those - // objects when assigning them - class dyn_obj_assignt - { - public: - const irep_idt pointer_id; - const exprt cond; - - dyn_obj_assignt(const irep_idt &pointer_id, const exprt &cond): - pointer_id(pointer_id), cond(cond) {} - }; - typedef std::list dyn_obj_assignst; - std::map dyn_obj_assigns; - // Map dynamic object names to guards of their allocation std::map allocation_guards; @@ -239,8 +224,6 @@ class local_SSAt ssa_value_ait ssa_value_ai; assignmentst assignments; - may_alias_analysist alias_analysis; - // protected: guard_mapt guard_map; @@ -288,6 +271,9 @@ class local_SSAt void build_assertions(locationt loc); void build_unknown_objs(locationt loc); + // competition-mode specific checks + void disable_unsupported_instructions(locationt loc); + void collect_allocation_guards(const code_assignt &assign, locationt loc); void get_alloc_guard_rec(const exprt &expr, exprt old_guard); void collect_record_frees(locationt loc); @@ -296,6 +282,10 @@ class local_SSAt void collect_custom_templates(); replace_mapt template_newvars; exprt template_last_newvar; + + optionalt get_recent_object_alloc_def( + locationt loc, + const ssa_domaint::def_mapt::const_iterator &def) const; }; std::list & operator << diff --git a/src/ssa/malloc_ssa.cpp b/src/ssa/malloc_ssa.cpp index a46fc6b0a..05008f686 100644 --- a/src/ssa/malloc_ssa.cpp +++ b/src/ssa/malloc_ssa.cpp @@ -72,6 +72,8 @@ exprt create_dynamic_object( from_integer(0, index_type()), value_symbol.type.subtype()); object=index_expr; + if(is_concrete) + to_index_expr(object).array().set("#concrete", true); } else { @@ -289,6 +291,38 @@ static bool replace_malloc_rec( } } +/// Finds the latest assignment to lhs before location_number and: +/// - if the assignment rhs is a symbol, continues recursively +/// - otherwise returns the rhs +exprt get_malloc_size( + const exprt &lhs, + unsigned location_number, + const goto_functiont &goto_function) +{ + exprt result=nil_exprt(); + unsigned result_loc_num=0; + forall_goto_program_instructions(it, goto_function.body) + { + if(!it->is_assign()) + continue; + + if(lhs==it->assign_lhs()) + { + result=it->assign_rhs(); + if(result.id()==ID_typecast) + result=to_typecast_expr(result).op(); + result_loc_num=it->location_number; + } + + if(it->location_number==location_number) + break; + } + if(result.id()==ID_symbol) + return get_malloc_size(result, result_loc_num, goto_function); + + return result; +} + bool replace_malloc( goto_modelt &goto_model, const std::string &suffix, @@ -336,14 +370,8 @@ bool replace_malloc( function_copy.copy_from(f_it.second); constant_propagator_ait const_propagator(function_copy); const_propagator(f_it.first, function_copy, ns); - forall_goto_program_instructions(copy_i_it, function_copy.body) - { - if(copy_i_it->location_number==i_it->location_number) - { - assert(copy_i_it->is_assign()); - malloc_size=copy_i_it->get_assign().rhs(); - } - } + malloc_size=get_malloc_size( + i_it->assign_lhs(), i_it->location_number, function_copy); } } if(replace_malloc_rec(code_assign.rhs(), diff --git a/src/ssa/ssa_domain.h b/src/ssa/ssa_domain.h index a8f1088b7..5fe41303f 100644 --- a/src/ssa/ssa_domain.h +++ b/src/ssa/ssa_domain.h @@ -34,6 +34,7 @@ class ssa_domaint:public ai_domain_baset inline bool is_input() const { return kind==INPUT; } inline bool is_assignment() const { return kind==ASSIGNMENT; } inline bool is_phi() const { return kind==PHI; } + inline bool is_allocation() const { return kind==ALLOCATION; } }; friend inline bool operator==(const deft &a, const deft &b) diff --git a/src/ssa/ssa_unwinder.cpp b/src/ssa/ssa_unwinder.cpp index 36c96ae9d..bac7c8f1a 100644 --- a/src/ssa/ssa_unwinder.cpp +++ b/src/ssa/ssa_unwinder.cpp @@ -515,6 +515,31 @@ equal_exprt ssa_local_unwindert::build_exit_merge( return equal_exprt(e, re); } + +/// Check whether the expression contains signed left shift. +/// This is a hack for SV-comp to disable hoisting assertions for this +/// operation. +bool has_overflow_shl(const exprt &expr) +{ + if(expr.id()==ID_shl) + { + binary_exprt shl=to_binary_expr(expr); + if(shl.op0().type().id()==ID_signedbv) + return true; + } + else + { + // Recursively go through the operands + if(!expr.has_operands()) + return false; + else + forall_operands(o_it, expr) + if(has_overflow_shl(*o_it)) + return true; + } + return false; +} + /// adds the assumptions for hoisted assertions for the current instance void ssa_local_unwindert::add_hoisted_assertions(loopt &loop, bool is_last) { @@ -525,11 +550,10 @@ void ssa_local_unwindert::add_hoisted_assertions(loopt &loop, bool is_last) if(!is_last // only add assumptions if we are not in %0 iteration && is_kinduction && !it->second.assertions.empty() #ifdef COMPETITION - && !(it->first->guard.id()==ID_not && - to_not_expr(it->first->guard).op().id()==ID_overflow_shl)) + && !has_overflow_shl(it->first->guard)) #endif { - exprt e=disjunction(it->second.exit_conditions); + exprt e=conjunction(it->second.exit_conditions); SSA.rename(e, loop.body_nodes.begin()->location); SSA.nodes.push_back( local_SSAt::nodet(it->first, SSA.nodes.end())); // add new node