diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index e4c5a8c25c6..3ec8698456d 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -176,7 +176,9 @@ void dep_graph_domaint::data_dependencies( { bool found=false; for(const auto &wr : w_range.second) + { for(const auto &r_range : r_ranges) + { if(!found && may_be_def_use_pair(wr.first, wr.second, r_range.first, r_range.second)) @@ -185,6 +187,8 @@ void dep_graph_domaint::data_dependencies( data_deps.insert(w_range.first); found=true; } + } + } } dep_graph.reaching_definitions()[to].clear_cache(it->first); diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 6c0039d5f86..ecdf18d1e9e 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -432,12 +432,18 @@ void rw_range_sett::get_objects_address_of(const exprt &object) object.id() == ID_label || object.id() == ID_array || object.id() == ID_null_object) + { // constant, nothing to do return; + } else if(object.id()==ID_symbol) + { get_objects_rec(get_modet::READ, object); + } else if(object.id()==ID_dereference) + { get_objects_rec(get_modet::READ, object); + } else if(object.id()==ID_index) { const index_exprt &index=to_index_expr(object); diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index a8cbd48afa5..654804e510c 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -54,9 +54,9 @@ literalt bv_pointerst::convert_rest(const exprt &expr) literalt l=prop.new_variable(); postponed_list.push_back(postponedt()); - postponed_list.back().op=convert_bv(operands[0]); + postponed_list.back().op = convert_bv(operands[0]); postponed_list.back().bv.push_back(l); - postponed_list.back().expr=expr; + postponed_list.back().expr = expr; return l; } @@ -734,7 +734,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv) void bv_pointerst::do_postponed( const postponedt &postponed) { - if(postponed.expr.id()==ID_dynamic_object) + if(postponed.expr.id() == ID_dynamic_object) { const pointer_logict::objectst &objects= pointer_logic.objects; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 89e44cc4230..345d6ff5506 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1398,7 +1398,7 @@ void smt2_convt::convert_expr(const exprt &expr) if(ext>0) out << ")"; // zero_extend } - else if(expr.id()==ID_dynamic_object) + else if(expr.id() == ID_dynamic_object) { convert_is_dynamic_object(expr); } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 9df4c4ff51c..a1ca8fa54b5 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2166,8 +2166,10 @@ bool simplify_exprt::simplify_node(exprt &expr) result=simplify_byte_extract(to_byte_extract_expr(expr)) && result; else if(expr.id()==ID_pointer_object) result=simplify_pointer_object(expr) && result; - else if(expr.id()==ID_dynamic_object) - result=simplify_dynamic_object(expr) && result; + else if(expr.id() == ID_dynamic_object) + { + result = simplify_dynamic_object(expr) && result; + } else if(expr.id()==ID_invalid_pointer) result=simplify_invalid_pointer(expr) && result; else if(expr.id()==ID_object_size) diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 1220f7babb3..2dc316073ba 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1706,11 +1706,12 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) if(expr.op0().id()==ID_address_of && expr.op0().operands().size()==1) { - if(expr.op0().op0().id()==ID_symbol || - expr.op0().op0().id()==ID_dynamic_object || - expr.op0().op0().id()==ID_member || - expr.op0().op0().id()==ID_index || - expr.op0().op0().id()==ID_string_constant) + if( + expr.op0().op0().id() == ID_symbol || + expr.op0().op0().id() == ID_dynamic_object || + expr.op0().op0().id() == ID_member || + expr.op0().op0().id() == ID_index || + expr.op0().op0().id() == ID_string_constant) { expr=false_exprt(); return false; diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 5f442689504..ba68bbd0190 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -463,15 +463,18 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr) if(op.id()==ID_address_of) { - if(op.operands().size()!=1 || - (op.op0().id()!=ID_symbol && - op.op0().id()!=ID_dynamic_object && - op.op0().id()!=ID_string_constant)) + if( + op.operands().size() != 1 || + (op.op0().id() != ID_symbol && op.op0().id() != ID_dynamic_object && + op.op0().id() != ID_string_constant)) + { return true; + } } - else if(op.id()!=ID_constant || - op.get(ID_value)!=ID_NULL) + else if(op.id() != ID_constant || op.get(ID_value) != ID_NULL) + { return true; + } } bool equal=expr.op0().op0()==expr.op1().op0();