diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 344f4a85ed1..b907cef042f 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -228,8 +228,7 @@ void goto_checkt::div_by_zero_check( if(zero.is_nil()) throw "no zero of argument type of operator "+expr.id_string(); - exprt inequality(ID_notequal, bool_typet()); - inequality.copy_to_operands(expr.op1(), zero); + const notequal_exprt inequality(expr.op1(), zero); add_guarded_claim( inequality, @@ -329,8 +328,7 @@ void goto_checkt::mod_by_zero_check( if(zero.is_nil()) throw "no zero of argument type of operator "+expr.id_string(); - exprt inequality(ID_notequal, bool_typet()); - inequality.copy_to_operands(expr.op1(), zero); + const notequal_exprt inequality(expr.op1(), zero); add_guarded_claim( inequality, @@ -374,13 +372,13 @@ void goto_checkt::conversion_check( if(new_width>=old_width) return; // always ok - binary_relation_exprt no_overflow_upper(ID_le); - no_overflow_upper.lhs()=expr.op0(); - no_overflow_upper.rhs()=from_integer(power(2, new_width-1)-1, old_type); + const binary_relation_exprt no_overflow_upper( + expr.op0(), + ID_le, + from_integer(power(2, new_width - 1) - 1, old_type)); - binary_relation_exprt no_overflow_lower(ID_ge); - no_overflow_lower.lhs()=expr.op0(); - no_overflow_lower.rhs()=from_integer(-power(2, new_width-1), old_type); + const binary_relation_exprt no_overflow_lower( + expr.op0(), ID_ge, from_integer(-power(2, new_width - 1), old_type)); add_guarded_claim( and_exprt(no_overflow_lower, no_overflow_upper), @@ -396,9 +394,10 @@ void goto_checkt::conversion_check( if(new_width>=old_width+1) return; // always ok - binary_relation_exprt no_overflow_upper(ID_le); - no_overflow_upper.lhs()=expr.op0(); - no_overflow_upper.rhs()=from_integer(power(2, new_width-1)-1, old_type); + const binary_relation_exprt no_overflow_upper( + expr.op0(), + ID_le, + from_integer(power(2, new_width - 1) - 1, old_type)); add_guarded_claim( no_overflow_upper, @@ -413,15 +412,13 @@ void goto_checkt::conversion_check( // Note that the fractional part is truncated! ieee_floatt upper(to_floatbv_type(old_type)); upper.from_integer(power(2, new_width-1)); - binary_relation_exprt no_overflow_upper(ID_lt); - no_overflow_upper.lhs()=expr.op0(); - no_overflow_upper.rhs()=upper.to_expr(); + const binary_relation_exprt no_overflow_upper( + expr.op0(), ID_lt, upper.to_expr()); ieee_floatt lower(to_floatbv_type(old_type)); lower.from_integer(-power(2, new_width-1)-1); - binary_relation_exprt no_overflow_lower(ID_gt); - no_overflow_lower.lhs()=expr.op0(); - no_overflow_lower.rhs()=lower.to_expr(); + const binary_relation_exprt no_overflow_lower( + expr.op0(), ID_gt, lower.to_expr()); add_guarded_claim( and_exprt(no_overflow_lower, no_overflow_upper), @@ -443,9 +440,8 @@ void goto_checkt::conversion_check( if(new_width>=old_width-1) { // only need lower bound check - binary_relation_exprt no_overflow_lower(ID_ge); - no_overflow_lower.lhs()=expr.op0(); - no_overflow_lower.rhs()=from_integer(0, old_type); + const binary_relation_exprt no_overflow_lower( + expr.op0(), ID_ge, from_integer(0, old_type)); add_guarded_claim( no_overflow_lower, @@ -458,13 +454,11 @@ void goto_checkt::conversion_check( else { // need both - binary_relation_exprt no_overflow_upper(ID_le); - no_overflow_upper.lhs()=expr.op0(); - no_overflow_upper.rhs()=from_integer(power(2, new_width)-1, old_type); + const binary_relation_exprt no_overflow_upper( + expr.op0(), ID_le, from_integer(power(2, new_width) - 1, old_type)); - binary_relation_exprt no_overflow_lower(ID_ge); - no_overflow_lower.lhs()=expr.op0(); - no_overflow_lower.rhs()=from_integer(0, old_type); + const binary_relation_exprt no_overflow_lower( + expr.op0(), ID_ge, from_integer(0, old_type)); add_guarded_claim( and_exprt(no_overflow_lower, no_overflow_upper), @@ -481,9 +475,8 @@ void goto_checkt::conversion_check( if(new_width>=old_width) return; // always ok - binary_relation_exprt no_overflow_upper(ID_le); - no_overflow_upper.lhs()=expr.op0(); - no_overflow_upper.rhs()=from_integer(power(2, new_width)-1, old_type); + const binary_relation_exprt no_overflow_upper( + expr.op0(), ID_le, from_integer(power(2, new_width) - 1, old_type)); add_guarded_claim( no_overflow_upper, @@ -498,15 +491,13 @@ void goto_checkt::conversion_check( // Note that the fractional part is truncated! ieee_floatt upper(to_floatbv_type(old_type)); upper.from_integer(power(2, new_width)-1); - binary_relation_exprt no_overflow_upper(ID_lt); - no_overflow_upper.lhs()=expr.op0(); - no_overflow_upper.rhs()=upper.to_expr(); + const binary_relation_exprt no_overflow_upper( + expr.op0(), ID_lt, upper.to_expr()); ieee_floatt lower(to_floatbv_type(old_type)); lower.from_integer(-1); - binary_relation_exprt no_overflow_lower(ID_gt); - no_overflow_lower.lhs()=expr.op0(); - no_overflow_lower.rhs()=lower.to_expr(); + const binary_relation_exprt no_overflow_lower( + expr.op0(), ID_gt, lower.to_expr()); add_guarded_claim( and_exprt(no_overflow_lower, no_overflow_upper), @@ -665,8 +656,8 @@ void goto_checkt::float_overflow_check( if(ns.follow(expr.op0().type()).id()==ID_floatbv) { // float-to-float - unary_exprt op0_inf(ID_isinf, expr.op0(), bool_typet()); - unary_exprt new_inf(ID_isinf, expr, bool_typet()); + const isinf_exprt op0_inf(expr.op0()); + const isinf_exprt new_inf(expr); or_exprt overflow_check(op0_inf, not_exprt(new_inf)); @@ -681,7 +672,7 @@ void goto_checkt::float_overflow_check( else { // non-float-to-float - unary_exprt new_inf(ID_isinf, expr, bool_typet()); + const isinf_exprt new_inf(expr); add_guarded_claim( not_exprt(new_inf), @@ -699,8 +690,8 @@ void goto_checkt::float_overflow_check( assert(expr.operands().size()==2); // Can overflow if dividing by something small - unary_exprt new_inf(ID_isinf, expr, bool_typet()); - unary_exprt op0_inf(ID_isinf, expr.op0(), bool_typet()); + const isinf_exprt new_inf(expr); + const isinf_exprt op0_inf(expr.op0()); or_exprt overflow_check(op0_inf, not_exprt(new_inf)); @@ -730,9 +721,9 @@ void goto_checkt::float_overflow_check( if(expr.operands().size()==2) { // Can overflow - unary_exprt new_inf(ID_isinf, expr, bool_typet()); - unary_exprt op0_inf(ID_isinf, expr.op0(), bool_typet()); - unary_exprt op1_inf(ID_isinf, expr.op1(), bool_typet()); + const isinf_exprt new_inf(expr); + const isinf_exprt op0_inf(expr.op0()); + const isinf_exprt op1_inf(expr.op1()); or_exprt overflow_check(op0_inf, op1_inf, not_exprt(new_inf)); @@ -791,11 +782,11 @@ void goto_checkt::nan_check( // there a two ways to get a new NaN on division: // 0/0 = NaN and x/inf = NaN // (note that x/0 = +-inf for x!=0 and x!=inf) - exprt zero_div_zero=and_exprt( + const and_exprt zero_div_zero( ieee_float_equal_exprt(expr.op0(), from_integer(0, expr.op0().type())), ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type()))); - exprt div_inf=unary_exprt(ID_isinf, expr.op1(), bool_typet()); + const isinf_exprt div_inf(expr.op1()); isnan=or_exprt(zero_div_zero, div_inf); } @@ -807,13 +798,13 @@ void goto_checkt::nan_check( assert(expr.operands().size()==2); // Inf * 0 is NaN - exprt inf_times_zero=and_exprt( - unary_exprt(ID_isinf, expr.op0(), bool_typet()), + const and_exprt inf_times_zero( + isinf_exprt(expr.op0()), ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type()))); - exprt zero_times_inf=and_exprt( + const and_exprt zero_times_inf( ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type())), - unary_exprt(ID_isinf, expr.op0(), bool_typet())); + isinf_exprt(expr.op0())); isnan=or_exprt(inf_times_zero, zero_times_inf); } @@ -1055,13 +1046,9 @@ void goto_checkt::pointer_validity_check( if(flags.is_unknown() || flags.is_dynamic_heap()) { - exprt dynamic_bounds= - or_exprt(dynamic_object_lower_bound(pointer, ns, access_lb), - dynamic_object_upper_bound( - pointer, - dereference_type, - ns, - access_ub)); + const or_exprt dynamic_bounds( + dynamic_object_lower_bound(pointer, ns, access_lb), + dynamic_object_upper_bound(pointer, dereference_type, ns, access_ub)); add_guarded_claim( or_exprt( @@ -1080,13 +1067,9 @@ void goto_checkt::pointer_validity_check( flags.is_dynamic_local() || flags.is_static_lifetime()) { - exprt object_bounds= - or_exprt(object_lower_bound(pointer, ns, access_lb), - object_upper_bound( - pointer, - dereference_type, - ns, - access_ub)); + const or_exprt object_bounds( + object_lower_bound(pointer, ns, access_lb), + object_upper_bound(pointer, dereference_type, ns, access_ub)); add_guarded_claim( or_exprt(allocs, dynamic_object(pointer), not_exprt(object_bounds)), @@ -1672,12 +1655,11 @@ void goto_checkt::goto_check( exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); if(!base_type_eq(lhs.type(), address_of_expr.type(), ns)) address_of_expr.make_typecast(lhs.type()); - exprt rhs= - if_exprt( - side_effect_expr_nondett(bool_typet()), - address_of_expr, - lhs, - lhs.type()); + const if_exprt rhs( + side_effect_expr_nondett(bool_typet()), + address_of_expr, + lhs, + lhs.type()); t->source_location=i.source_location; t->code=code_assignt(lhs, rhs); t->code.add_source_location()=i.source_location; diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp index 97211760f52..311c310dc89 100644 --- a/src/analyses/invariant_propagation.cpp +++ b/src/analyses/invariant_propagation.cpp @@ -98,15 +98,10 @@ void invariant_propagationt::get_objects_rec( { const struct_typet &struct_type=to_struct_type(t); - const struct_typet::componentst &c=struct_type.components(); - - exprt member_expr(ID_member); - member_expr.copy_to_operands(src); - - for(const auto &component : c) + for(const auto &component : struct_type.components()) { - member_expr.set(ID_component_name, component.get_name()); - member_expr.type()=component.type(); + const member_exprt member_expr( + src, component.get_name(), component.type()); // recursive call get_objects_rec(member_expr, dest); } diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index 0445d5a1596..e1819908938 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -491,23 +491,15 @@ void invariant_sett::strengthen_rec(const exprt &expr) { const struct_typet &struct_type=to_struct_type(op_type); - exprt lhs_member_expr(ID_member); - exprt rhs_member_expr(ID_member); - lhs_member_expr.copy_to_operands(expr.op0()); - rhs_member_expr.copy_to_operands(expr.op1()); for(const auto &comp : struct_type.components()) { - const irep_idt &component_name=comp.get(ID_name); + const member_exprt lhs_member_expr( + expr.op0(), comp.get_name(), comp.type()); + const member_exprt rhs_member_expr( + expr.op1(), comp.get_name(), comp.type()); - lhs_member_expr.set(ID_component_name, component_name); - rhs_member_expr.set(ID_component_name, component_name); - lhs_member_expr.type()=comp.type(); - rhs_member_expr.type()=comp.type(); - - equal_exprt equality; - equality.lhs()=lhs_member_expr; - equality.rhs()=rhs_member_expr; + const equal_exprt equality(lhs_member_expr, rhs_member_expr); // recursive call strengthen_rec(equality); @@ -870,11 +862,7 @@ exprt invariant_sett::get_constant(const exprt &expr) const if(expr.type().id()==ID_pointer) { if(value==0) - { - exprt tmp(ID_constant, expr.type()); - tmp.set(ID_value, ID_NULL); - return tmp; - } + return null_pointer_exprt(to_pointer_type(expr.type())); } else return from_integer(value, expr.type()); @@ -884,9 +872,7 @@ exprt invariant_sett::get_constant(const exprt &expr) const if(e.type()==expr.type()) return e; - exprt tmp(ID_typecast, expr.type()); - tmp.copy_to_operands(e); - return tmp; + return typecast_exprt(e, expr.type()); } } } diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 486ef7a1f8a..a632d616fc2 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -270,12 +270,9 @@ bool generate_ansi_c_start_function( // assume argc is at least one exprt one=from_integer(1, argc_symbol.type); - exprt ge(ID_ge, typet(ID_bool)); - ge.copy_to_operands(argc_symbol.symbol_expr(), one); + const binary_relation_exprt ge(argc_symbol.symbol_expr(), ID_ge, one); - codet assumption; - assumption.set_statement(ID_assume); - assumption.move_to_operands(ge); + code_assumet assumption(ge); init_code.move_to_operands(assumption); } @@ -286,12 +283,10 @@ bool generate_ansi_c_start_function( exprt bound_expr=from_integer(upper_bound, argc_symbol.type); - exprt le(ID_le, typet(ID_bool)); - le.copy_to_operands(argc_symbol.symbol_expr(), bound_expr); + const binary_relation_exprt le( + argc_symbol.symbol_expr(), ID_le, bound_expr); - codet assumption; - assumption.set_statement(ID_assume); - assumption.move_to_operands(le); + code_assumet assumption(le); init_code.move_to_operands(assumption); } @@ -325,12 +320,10 @@ bool generate_ansi_c_start_function( exprt max_minus_one=from_integer(max-1, envp_size_symbol.type); - exprt le(ID_le, bool_typet()); - le.copy_to_operands(envp_size_symbol.symbol_expr(), max_minus_one); + const binary_relation_exprt le( + envp_size_symbol.symbol_expr(), ID_le, max_minus_one); - codet assumption; - assumption.set_statement(ID_assume); - assumption.move_to_operands(le); + code_assumet assumption(le); init_code.move_to_operands(assumption); } @@ -341,8 +334,7 @@ bool generate_ansi_c_start_function( exprt zero_string(ID_zero_string, array_typet()); zero_string.type().subtype()=char_type(); zero_string.type().set(ID_size, "infinity"); - exprt index(ID_index, char_type()); - index.copy_to_operands(zero_string, from_integer(0, uint_type())); + const index_exprt index(zero_string, from_integer(0, uint_type())); exprt address_of=address_of_exprt(index, pointer_type(char_type())); if(argv_symbol.type.subtype()!=address_of.type()) @@ -358,13 +350,11 @@ bool generate_ansi_c_start_function( { // assign argv[argc] to NULL - exprt null(ID_constant, argv_symbol.type.subtype()); - null.set(ID_value, ID_NULL); + const null_pointer_exprt null( + to_pointer_type(argv_symbol.type.subtype())); - exprt index_expr(ID_index, argv_symbol.type.subtype()); - index_expr.copy_to_operands( - argv_symbol.symbol_expr(), - argc_symbol.symbol_expr()); + index_exprt index_expr( + argv_symbol.symbol_expr(), argc_symbol.symbol_expr()); // disable bounds check on that one index_expr.set("bounds_check", false); @@ -378,23 +368,17 @@ bool generate_ansi_c_start_function( const symbolt &envp_size_symbol=ns.lookup("envp_size'"); // assume envp[envp_size] is NULL - exprt null(ID_constant, envp_symbol.type.subtype()); - null.set(ID_value, ID_NULL); - - exprt index_expr(ID_index, envp_symbol.type.subtype()); - index_expr.copy_to_operands( - envp_symbol.symbol_expr(), - envp_size_symbol.symbol_expr()); + const null_pointer_exprt null( + to_pointer_type(envp_symbol.type.subtype())); + index_exprt index_expr( + envp_symbol.symbol_expr(), envp_size_symbol.symbol_expr()); // disable bounds check on that one index_expr.set("bounds_check", false); - exprt is_null(ID_equal, typet(ID_bool)); - is_null.copy_to_operands(index_expr, null); + const equal_exprt is_null(index_expr, null); - codet assumption2; - assumption2.set_statement(ID_assume); - assumption2.move_to_operands(is_null); + code_assumet assumption2(is_null); init_code.move_to_operands(assumption2); } diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index 771fd17493c..9d51bca80e8 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -486,11 +486,9 @@ void c_typecastt::implicit_typecast_followed( if(!check_c_implicit_typecast(src_type_no_const, comp.type())) { // build union constructor - exprt union_expr(ID_union, orig_dest_type); - union_expr.move_to_operands(expr); + union_exprt union_expr(comp.get_name(), expr, orig_dest_type); if(!src_type.full_eq(src_type_no_const)) - do_typecast(union_expr.op0(), src_type_no_const); - union_expr.set(ID_component_name, comp.get_name()); + do_typecast(union_expr.op(), src_type_no_const); expr=union_expr; return; // ok } diff --git a/src/ansi-c/c_typecheck_argc_argv.cpp b/src/ansi-c/c_typecheck_argc_argv.cpp index 879887db5b2..dfc752c8e19 100644 --- a/src/ansi-c/c_typecheck_argc_argv.cpp +++ b/src/ansi-c/c_typecheck_argc_argv.cpp @@ -67,16 +67,12 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol) } // we make the type of this thing an array of pointers - typet argv_type=array_typet(); - argv_type.subtype()=op1.type().subtype(); - // need to add one to the size -- the array is terminated // with NULL exprt one_expr=from_integer(1, argc_new_symbol->type); - exprt size_expr(ID_plus, argc_new_symbol->type); - size_expr.copy_to_operands(argc_new_symbol->symbol_expr(), one_expr); - argv_type.add(ID_size).swap(size_expr); + const plus_exprt size_expr(argc_new_symbol->symbol_expr(), one_expr); + const array_typet argv_type(op1.type().subtype(), size_expr); symbolt argv_symbol; diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b49ccb2289d..6c7b3ddbcf5 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -896,23 +896,19 @@ void c_typecheck_baset::typecheck_side_effect_statement_expression( if(fc.lhs().is_nil()) { - codet code_expr(ID_expression); + code_expressiont code_expr(sideeffect); code_expr.add_source_location() = fc.source_location(); - code_expr.move_to_operands(sideeffect); last.swap(code_expr); } else { - codet code_expr(ID_expression); - code_expr.add_source_location() = fc.source_location(); - - exprt assign(ID_side_effect); - assign.set(ID_statement, ID_assign); + side_effect_exprt assign(ID_assign, sideeffect.type()); assign.add_source_location()=fc.source_location(); assign.move_to_operands(fc.lhs(), sideeffect); - assign.type()=assign.op1().type(); - code_expr.move_to_operands(assign); + code_expressiont code_expr(assign); + code_expr.add_source_location() = fc.source_location(); + last.swap(code_expr); } } @@ -1446,8 +1442,7 @@ void c_typecheck_baset::typecheck_expr_ptrmember(exprt &expr) // turn x->y into (*x).y - exprt deref(ID_dereference); - deref.move_to_operands(expr.op0()); + dereference_exprt deref(expr.op0()); deref.add_source_location()=expr.source_location(); typecheck_expr_dereference(deref); @@ -1974,10 +1969,9 @@ void c_typecheck_baset::typecheck_side_effect_function_call( } else { - exprt tmp(ID_dereference, f_op_type.subtype()); + dereference_exprt tmp(f_op, f_op_type.subtype()); tmp.set(ID_C_implicit, true); tmp.add_source_location()=f_op.source_location(); - tmp.move_to_operands(f_op); f_op.swap(tmp); } @@ -2038,9 +2032,8 @@ exprt c_typecheck_baset::do_special_functions( typecheck_function_call_arguments(expr); - exprt get_must_expr= - binary_predicate_exprt( - expr.arguments()[0], "get_must", expr.arguments()[1]); + binary_predicate_exprt get_must_expr( + expr.arguments()[0], "get_must", expr.arguments()[1]); get_must_expr.add_source_location()=source_location; return get_must_expr; @@ -2056,9 +2049,8 @@ exprt c_typecheck_baset::do_special_functions( typecheck_function_call_arguments(expr); - exprt get_may_expr= - binary_predicate_exprt( - expr.arguments()[0], "get_may", expr.arguments()[1]); + binary_predicate_exprt get_may_expr( + expr.arguments()[0], "get_may", expr.arguments()[1]); get_may_expr.add_source_location()=source_location; return get_may_expr; @@ -2072,8 +2064,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - predicate_exprt same_object_expr(ID_invalid_pointer); - same_object_expr.operands()=expr.arguments(); + exprt same_object_expr = invalid_pointer(expr.arguments().front()); same_object_expr.add_source_location()=source_location; return same_object_expr; @@ -2202,8 +2193,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt isnan_expr(ID_isnan, bool_typet()); - isnan_expr.operands()=expr.arguments(); + isnan_exprt isnan_expr(expr.arguments().front()); isnan_expr.add_source_location()=source_location; return isnan_expr; @@ -2219,8 +2209,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt isfinite_expr(ID_isfinite, bool_typet()); - isfinite_expr.operands()=expr.arguments(); + isfinite_exprt isfinite_expr(expr.arguments().front()); isfinite_expr.add_source_location()=source_location; return isfinite_expr; @@ -2267,8 +2256,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt abs_expr(ID_abs, expr.type()); - abs_expr.operands()=expr.arguments(); + abs_exprt abs_expr(expr.arguments().front()); abs_expr.add_source_location()=source_location; return abs_expr; @@ -2282,8 +2270,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt malloc_expr=side_effect_exprt(ID_allocate); - malloc_expr.type()=expr.type(); + side_effect_exprt malloc_expr(ID_allocate, expr.type()); malloc_expr.add_source_location()=source_location; malloc_expr.operands()=expr.arguments(); @@ -2301,8 +2288,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt isinf_expr(ID_isinf, bool_typet()); - isinf_expr.operands()=expr.arguments(); + isinf_exprt isinf_expr(expr.arguments().front()); isinf_expr.add_source_location()=source_location; return isinf_expr; @@ -2318,8 +2304,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt isnormal_expr(ID_isnormal, bool_typet()); - isnormal_expr.operands()=expr.arguments(); + isnormal_exprt isnormal_expr(expr.arguments().front()); isnormal_expr.add_source_location()=source_location; return isnormal_expr; @@ -2338,8 +2323,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt sign_expr(ID_sign, bool_typet()); - sign_expr.operands()=expr.arguments(); + sign_exprt sign_expr(expr.arguments().front()); sign_expr.add_source_location()=source_location; return sign_expr; diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 5128b7802b4..15bb1bd4608 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1890,8 +1890,7 @@ std::string expr2ct::convert_constant( if(src.find(ID_C_c_sizeof_type).is_not_nil() && sizeof_nesting==0) { - exprt sizeof_expr=nil_exprt(); - sizeof_expr=build_sizeof_expr(to_constant_expr(src), ns); + const exprt sizeof_expr = build_sizeof_expr(to_constant_expr(src), ns); if(sizeof_expr.is_not_nil()) { diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp index 8838a2e3492..626b046b5fa 100644 --- a/src/ansi-c/literals/convert_float_literal.cpp +++ b/src/ansi-c/literals/convert_float_literal.cpp @@ -137,13 +137,8 @@ exprt convert_float_literal(const std::string &src) if(is_imaginary) { - complex_typet complex_type; - complex_type.subtype()=result.type(); - exprt complex_expr(ID_complex, complex_type); - complex_expr.operands().resize(2); - complex_expr.op0()=from_integer(0, result.type()); - complex_expr.op1()=result; - return complex_expr; + const complex_typet complex_type(result.type()); + return complex_exprt(from_integer(0, result.type()), result, complex_type); } return result; diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 05fceb54923..e1a9f916ad0 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -227,10 +227,8 @@ bool bmc_covert::operator()() if(it->is_assert()) { assert(it->source.pc->is_assert()); - exprt c= - conjunction({ // NOLINT(whitespace/braces) - literal_exprt(it->guard_literal), - literal_exprt(!it->cond_literal) }); + const and_exprt c( + literal_exprt(it->guard_literal), literal_exprt(!it->cond_literal)); literalt l_c=solver.convert(c); goal_map[id(it->source.pc)].add_instance(it, l_c); } diff --git a/src/cbmc/bv_cbmc.cpp b/src/cbmc/bv_cbmc.cpp index e1652695796..06a32d52686 100644 --- a/src/cbmc/bv_cbmc.cpp +++ b/src/cbmc/bv_cbmc.cpp @@ -39,34 +39,23 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr) { // constraint: new_cycle>=old_cycle - exprt rel_expr(ID_ge, bool_typet()); - rel_expr.copy_to_operands(new_cycle, old_cycle); - set_to_true(rel_expr); + set_to_true(binary_relation_exprt(new_cycle, ID_ge, old_cycle)); } { // constraint: new_cycle<=bound+1 exprt one=from_integer(1, bound.type()); - - exprt bound_plus1(ID_plus, bound.type()); - bound_plus1.reserve_operands(2); - bound_plus1.copy_to_operands(bound); - bound_plus1.move_to_operands(one); - - exprt rel_expr(ID_le, bool_typet()); - rel_expr.copy_to_operands(new_cycle, bound_plus1); - set_to_true(rel_expr); + const plus_exprt bound_plus1(bound, one); + set_to_true(binary_relation_exprt(new_cycle, ID_le, bound_plus1)); } for(mp_integer i=0; i<=bound_value; i=i+1) { // replace cycle_var by old_cycle+i; - exprt old_cycle_plus_i(ID_plus, old_cycle.type()); - old_cycle_plus_i.operands().resize(2); - old_cycle_plus_i.op0()=old_cycle; - old_cycle_plus_i.op1()=from_integer(i, old_cycle.type()); + const plus_exprt old_cycle_plus_i( + old_cycle, from_integer(i, old_cycle.type())); exprt tmp_predicate=predicate; replace_expr(cycle_var, old_cycle_plus_i, tmp_predicate); @@ -79,50 +68,25 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr) // assume(property); { - exprt cycle_le_bound(ID_le, bool_typet()); - cycle_le_bound.operands().resize(2); - cycle_le_bound.op0()=old_cycle_plus_i; - cycle_le_bound.op1()=bound; - - exprt cycle_lt_new_cycle(ID_lt, bool_typet()); - cycle_lt_new_cycle.operands().resize(2); - cycle_lt_new_cycle.op0()=old_cycle_plus_i; - cycle_lt_new_cycle.op1()=new_cycle; - - exprt and_expr(ID_and, bool_typet()); - and_expr.operands().resize(2); - and_expr.op0().swap(cycle_le_bound); - and_expr.op1().swap(cycle_lt_new_cycle); - - exprt top_impl(ID_implies, bool_typet()); - top_impl.reserve_operands(2); - top_impl.move_to_operands(and_expr); - top_impl.copy_to_operands(tmp_predicate); + const binary_relation_exprt cycle_le_bound( + old_cycle_plus_i, ID_le, bound); + const binary_relation_exprt cycle_lt_new_cycle( + old_cycle_plus_i, ID_lt, new_cycle); + const and_exprt and_expr(cycle_le_bound, cycle_lt_new_cycle); + + implies_exprt top_impl(and_expr, tmp_predicate); top_impl.op1().make_not(); set_to_true(top_impl); } { - exprt cycle_le_bound(ID_le, bool_typet()); - cycle_le_bound.operands().resize(2); - cycle_le_bound.op0()=old_cycle_plus_i; - cycle_le_bound.op1()=bound; - - exprt cycle_eq_new_cycle(ID_equal, bool_typet()); - cycle_eq_new_cycle.operands().resize(2); - cycle_eq_new_cycle.op0()=old_cycle_plus_i; - cycle_eq_new_cycle.op1()=new_cycle; - - exprt and_expr(ID_and, bool_typet()); - and_expr.operands().resize(2); - and_expr.op0().swap(cycle_le_bound); - and_expr.op1().swap(cycle_eq_new_cycle); - - exprt top_impl(ID_implies, bool_typet()); - top_impl.reserve_operands(2); - top_impl.move_to_operands(and_expr); - top_impl.copy_to_operands(tmp_predicate); + const binary_relation_exprt cycle_le_bound( + old_cycle_plus_i, ID_le, bound); + const equal_exprt cycle_eq_new_cycle(old_cycle_plus_i, new_cycle); + const and_exprt and_expr(cycle_le_bound, cycle_eq_new_cycle); + + const implies_exprt top_impl(and_expr, tmp_predicate); set_to_true(top_impl); } @@ -148,9 +112,7 @@ bvt bv_cbmct::convert_waitfor_symbol(const exprt &expr) // constraint: result<=bound - exprt rel_expr(ID_le, bool_typet()); - rel_expr.copy_to_operands(result, bound); - set_to_true(rel_expr); + set_to_true(binary_relation_exprt(result, ID_le, bound)); return convert_bitvector(result); } diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp index e2eeaae1ca6..4639103e47e 100644 --- a/src/cpp/cpp_constructor.cpp +++ b/src/cpp/cpp_constructor.cpp @@ -103,7 +103,7 @@ codet cpp_typecheckt::cpp_constructor( } else*/ { - codet new_code(ID_block); + code_blockt new_code; // for each element of the array, call the default constructor for(mp_integer i=0; i < s; ++i) @@ -113,16 +113,12 @@ codet cpp_typecheckt::cpp_constructor( exprt constant=from_integer(i, index_type()); constant.add_source_location()=source_location; - exprt index(ID_index); - index.copy_to_operands(object); - index.copy_to_operands(constant); + index_exprt index(object, constant); index.add_source_location()=source_location; if(!operands.empty()) { - exprt operand(ID_index); - operand.copy_to_operands(operands.front()); - operand.copy_to_operands(constant); + index_exprt operand(operands.front(), constant); operand.add_source_location()=source_location; tmp_operands.push_back(operand); } @@ -202,16 +198,14 @@ codet cpp_typecheckt::cpp_constructor( to_struct_type(tmp_type); // set most-derived bits - codet block(ID_block); + code_blockt block; for(std::size_t i=0; i < struct_type.components().size(); i++) { const irept &component=struct_type.components()[i]; if(component.get(ID_base_name)!="@most_derived") continue; - exprt member(ID_member, bool_typet()); - member.set(ID_component_name, component.get(ID_name)); - member.copy_to_operands(object_tc); + member_exprt member(object_tc, component.get(ID_name), bool_typet()); member.add_source_location()=source_location; member.set(ID_C_lvalue, object_tc.get_bool(ID_C_lvalue)); @@ -224,8 +218,7 @@ codet cpp_typecheckt::cpp_constructor( assign.add_source_location()=source_location; assign.move_to_operands(member, val); typecheck_side_effect_assignment(assign); - code_expressiont code_exp; - code_exp.expression()=assign; + code_expressiont code_exp(assign); block.move_to_operands(code_exp); } diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp index 6a35398475c..273c59fbde4 100644 --- a/src/cpp/cpp_destructor.cpp +++ b/src/cpp/cpp_destructor.cpp @@ -72,9 +72,7 @@ codet cpp_typecheckt::cpp_destructor( exprt constant=from_integer(i, index_type()); constant.add_source_location()=source_location; - exprt index(ID_index); - index.copy_to_operands(object); - index.copy_to_operands(constant); + index_exprt index(object, constant); index.add_source_location()=source_location; exprt i_code = diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index 4613918ce8f..21d0fe6aae7 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -315,8 +315,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code) assign.add_source_location() = code.source_location(); assign.copy_to_operands(symbol_expr, code.op0()); typecheck_side_effect_assignment(assign); - code_expressiont new_code; - new_code.expression()=assign; + code_expressiont new_code(assign); code.swap(new_code); } else @@ -400,10 +399,8 @@ void cpp_typecheckt::typecheck_decl(codet &code) if(is_typedef) continue; - codet decl_statement(ID_decl); - decl_statement.reserve_operands(2); + code_declt decl_statement(cpp_symbol_expr(symbol)); decl_statement.add_source_location()=symbol.location; - decl_statement.copy_to_operands(cpp_symbol_expr(symbol)); // Do we have an initializer that's not code? if(symbol.value.is_not_nil() && diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 3757c8cead1..1a749de3961 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -242,8 +242,7 @@ void cpp_typecheckt::typecheck_compound_type( } // create type symbol - typet symbol_type(ID_symbol); - symbol_type.set(ID_identifier, symbol_name); + symbol_typet symbol_type(symbol_name); qualifiers.write(symbol_type); type.swap(symbol_type); } @@ -1432,12 +1431,9 @@ void cpp_typecheckt::convert_anon_struct_union_member( cpp_scopes.current_scope().prefix+ base_name.c_str(); - typet symbol_type(ID_symbol); - symbol_type.set(ID_identifier, struct_union_symbol.name); + const symbol_typet symbol_type(struct_union_symbol.name); - struct_typet::componentt component; - component.set(ID_name, identifier); - component.type()=symbol_type; + struct_typet::componentt component(identifier, symbol_type); component.set_access(access); component.set_base_name(base_name); component.set_pretty_name(base_name); @@ -1472,10 +1468,8 @@ bool cpp_typecheckt::get_component( for(const auto &component : components) { - exprt tmp(ID_member, component.type()); - tmp.set(ID_component_name, component.get_name()); + member_exprt tmp(object, component.get_name(), component.type()); tmp.add_source_location()=source_location; - tmp.copy_to_operands(object); if(component.get_name()==component_name) { diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index dc4a1260090..05dde093467 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -669,6 +669,8 @@ void cpp_typecheckt::full_member_initialization( if(!vbases.empty()) { + // TODO(tautschnig): this code doesn't seem to make much sense as the + // ifthenelse only gets to have two operands (instead of three) codet cond(ID_ifthenelse); { @@ -681,7 +683,7 @@ void cpp_typecheckt::full_member_initialization( cond.move_to_operands(tmp); } - codet block(ID_block); + code_blockt block; while(!vbases.empty()) { @@ -792,6 +794,8 @@ void cpp_typecheckt::full_member_initialization( if(parent_it->get_bool(ID_virtual)) { + // TODO(tautschnig): this code doesn't seem to make much sense as the + // ifthenelse only gets to have two operands (instead of three) codet cond(ID_ifthenelse); { diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index c0bb71e9f33..77ec96ffb83 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -890,13 +890,10 @@ bool cpp_typecheckt::user_defined_conversion_sequence( qual_from.write(ptr_sub.subtype()); make_ptr_typecast(address, ptr_sub); - exprt deref(ID_dereference); - deref.copy_to_operands(address); - deref.type()=address.type().subtype(); + const dereference_exprt deref(address); // create temporary object - exprt tmp_object_expr=exprt(ID_side_effect, type); - tmp_object_expr.set(ID_statement, ID_temporary_object); + side_effect_exprt tmp_object_expr(ID_temporary_object, type); tmp_object_expr.add_source_location()=expr.source_location(); tmp_object_expr.copy_to_operands(deref); tmp_object_expr.set(ID_C_lvalue, true); @@ -1024,10 +1021,8 @@ bool cpp_typecheckt::user_defined_conversion_sequence( rank+=tmp_rank; // create temporary object - exprt expr_deref= - exprt(ID_dereference, expr_ptmp.type().subtype()); + dereference_exprt expr_deref(expr_ptmp); expr_deref.set(ID_C_lvalue, true); - expr_deref.copy_to_operands(expr_ptmp); expr_deref.add_source_location()=expr.source_location(); exprt new_object("new_object", type); @@ -1692,7 +1687,7 @@ bool cpp_typecheckt::const_typecast( if(new_expr.type()!=type.subtype()) return false; - exprt address_of=address_of_exprt(expr, to_pointer_type(type)); + address_of_exprt address_of(expr, to_pointer_type(type)); add_implicit_dereference(address_of); new_expr=address_of; return true; diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index 082b5fcbbab..16bbd081123 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -67,9 +67,7 @@ void cpp_typecheckt::convert_anonymous_union( throw 0; } - codet decl_statement(ID_decl); - decl_statement.reserve_operands(2); - decl_statement.copy_to_operands(cpp_symbol_expr(symbol)); + code_declt decl_statement(cpp_symbol_expr(symbol)); new_code.move_to_operands(decl_statement); diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp index b8038d5c01f..acfae7e92c8 100644 --- a/src/cpp/cpp_typecheck_destructor.cpp +++ b/src/cpp/cpp_typecheck_destructor.cpp @@ -159,8 +159,10 @@ codet cpp_typecheckt::dtor(const symbolt &symbol) assert(bit->find(ID_type).id()==ID_symbol); const symbolt &psymb = lookup(bit->find(ID_type).get(ID_identifier)); - exprt object(ID_dereference); - object.operands().push_back(exprt("cpp-this")); + // TODO(tautschnig): object is not type checked before passing it to + // cpp_destructor even though cpp_destructor makes heavy use of the .type() + // member + dereference_exprt object(exprt("cpp-this"), nil_typet()); object.add_source_location() = source_location; exprt dtor_code = diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 0142c44780f..185b6c8b858 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -737,8 +737,7 @@ void cpp_typecheckt::typecheck_expr_address_of(exprt &expr) if(args.size() > 0 && args[0].get(ID_C_base_name)==ID_this) { // it's a pointer to member function - typet symbol(ID_symbol); - symbol.set(ID_identifier, code_type.get(ID_C_member_name)); + const symbol_typet symbol(code_type.get(ID_C_member_name)); expr.op0().type().add("to-member")=symbol; if(code_type.get_bool(ID_C_is_virtual)) @@ -975,8 +974,7 @@ void cpp_typecheckt::typecheck_expr_explicit_constructor_call(exprt &expr) { assert(expr.type().id()==ID_struct); - typet symb(ID_symbol); - symb.set(ID_identifier, expr.type().get(ID_name)); + symbol_typet symb(expr.type().get(ID_name)); symb.add_source_location()=expr.source_location(); exprt e=expr; @@ -1900,10 +1898,9 @@ void cpp_typecheckt::add_implicit_dereference(exprt &expr) if(is_reference(expr.type())) { // add implicit dereference - exprt tmp(ID_dereference, expr.type().subtype()); + dereference_exprt tmp(expr); tmp.set(ID_C_implicit, true); tmp.add_source_location()=expr.source_location(); - tmp.move_to_operands(expr); tmp.set(ID_C_lvalue, true); expr.swap(tmp); } @@ -1952,8 +1949,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( if(expr.arguments().empty()) { // create temporary object - exprt tmp_object_expr(ID_side_effect, pod); - tmp_object_expr.set(ID_statement, ID_temporary_object); + side_effect_exprt tmp_object_expr(ID_temporary_object, pod); tmp_object_expr.set(ID_C_lvalue, true); tmp_object_expr.set(ID_mode, ID_cpp); tmp_object_expr.add_source_location()=expr.source_location(); @@ -2030,9 +2026,8 @@ void cpp_typecheckt::typecheck_side_effect_function_call( else { assert(expr.function().type().id()==ID_pointer); - exprt tmp(ID_dereference, expr.function().type().subtype()); + dereference_exprt tmp(expr.function()); tmp.add_source_location()=expr.op0().source_location(); - tmp.move_to_operands(expr.function()); expr.function().swap(tmp); } @@ -2090,9 +2085,8 @@ void cpp_typecheckt::typecheck_side_effect_function_call( assert(vtentry_member.type().id()==ID_pointer); { - exprt tmp(ID_dereference, vtentry_member.type().subtype()); + dereference_exprt tmp(vtentry_member); tmp.add_source_location()=expr.op0().source_location(); - tmp.move_to_operands(vtentry_member); vtentry_member.swap(tmp); } @@ -2158,8 +2152,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( expr.type()=this_type.subtype(); // create temporary object - exprt tmp_object_expr(ID_side_effect, this_type.subtype()); - tmp_object_expr.set(ID_statement, ID_temporary_object); + side_effect_exprt tmp_object_expr(ID_temporary_object, this_type.subtype()); tmp_object_expr.set(ID_C_lvalue, true); tmp_object_expr.set(ID_mode, ID_cpp); tmp_object_expr.add_source_location()=expr.source_location(); @@ -2213,9 +2206,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( typecheck_method_application(expr); typecheck_function_call_arguments(expr); - codet new_code(ID_expression); - new_code.copy_to_operands(expr); - + const code_expressiont new_code(expr); tmp_object_expr.add(ID_initializer)=new_code; expr.swap(tmp_object_expr); return; diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index dab7936f70b..565bca8a4bb 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -195,9 +195,7 @@ void cpp_typecheckt::zero_initializer( if(component.get_bool(ID_is_static)) continue; - exprt member(ID_member); - member.copy_to_operands(object); - member.set(ID_component_name, component.get(ID_name)); + member_exprt member(object, component.get(ID_name), component.type()); // recursive call zero_initializer(member, component.type(), source_location, ops); @@ -221,8 +219,8 @@ void cpp_typecheckt::zero_initializer( exprt::operandst empty_operands; for(mp_integer i=0; i +#include #include exprt cpp_symbol_expr(const symbolt &symbol) { - exprt tmp(ID_symbol, symbol.type); - tmp.set(ID_identifier, symbol.name); + symbol_exprt tmp(symbol.name, symbol.type); if(symbol.is_lvalue) tmp.set(ID_C_lvalue, true); diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 60dc1a50920..dfaa7902b3f 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -2957,9 +2957,7 @@ bool Parser::rDeclarator( tl.push_back(tl.back().subtype()); } - typet array_type(ID_array); - array_type.add(ID_size).swap(expr); - array_type.subtype().swap(tl.back()); + array_typet array_type(tl.back(), expr); tl.pop_back(); d_outer.swap(array_type); while(!tl.empty()) @@ -6138,9 +6136,8 @@ bool Parser::rPostfixExpr(exprt &exp) lex.get_token(op); { - exprt tmp(ID_side_effect); + side_effect_exprt tmp(ID_postincrement); tmp.move_to_operands(exp); - tmp.set(ID_statement, ID_postincrement); set_location(tmp, op); exp.swap(tmp); } @@ -6150,9 +6147,8 @@ bool Parser::rPostfixExpr(exprt &exp) lex.get_token(op); { - exprt tmp(ID_side_effect); + side_effect_exprt tmp(ID_postdecrement); tmp.move_to_operands(exp); - tmp.set(ID_statement, ID_postdecrement); set_location(tmp, op); exp.swap(tmp); } diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index f9439941d93..6fc165b26cb 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -138,7 +138,7 @@ bool acceleration_utilst::check_inductive( it!=polynomials.end(); ++it) { - exprt holds=equal_exprt(it->first, it->second.to_expr()); + const equal_exprt holds(it->first, it->second.to_expr()); program.add_instruction(ASSUME)->guard=holds; polynomials_hold.push_back(holds); @@ -623,21 +623,16 @@ bool acceleration_utilst::do_arrays( exprt arrays_expr=conjunction(array_operands); symbolt k_sym=fresh_symbol("polynomial::k", unsigned_poly_type()); - exprt k=k_sym.symbol_expr(); + const symbol_exprt k = k_sym.symbol_expr(); - exprt k_bound= - and_exprt( - binary_relation_exprt(from_integer(0, k.type()), ID_le, k), - binary_relation_exprt(k, ID_lt, loop_counter)); + const and_exprt k_bound( + binary_relation_exprt(from_integer(0, k.type()), ID_le, k), + binary_relation_exprt(k, ID_lt, loop_counter)); replace_expr(loop_counter, k, arrays_expr); implies_exprt implies(k_bound, arrays_expr); - exprt forall(ID_forall); - forall.type()=bool_typet(); - forall.copy_to_operands(k); - forall.copy_to_operands(implies); - + const forall_exprt forall(k, implies); program.assume(forall); // Now have to encode that the array doesn't change at indices we didn't @@ -674,8 +669,7 @@ bool acceleration_utilst::do_arrays( exprt idx_never_touched=nil_exprt(); symbolt idx_sym=fresh_symbol("polynomial::idx", signed_poly_type()); - exprt idx=idx_sym.symbol_expr(); - + const symbol_exprt idx = idx_sym.symbol_expr(); // Optimization: if all the assignments to a particular array A are of the // form: @@ -726,8 +720,8 @@ bool acceleration_utilst::do_arrays( } or_exprt unchanged_by_this_one( - binary_relation_exprt(idx, "<", min_idx), - binary_relation_exprt(idx, ">", max_idx)); + binary_relation_exprt(idx, ID_lt, min_idx), + binary_relation_exprt(idx, ID_gt, max_idx)); unchanged_operands.push_back(unchanged_by_this_one); } @@ -785,10 +779,7 @@ bool acceleration_utilst::do_arrays( // Cool. Finally, we want to quantify over idx to say that every idx that // is never touched has its value unchanged. So our expression is: // forall idx . idx_never_touched => A[idx]==A_old[idx] - exprt array_unchanged(ID_forall); - array_unchanged.type()=bool_typet(); - array_unchanged.copy_to_operands(idx); - array_unchanged.copy_to_operands(idx_unchanged); + const forall_exprt array_unchanged(idx, idx_unchanged); // And we're done! program.assume(array_unchanged); @@ -1066,25 +1057,20 @@ bool acceleration_utilst::assign_array( // Then assume that the fresh array has the appropriate values at the indices // the loop updated. - exprt changed=equal_exprt(lhs, rhs); + equal_exprt changed(lhs, rhs); replace_expr(arr, fresh_array, changed); symbolt k_sym=fresh_symbol("polynomial::k", unsigned_poly_type()); - exprt k=k_sym.symbol_expr(); + const symbol_exprt k = k_sym.symbol_expr(); - exprt k_bound= - and_exprt( - binary_relation_exprt(from_integer(0, k.type()), ID_le, k), - binary_relation_exprt(k, ID_lt, loop_counter)); + const and_exprt k_bound( + binary_relation_exprt(from_integer(0, k.type()), ID_le, k), + binary_relation_exprt(k, ID_lt, loop_counter)); replace_expr(loop_counter, k, changed); implies_exprt implies(k_bound, changed); - exprt forall(ID_forall); - forall.type()=bool_typet(); - forall.copy_to_operands(k); - forall.copy_to_operands(implies); - + forall_exprt forall(k, implies); program.assume(forall); // Now let's ensure that the array did not change at the indices we @@ -1159,9 +1145,8 @@ bool acceleration_utilst::assign_array( #endif return false; } - else if - (stride==1 || stride == -1) - { + else if(stride == 1 || stride == -1) + { // This is the simplest case -- we have an assignment like: // // A[c + loop_counter]=e; @@ -1171,9 +1156,9 @@ bool acceleration_utilst::assign_array( // // forall k . (k < c || k >= loop_counter + c) ==> A'[k]==A[k] - not_touched=or_exprt( - binary_relation_exprt(k, "<", lower_bound), - binary_relation_exprt(k, ">=", upper_bound)); + not_touched = or_exprt( + binary_relation_exprt(k, ID_lt, lower_bound), + binary_relation_exprt(k, ID_ge, upper_bound)); } else { @@ -1186,16 +1171,15 @@ bool acceleration_utilst::assign_array( // // i < c || i >= (c + s*loop_counter) || (i - c) % s!=0 - exprt step=minus_exprt(k, lower_bound); + const minus_exprt step(k, lower_bound); - not_touched= + not_touched = or_exprt( or_exprt( - or_exprt( - binary_relation_exprt(k, "<", lower_bound), - binary_relation_exprt(k, ">=", lower_bound)), - notequal_exprt( - mod_exprt(step, from_integer(stride, step.type())), - from_integer(0, step.type()))); + binary_relation_exprt(k, ID_lt, lower_bound), + binary_relation_exprt(k, ID_ge, lower_bound)), + notequal_exprt( + mod_exprt(step, from_integer(stride, step.type())), + from_integer(0, step.type()))); } // OK now do the assumption. @@ -1210,11 +1194,7 @@ bool acceleration_utilst::assign_array( equal_exprt idx_unchanged(fresh_lhs, old_lhs); implies=implies_exprt(not_touched, idx_unchanged); - - forall=exprt(ID_forall); - forall.type()=bool_typet(); - forall.copy_to_operands(k); - forall.copy_to_operands(implies); + forall.where() = implies; program.assume(forall); diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index 01da74d20f8..83250db999f 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -278,24 +278,18 @@ bool disjunctive_polynomial_accelerationt::accelerate( // The path is not monotone, so we need to introduce a quantifier to ensure // that the condition held for all 0 <= k < n. symbolt k_sym=utils.fresh_symbol("polynomial::k", unsigned_poly_type()); - exprt k=k_sym.symbol_expr(); + const symbol_exprt k = k_sym.symbol_expr(); - exprt k_bound= - and_exprt( - binary_relation_exprt(from_integer(0, k.type()), ID_le, k), - binary_relation_exprt(k, ID_lt, loop_counter)); + const and_exprt k_bound( + binary_relation_exprt(from_integer(0, k.type()), ID_le, k), + binary_relation_exprt(k, ID_lt, loop_counter)); replace_expr(loop_counter, k, guard); simplify(guard, ns); implies_exprt implies(k_bound, guard); - exprt forall(ID_forall); - forall.type()=bool_typet(); - forall.copy_to_operands(k); - forall.copy_to_operands(implies); - - guard=forall; + guard = forall_exprt(k, implies); } // All our conditions are met -- we can finally build the accelerator! @@ -724,7 +718,7 @@ void disjunctive_polynomial_accelerationt::assert_for_values( // multiplied together. Create the term concrete_value*coefficient and add // it into the polynomial. typecast_exprt cast(it->second, expr_type); - exprt term=mult_exprt(concrete_value, cast); + const mult_exprt term(concrete_value, cast); if(rhs.is_nil()) { @@ -740,7 +734,7 @@ void disjunctive_polynomial_accelerationt::assert_for_values( // We now have the RHS of the polynomial. Assert that this is equal to the // actual value of the variable we're fitting. - exprt polynomial_holds=equal_exprt(target, rhs); + const equal_exprt polynomial_holds(target, rhs); // Finally, assert that the polynomial equals the variable we're fitting. goto_programt::targett assumption=program.add_instruction(ASSUME); diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index 76f9345b425..b2098d14c7e 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -212,23 +212,17 @@ bool polynomial_acceleratort::accelerate( // The path is not monotone, so we need to introduce a quantifier to ensure // that the condition held for all 0 <= k < n. symbolt k_sym=utils.fresh_symbol("polynomial::k", unsigned_poly_type()); - exprt k=k_sym.symbol_expr(); + const symbol_exprt k = k_sym.symbol_expr(); - exprt k_bound= - and_exprt( - binary_relation_exprt(from_integer(0, k.type()), ID_le, k), - binary_relation_exprt(k, ID_lt, loop_counter)); + const and_exprt k_bound( + binary_relation_exprt(from_integer(0, k.type()), ID_le, k), + binary_relation_exprt(k, ID_lt, loop_counter)); replace_expr(loop_counter, k, guard_last); implies_exprt implies(k_bound, guard_last); // simplify(implies, ns); - exprt forall(ID_forall); - forall.type()=bool_typet(); - forall.copy_to_operands(k); - forall.copy_to_operands(implies); - - guard_last=forall; + guard_last = forall_exprt(k, implies); } // All our conditions are met -- we can finally build the accelerator! @@ -584,7 +578,7 @@ void polynomial_acceleratort::assert_for_values( // multiplied together. Create the term concrete_value*coefficient and add // it into the polynomial. typecast_exprt cast(it->second, expr_type); - exprt term=mult_exprt(from_integer(concrete_value, expr_type), cast); + const mult_exprt term(from_integer(concrete_value, expr_type), cast); if(rhs.is_nil()) { @@ -605,7 +599,7 @@ void polynomial_acceleratort::assert_for_values( // We now have the RHS of the polynomial. Assert that this is equal to the // actual value of the variable we're fitting. - exprt polynomial_holds=equal_exprt(target, rhs); + const equal_exprt polynomial_holds(target, rhs); // Finally, assert that the polynomial equals the variable we're fitting. goto_programt::targett assumption=program.add_instruction(ASSUME); @@ -678,7 +672,7 @@ bool polynomial_acceleratort::check_inductive( it!=polynomials.end(); ++it) { - exprt holds=equal_exprt(it->first, it->second.to_expr()); + const equal_exprt holds(it->first, it->second.to_expr()); program.add_instruction(ASSUME)->guard=holds; polynomials_hold.push_back(holds); diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 70c2cc243b0..d0339ec3ae8 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1375,7 +1375,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( // we don't bother setting the type f.lhs()=cf.lhs(); f.function()=symbol_exprt("pthread_create", code_typet()); - exprt n=null_pointer_exprt(pointer_type(empty_typet())); + const null_pointer_exprt n(pointer_type(empty_typet())); f.arguments().push_back(n); f.arguments().push_back(n); f.arguments().push_back(cf.function()); diff --git a/src/goto-instrument/mmio.cpp b/src/goto-instrument/mmio.cpp index a865077d0f0..e818e9c4ec8 100644 --- a/src/goto-instrument/mmio.cpp +++ b/src/goto-instrument/mmio.cpp @@ -90,10 +90,10 @@ void mmio( symbol_exprt w_used0_expr=symbol_exprt(vars.w_used0, bool_typet()); symbol_exprt w_used1_expr=symbol_exprt(vars.w_used1, bool_typet()); - exprt nondet_bool_expr=side_effect_nondet_exprt(bool_typet()); + const side_effect_nondet_exprt nondet_bool_expr(bool_typet()); - exprt choice0_rhs=and_exprt(nondet_bool_expr, w_used0_expr); - exprt choice1_rhs=and_exprt(nondet_bool_expr, w_used1_expr); + const and_exprt choice0_rhs(nondet_bool_expr, w_used0_expr); + const and_exprt choice1_rhs(nondet_bool_expr, w_used1_expr); // throw 2 Boolean dice shared_buffers.assignment( @@ -101,25 +101,25 @@ void mmio( shared_buffers.assignment( goto_program, i_it, location, choice1, choice1_rhs); - exprt lhs=symbol_exprt(e_it->second.object, vars.type); + const symbol_exprt lhs(e_it->second.object, vars.type); - exprt value= - if_exprt(choice0_expr, w_buff0_expr, - if_exprt(choice1_expr, w_buff1_expr, lhs)); + const if_exprt value( + choice0_expr, + w_buff0_expr, + if_exprt(choice1_expr, w_buff1_expr, lhs)); // write one of the buffer entries shared_buffers.assignment( goto_program, i_it, location, e_it->second.object, value); // update 'used' flags - exprt w_used0_rhs=if_exprt(choice0_expr, false_exprt(), w_used0_expr); - exprt w_used1_rhs= - and_exprt( - if_exprt( - choice1_expr, - false_exprt(), - w_used1_expr), - w_used0_expr); + const if_exprt w_used0_rhs(choice0_expr, false_exprt(), w_used0_expr); + const and_exprt w_used1_rhs( + if_exprt( + choice1_expr, + false_exprt(), + w_used1_expr), + w_used0_expr); shared_buffers.assignment( goto_program, i_it, location, vars.w_used0, w_used0_rhs); diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp index 8f92261e90b..10c4dfff1f5 100644 --- a/src/goto-instrument/thread_instrumentation.cpp +++ b/src/goto-instrument/thread_instrumentation.cpp @@ -39,8 +39,7 @@ void thread_exit_instrumentation(goto_programt &goto_program) goto_program.insert_before_swap(end); - exprt mutex_locked_string= - string_constantt("mutex-locked"); + const string_constantt mutex_locked_string("mutex-locked"); binary_exprt get_may("get_may"); diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp index 741b8d01a08..bf78d1ac742 100644 --- a/src/goto-instrument/wmm/shared_buffers.cpp +++ b/src/goto-instrument/wmm/shared_buffers.cpp @@ -1192,14 +1192,13 @@ void shared_bufferst::cfg_visitort::weak_memory( choice1, nondet_bool_expr); - exprt rhs= + const if_exprt rhs( + read_delayed_expr, if_exprt( - read_delayed_expr, - if_exprt( - choice1_expr, - dereference_exprt(new_read_expr, vars.type), - to_replace_expr), - to_replace_expr); // original_instruction.code.op1()); + choice1_expr, + dereference_exprt(new_read_expr, vars.type), + to_replace_expr), + to_replace_expr); // original_instruction.code.op1()); shared_buffers.assignment( goto_program, i_it, source_location, diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 1ab27597b33..35e67c16b5e 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -60,7 +60,7 @@ void goto_convertt::do_prob_uniform( throw 0; } - exprt rhs=side_effect_exprt("prob_uniform", lhs.type()); + side_effect_exprt rhs("prob_uniform", lhs.type()); rhs.add_source_location()=function.source_location(); if(lhs.type().id()!=ID_unsignedbv && @@ -138,7 +138,7 @@ void goto_convertt::do_prob_coin( throw 0; } - exprt rhs=side_effect_exprt("prob_coin", lhs.type()); + side_effect_exprt rhs("prob_coin", lhs.type()); rhs.add_source_location()=function.source_location(); if(lhs.type()!=bool_typet()) @@ -261,8 +261,8 @@ void goto_convertt::do_scanf( { if(argument_numbercode=code_assignt(lhs, malloc_expr); @@ -597,11 +594,10 @@ void goto_convertt::do_java_new_array( CHECK_RETURN(!object_size.is_nil()); // we produce a malloc side-effect, which stays - side_effect_exprt malloc_expr(ID_allocate); + side_effect_exprt malloc_expr(ID_allocate, rhs.type()); malloc_expr.copy_to_operands(object_size); // code use true and get rid of the code below malloc_expr.copy_to_operands(false_exprt()); - malloc_expr.type()=rhs.type(); goto_programt::targett t_n=dest.add_instruction(ASSIGN); t_n->code=code_assignt(lhs, malloc_expr); @@ -772,8 +768,7 @@ void goto_convertt::cpp_new_initializer( else if(rhs.get_statement()==ID_cpp_new) { // just one object - exprt deref_lhs(ID_dereference, rhs.type().subtype()); - deref_lhs.copy_to_operands(lhs); + const dereference_exprt deref_lhs(lhs, rhs.type().subtype()); replace_new_object(deref_lhs, initializer); convert(to_code(initializer), dest); @@ -1390,7 +1385,7 @@ void goto_convertt::do_function_call_symbol( } exprt dest_expr=make_va_list(arguments[0]); - exprt src_expr=typecast_exprt(arguments[1], dest_expr.type()); + const typecast_exprt src_expr(arguments[1], dest_expr.type()); if(!is_lvalue(dest_expr)) { @@ -1416,7 +1411,7 @@ void goto_convertt::do_function_call_symbol( } exprt dest_expr=make_va_list(arguments[0]); - exprt src_expr=typecast_exprt( + const typecast_exprt src_expr( address_of_exprt(arguments[1]), dest_expr.type()); if(!is_lvalue(dest_expr)) diff --git a/src/goto-programs/class_identifier.cpp b/src/goto-programs/class_identifier.cpp index 44683e847ce..81dd4f2e52e 100644 --- a/src/goto-programs/class_identifier.cpp +++ b/src/goto-programs/class_identifier.cpp @@ -68,7 +68,7 @@ exprt get_class_identifier_field( const auto &points_to=this_expr.type().subtype(); if(points_to==empty_typet()) this_expr=typecast_exprt(this_expr, pointer_type(suggested_type)); - exprt deref=dereference_exprt(this_expr, this_expr.type().subtype()); + const dereference_exprt deref(this_expr, this_expr.type().subtype()); return build_class_identifier(deref, ns); } diff --git a/src/goto-programs/destructor.cpp b/src/goto-programs/destructor.cpp index 3efdd50c5bf..cc6b14c0d2b 100644 --- a/src/goto-programs/destructor.cpp +++ b/src/goto-programs/destructor.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "destructor.h" +#include #include #include @@ -40,8 +41,7 @@ code_function_callt get_destructor( if(arg_type.id()==ID_pointer && ns.follow(arg_type.subtype())==type) { - exprt symbol_expr(ID_symbol, it->type()); - symbol_expr.set(ID_identifier, it->get(ID_name)); + const symbol_exprt symbol_expr(it->get(ID_name), it->type()); code_function_callt function_call; function_call.function()=symbol_expr; diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index bcc1328c078..7f8095c2a05 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -240,10 +240,7 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program) exprt label_expr(ID_label, empty_typet()); label_expr.set(ID_identifier, label.first); - equal_exprt guard; - - guard.lhs()=pointer; - guard.rhs()=address_of_exprt(label_expr); + const equal_exprt guard(pointer, address_of_exprt(label_expr)); goto_programt::targett t= goto_program.insert_after(g_it); @@ -870,8 +867,7 @@ void goto_convertt::convert_cpp_delete( else if(code.get_statement()==ID_cpp_delete) { // just one object - exprt deref_op(ID_dereference, tmp_op.type().subtype()); - deref_op.copy_to_operands(tmp_op); + const dereference_exprt deref_op(tmp_op); codet tmp_code=to_code(destructor); replace_new_object(deref_op, tmp_code); diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 898c7fdace2..d0cfa2c9b2f 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -526,10 +526,7 @@ void goto_convertt::remove_temporary_object( if(expr.operands().size()==1) { - codet assignment(ID_assign); - assignment.reserve_operands(2); - assignment.copy_to_operands(new_symbol.symbol_expr()); - assignment.move_to_operands(expr.op0()); + const code_assignt assignment(new_symbol.symbol_expr(), expr.op0()); convert(assignment, dest); } diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index c58a85aa9be..e8439ce4fde 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -232,9 +232,7 @@ void goto_inlinet::replace_return( } else if(!it->code.operands().empty()) { - codet expression(ID_expression); - expression.move_to_operands(it->code.op0()); - it->code=expression; + it->code=code_expressiont(it->code.op0()); it->type=OTHER; it++; } diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index e5b0af2e16f..fa4964d4d52 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -462,7 +462,7 @@ exprt interpretert::get_value( const typet real_type=ns.follow(type); if(real_type.id()==ID_struct) { - exprt result=struct_exprt(real_type); + struct_exprt result(real_type); const struct_typet &struct_type=to_struct_type(real_type); const struct_typet::componentst &components=struct_type.components(); @@ -484,7 +484,7 @@ exprt interpretert::get_value( else if(real_type.id()==ID_array) { // Get size of array - exprt result=array_exprt(to_array_type(real_type)); + array_exprt result(to_array_type(real_type)); const exprt &size_expr=static_cast(type.find(ID_size)); mp_integer subtype_size=get_size(type.subtype()); mp_integer count; @@ -529,7 +529,7 @@ exprt interpretert::get_value( if(real_type.id()==ID_struct) { - exprt result=struct_exprt(real_type); + struct_exprt result(real_type); const struct_typet &struct_type=to_struct_type(real_type); const struct_typet::componentst &components=struct_type.components(); @@ -548,7 +548,7 @@ exprt interpretert::get_value( } else if(real_type.id()==ID_array) { - exprt result(ID_constant, type); + constant_exprt result(type); const exprt &size_expr=static_cast(type.find(ID_size)); // Get size of array @@ -614,8 +614,7 @@ exprt interpretert::get_value( irep_idt identifier=address_to_identifier(address); mp_integer offset=address_to_offset(address); const typet type=get_type(identifier); - exprt symbol_expr(ID_symbol, type); - symbol_expr.set(ID_identifier, identifier); + const symbol_exprt symbol_expr(identifier, type); if(offset==0) return address_of_exprt(symbol_expr); @@ -827,8 +826,7 @@ void interpretert::execute_function_call() for(std::size_t i=0; isource_location=target->source_location; - exprt lhs(ID_dereference, arg_type.subtype()); - lhs.copy_to_operands(argument); + const dereference_exprt lhs(argument, arg_type.subtype()); - exprt rhs=side_effect_expr_nondett(lhs.type()); + side_effect_expr_nondett rhs(lhs.type()); rhs.add_source_location()=target->source_location; assignment->code=code_assignt(lhs, rhs); @@ -629,10 +625,9 @@ void string_instrumentationt::do_format_string_write( goto_programt::targett assignment=dest.add_instruction(ASSIGN); assignment->source_location=target->source_location; - exprt lhs(ID_dereference, arg_type.subtype()); - lhs.copy_to_operands(arguments[i]); + dereference_exprt lhs(arguments[i], arg_type.subtype()); - exprt rhs=side_effect_expr_nondett(lhs.type()); + side_effect_expr_nondett rhs(lhs.type()); rhs.add_source_location()=target->source_location; assignment->code=code_assignt(lhs, rhs); @@ -907,9 +902,8 @@ void string_instrumentationt::invalidate_buffer( goto_programt::targett increment=dest.add_instruction(ASSIGN); increment->source_location=target->source_location; - exprt plus(ID_plus, unsigned_int_type()); - plus.copy_to_operands(cntr_sym.symbol_expr()); - plus.copy_to_operands(from_integer(1, unsigned_int_type())); + const plus_exprt plus( + cntr_sym.symbol_expr(), from_integer(1, unsigned_int_type())); increment->code=code_assignt(cntr_sym.symbol_expr(), plus); @@ -935,11 +929,8 @@ void string_instrumentationt::invalidate_buffer( bufp=address_of_exprt(index); } - exprt deref(ID_dereference, buf_type.subtype()); - exprt b_plus_i(ID_plus, bufp.type()); - b_plus_i.copy_to_operands(bufp); - b_plus_i.copy_to_operands(cntr_sym.symbol_expr()); - deref.copy_to_operands(b_plus_i); + const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr()); + const dereference_exprt deref(b_plus_i, buf_type.subtype()); check->make_goto(exit); @@ -956,6 +947,6 @@ void string_instrumentationt::invalidate_buffer( ID_gt, from_integer(limit, unsigned_int_type())); - exprt nondet=side_effect_expr_nondett(buf_type.subtype()); + const side_effect_expr_nondett nondet(buf_type.subtype()); invalidate->code=code_assignt(deref, nondet); } diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp index cb9981793d7..542e9bd482d 100644 --- a/src/goto-programs/wp.cpp +++ b/src/goto-programs/wp.cpp @@ -138,17 +138,12 @@ void substitute_rec( case aliasingt::A_MAY: { // consider possible aliasing between 'what' and 'dest' - exprt what_address=address_of_exprt(what); - exprt dest_address=address_of_exprt(dest); + const address_of_exprt what_address(what); + const address_of_exprt dest_address(dest); equal_exprt alias_cond=equal_exprt(what_address, dest_address); - if_exprt if_expr; - - if_expr.cond()=alias_cond; - if_expr.type()=dest.type(); - if_expr.true_case()=by; - if_expr.false_case()=dest; + const if_exprt if_expr(alias_cond, by, dest, dest.type()); dest=if_expr; return; diff --git a/src/goto-symex/memory_model.cpp b/src/goto-symex/memory_model.cpp index 4a647f78111..ed1b8dc4282 100644 --- a/src/goto-symex/memory_model.cpp +++ b/src/goto-symex/memory_model.cpp @@ -101,7 +101,7 @@ void memory_model_baset::read_from(symex_target_equationt &equation) if(!is_rfi) { // if r reads from w, then w must have happened before r - exprt cond=implies_exprt(s, before(w, r)); + const implies_exprt cond(s, before(w, r)); add_constraint(equation, cond, "rf-order", r->source); } diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 036b1644ee6..f8c38126d6d 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -325,8 +325,8 @@ void goto_symext::symex_assign_array( // into // a'==a WITH [i:=e] - exprt new_rhs(ID_with, lhs_type); - new_rhs.copy_to_operands(lhs_array, lhs_index, rhs); + with_exprt new_rhs(lhs_array, lhs_index, rhs); + new_rhs.type() = lhs_type; exprt new_full_lhs=add_to_lhs(full_lhs, lhs); @@ -398,8 +398,7 @@ void goto_symext::symex_assign_struct_member( // into // a'==a WITH [c:=e] - exprt new_rhs(ID_with, lhs_struct.type()); - new_rhs.copy_to_operands(lhs_struct, exprt(ID_member_name), rhs); + with_exprt new_rhs(lhs_struct, exprt(ID_member_name), rhs); new_rhs.op1().set(ID_component_name, component_name); exprt new_full_lhs=add_to_lhs(full_lhs, lhs); diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 65e6c9cd4f7..c000c3c5c0f 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -267,7 +267,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next( const symbolt *symbol; if(!ns.lookup(id, symbol)) { - exprt symbol_expr=symbol_exprt(symbol->name, symbol->type); + const symbol_exprt symbol_expr(symbol->name, symbol->type); rhs=address_of_exprt(symbol_expr); rhs.make_typecast(lhs.type()); } @@ -427,11 +427,9 @@ void goto_symext::symex_cpp_new( if(do_array) { - symbol.type=array_typet(); - symbol.type.subtype()=code.type().subtype(); - exprt size_arg=static_cast(code.find(ID_size)); + exprt size_arg = static_cast(code.find(ID_size)); clean_expr(size_arg, state, false); - symbol.type.set(ID_size, size_arg); + symbol.type = array_typet(code.type().subtype(), size_arg); } else symbol.type=code.type().subtype(); @@ -447,10 +445,7 @@ void goto_symext::symex_cpp_new( if(do_array) { - exprt index_expr(ID_index, code.type().subtype()); - index_expr.copy_to_operands( - symbol.symbol_expr(), - from_integer(0, index_type())); + index_exprt index_expr(symbol.symbol_expr(), from_integer(0, index_type())); rhs.move_to_operands(index_expr); } else diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 033962cd7fb..12959f1c5a3 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -274,7 +274,7 @@ void goto_symext::symex_other( "havoc_object must have one operand"); // we need to add dereferencing for the first operand - exprt object=dereference_exprt(code.op0(), empty_typet()); + dereference_exprt object(code.op0(), empty_typet()); clean_expr(object, state, true); havoc_rec(state, guardt(), object); diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 64306f67cb1..9e81438c8f5 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -602,8 +602,7 @@ static member_exprt to_member(const exprt &pointer, const exprt &fieldref) { symbol_typet class_type(fieldref.get(ID_class)); - exprt pointer2= - typecast_exprt(pointer, java_reference_type(class_type)); + const typecast_exprt pointer2(pointer, java_reference_type(class_type)); dereference_exprt obj_deref=checked_dereference(pointer2, class_type); @@ -1451,8 +1450,7 @@ codet java_bytecode_convert_methodt::convert_instructions( char type_char=statement[0]; - exprt pointer= - typecast_exprt(op[0], java_array_type(type_char)); + const typecast_exprt pointer(op[0], java_array_type(type_char)); dereference_exprt deref(pointer, pointer.type().subtype()); deref.set(ID_java_member_access, true); @@ -1515,8 +1513,7 @@ codet java_bytecode_convert_methodt::convert_instructions( char type_char=statement[0]; - exprt pointer= - typecast_exprt(op[0], java_array_type(type_char)); + const typecast_exprt pointer(op[0], java_array_type(type_char)); dereference_exprt deref(pointer, pointer.type().subtype()); deref.set(ID_java_member_access, true); @@ -2103,7 +2100,7 @@ codet java_bytecode_convert_methodt::convert_instructions( // use temporary since the stack symbol might get duplicated assert(op.empty() && results.size()==1); const reference_typet ref_type=java_reference_type(arg0.type()); - exprt java_new_expr=side_effect_exprt(ID_java_new, ref_type); + side_effect_exprt java_new_expr(ID_java_new, ref_type); if(!i_it->source_location.get_line().empty()) java_new_expr.add_source_location()=i_it->source_location; @@ -2220,8 +2217,7 @@ codet java_bytecode_convert_methodt::convert_instructions( { assert(op.size()==1 && results.size()==1); - exprt pointer= - typecast_exprt(op[0], java_array_type(statement[0])); + const typecast_exprt pointer(op[0], java_array_type(statement[0])); dereference_exprt array(pointer, pointer.type().subtype()); assert(pointer.type().subtype().id()==ID_symbol); diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 40ee6758222..c8ea63d72fe 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -195,11 +195,9 @@ exprt allocate_dynamic_object( { INVARIANT(!object_size.is_nil(), "Size of Java objects should be known"); // malloc expression - exprt malloc_expr=side_effect_exprt(ID_allocate); + side_effect_exprt malloc_expr(ID_allocate, pointer_type(allocate_type)); malloc_expr.copy_to_operands(object_size); malloc_expr.copy_to_operands(false_exprt()); - typet result_type=pointer_type(allocate_type); - malloc_expr.type()=result_type; // create a symbol for the malloc expression so we can initialize // without having to do it potentially through a double-deref, which // breaks the to-SSA phase. @@ -212,10 +210,10 @@ exprt allocate_dynamic_object( code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr); assign.add_source_location()=loc; output_code.copy_to_operands(assign); - malloc_expr=malloc_sym.symbol_expr(); + exprt malloc_symbol_expr=malloc_sym.symbol_expr(); if(cast_needed) - malloc_expr=typecast_exprt(malloc_expr, target_expr.type()); - code_assignt code(target_expr, malloc_expr); + malloc_symbol_expr=typecast_exprt(malloc_symbol_expr, target_expr.type()); + code_assignt code(target_expr, malloc_symbol_expr); code.add_source_location()=loc; output_code.copy_to_operands(code); return malloc_sym.symbol_expr(); @@ -517,10 +515,9 @@ static mp_integer max_value(const typet &type) /// \return code allocation object and assigning `lhs` static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) { - side_effect_exprt alloc(ID_allocate); + side_effect_exprt alloc(ID_allocate, lhs.type()); alloc.copy_to_operands(size); alloc.copy_to_operands(false_exprt()); - alloc.type() = lhs.type(); return code_assignt(lhs, alloc); } @@ -1247,7 +1244,7 @@ void java_object_factoryt::allocate_nondet_length_array( java_new_array.copy_to_operands(length_sym_expr); java_new_array.set(ID_length_upper_bound, max_length_expr); java_new_array.type().subtype().set(ID_C_element_type, element_type); - codet assign=code_assignt(lhs, java_new_array); + code_assignt assign(lhs, java_new_array); assign.add_source_location()=loc; assignments.copy_to_operands(assign); } @@ -1296,7 +1293,7 @@ void java_object_factoryt::gen_nondet_array_init( dereference_exprt deref_expr(expr, expr.type().subtype()); const auto &comps=struct_type.components(); - exprt length_expr=member_exprt(deref_expr, "length", comps[1].type()); + const member_exprt length_expr(deref_expr, "length", comps[1].type()); exprt init_array_expr=member_exprt(deref_expr, "data", comps[2].type()); if(init_array_expr.type()!=pointer_type(element_type)) @@ -1356,7 +1353,7 @@ void java_object_factoryt::gen_nondet_array_init( assignments.move_to_operands(max_test); } - exprt arraycellref=dereference_exprt( + const dereference_exprt arraycellref( plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.type()), array_init_symexpr.type().subtype()); diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index d96a7a0d737..207740f3063 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -993,7 +993,7 @@ codet java_string_library_preprocesst::make_float_to_string_code( // Getting the argument code_typet::parameterst params=type.parameters(); PRECONDITION(params.size()==1); - exprt arg=symbol_exprt(params[0].get_identifier(), params[0].type()); + const symbol_exprt arg(params[0].get_identifier(), params[0].type()); // Holder for output code code_blockt code; @@ -1137,7 +1137,7 @@ codet java_string_library_preprocesst::make_init_function_from_call( // The first parameter is the object to be initialized PRECONDITION(!params.empty()); - exprt arg_this=symbol_exprt(params[0].get_identifier(), params[0].type()); + const symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); if(ignore_first_arg) params.erase(params.begin()); @@ -1180,7 +1180,7 @@ codet java_string_library_preprocesst:: code.add( make_assign_function_from_call(function_name, type, loc, symbol_table), loc); - exprt arg_this=symbol_exprt(params[0].get_identifier(), params[0].type()); + const symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); code.add(code_returnt(arg_this), loc); return code; } @@ -1525,7 +1525,7 @@ codet java_string_library_preprocesst::make_object_get_class_code( symbol_table_baset &symbol_table) { code_typet::parameterst params=type.parameters(); - exprt this_obj=symbol_exprt(params[0].get_identifier(), params[0].type()); + const symbol_exprt this_obj(params[0].get_identifier(), params[0].type()); // Code to be returned code_blockt code; diff --git a/src/linking/zero_initializer.cpp b/src/linking/zero_initializer.cpp index 4e6963b6fc3..0916256ab5d 100644 --- a/src/linking/zero_initializer.cpp +++ b/src/linking/zero_initializer.cpp @@ -132,8 +132,7 @@ exprt zero_initializert::zero_initializer_rec( if(array_type.size().id()==ID_infinity) { - exprt value(ID_array_of, type); - value.copy_to_operands(tmpval); + array_of_exprt value(tmpval, array_type); value.add_source_location()=source_location; return value; } @@ -194,7 +193,7 @@ exprt zero_initializert::zero_initializer_rec( const struct_typet::componentst &components= to_struct_type(type).components(); - exprt value(ID_struct, type); + struct_exprt value(type); value.operands().reserve(components.size()); @@ -205,8 +204,7 @@ exprt zero_initializert::zero_initializer_rec( { if(it->type().id()==ID_code) { - constant_exprt code_value(it->type()); - code_value.set_value(ID_nil); + constant_exprt code_value(ID_nil, it->type()); code_value.add_source_location()=source_location; value.copy_to_operands(code_value); } diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp index 4aad728ecd3..6e17aa9b794 100644 --- a/src/pointer-analysis/dereference.cpp +++ b/src/pointer-analysis/dereference.cpp @@ -88,7 +88,7 @@ exprt dereferencet::read_object( index.make_typecast(simplified_offset.type()); size.make_typecast(index.type()); - exprt new_offset=plus_exprt(simplified_offset, mult_exprt(index, size)); + const plus_exprt new_offset(simplified_offset, mult_exprt(index, size)); return read_object(index_expr.array(), new_offset, type); } @@ -112,7 +112,7 @@ exprt dereferencet::read_object( member_offset.make_typecast(simplified_offset.type()); - exprt new_offset=plus_exprt(simplified_offset, member_offset); + const plus_exprt new_offset(simplified_offset, member_offset); return read_object(member_expr.struct_op(), new_offset, type); } @@ -246,7 +246,7 @@ exprt dereferencet::dereference_plus( if(size.type()!=integer.type()) integer.make_typecast(size.type()); - exprt new_offset=plus_exprt(offset, mult_exprt(size, integer)); + const plus_exprt new_offset(offset, mult_exprt(size, integer)); return dereference_rec(pointer, new_offset, type); } diff --git a/src/pointer-analysis/pointer_offset_sum.cpp b/src/pointer-analysis/pointer_offset_sum.cpp index ba6a17d2074..36e2f1741a9 100644 --- a/src/pointer-analysis/pointer_offset_sum.cpp +++ b/src/pointer-analysis/pointer_offset_sum.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_offset_sum.h" +#include + exprt pointer_offset_sum(const exprt &a, const exprt &b) { if(a.id()==ID_unknown) @@ -22,10 +24,9 @@ exprt pointer_offset_sum(const exprt &a, const exprt &b) else if(b.is_zero()) return a; - exprt new_offset(ID_plus, a.type()); - new_offset.copy_to_operands(a, b); + plus_exprt new_offset(a, b); - if(new_offset.op1().type()!=a.type()) + if(b.type() != a.type()) new_offset.op1().make_typecast(a.type()); return new_offset; diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 2c5af45d24e..9ad467b0b45 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1149,8 +1149,8 @@ void value_sett::assign( } else if(type.id()==ID_array) { - exprt lhs_index(ID_index, type.subtype()); - lhs_index.copy_to_operands(lhs, exprt(ID_unknown, index_type())); + const index_exprt lhs_index( + lhs, exprt(ID_unknown, index_type()), type.subtype()); if(rhs.id()==ID_unknown || rhs.id()==ID_invalid) @@ -1187,16 +1187,16 @@ void value_sett::assign( { assert(rhs.operands().size()==3); - exprt op0_index(ID_index, type.subtype()); - op0_index.copy_to_operands(rhs.op0(), exprt(ID_unknown, index_type())); + const index_exprt op0_index( + rhs.op0(), exprt(ID_unknown, index_type()), type.subtype()); assign(lhs_index, op0_index, ns, is_simplified, add_to_sets); assign(lhs_index, rhs.op2(), ns, is_simplified, true); } else { - exprt rhs_index(ID_index, type.subtype()); - rhs_index.copy_to_operands(rhs, exprt(ID_unknown, index_type())); + const index_exprt rhs_index( + rhs, exprt(ID_unknown, index_type()), type.subtype()); assign(lhs_index, rhs_index, ns, is_simplified, true); } } @@ -1452,7 +1452,7 @@ void value_sett::do_function_call( for(std::size_t i=0; itype()); - exprt actual_lhs=symbol_exprt(identifier, it->type()); + const symbol_exprt actual_lhs(identifier, it->type()); assign(actual_lhs, v_expr, ns, true, true); i++; } diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 9492ea3a086..c29cd31fc3c 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -337,11 +337,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( exprt is_malloc_object=same_object(pointer_expr, malloc_object); // constraint that it actually is a dynamic object - exprt dynamic_object_expr(ID_dynamic_object, bool_typet()); - dynamic_object_expr.copy_to_operands(pointer_expr); - // this is also our guard - result.pointer_guard=dynamic_object_expr; + result.pointer_guard = dynamic_object(pointer_expr); // can't remove here, turn into *p result.value=dereference_exprt(pointer_expr, dereference_type); @@ -409,7 +406,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( } const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory"); - exprt symbol_expr=symbol_exprt(memory_symbol.name, memory_symbol.type); + const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type); if(base_type_eq( ns.follow(memory_symbol.type).subtype(), @@ -418,16 +415,20 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // Types match already, what a coincidence! // We can use an index expression. - exprt index_expr=index_exprt(symbol_expr, pointer_offset(pointer_expr)); - index_expr.type()=ns.follow(memory_symbol.type).subtype(); + const index_exprt index_expr( + symbol_expr, + pointer_offset(pointer_expr), + ns.follow(memory_symbol.type).subtype()); result.value=index_expr; } else if(dereference_type_compare( ns.follow(memory_symbol.type).subtype(), dereference_type)) { - exprt index_expr=index_exprt(symbol_expr, pointer_offset(pointer_expr)); - index_expr.type()=ns.follow(memory_symbol.type).subtype(); + const index_exprt index_expr( + symbol_expr, + pointer_offset(pointer_expr), + ns.follow(memory_symbol.type).subtype()); result.value=typecast_exprt(index_expr, dereference_type); } else diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 23ccd0c7dad..1dc9b756910 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -184,8 +184,7 @@ void value_set_fit::flatten_rec( if(fi==values.end()) { // this is some static object, keep it in. - exprt se(ID_symbol, o.type().subtype()); - se.set(ID_identifier, o.get(ID_identifier)); + const symbol_exprt se(o.get(ID_identifier), o.type().subtype()); insert(dest, se, 0); } else @@ -874,10 +873,8 @@ void value_set_fit::get_reference_set_sharing_rec( insert(dest, exprt(ID_unknown, expr.type())); else { - exprt index_expr(ID_index, expr.type()); - index_expr.operands().resize(2); - index_expr.op0()=object; - index_expr.op1()=from_integer(0, index_type()); + index_exprt index_expr( + object, from_integer(0, index_type()), expr.type()); // adjust type? if(object.type().id()!="#REF#" && @@ -932,9 +929,7 @@ void value_set_fit::get_reference_set_sharing_rec( { offsett o = it->second; - exprt member_expr(ID_member, expr.type()); - member_expr.copy_to_operands(object); - member_expr.set(ID_component_name, component_name); + member_exprt member_expr(object, component_name, expr.type()); // adjust type? if(ns.follow(struct_op.type())!=ns.follow(object.type())) @@ -1000,9 +995,7 @@ void value_set_fit::assign( if(subtype.id()==ID_code) continue; - exprt lhs_member(ID_member, subtype); - lhs_member.set(ID_component_name, name); - lhs_member.copy_to_operands(lhs); + member_exprt lhs_member(lhs, name, subtype); exprt rhs_member; @@ -1060,8 +1053,8 @@ void value_set_fit::assign( } else if(type.id()==ID_array) { - exprt lhs_index(ID_index, type.subtype()); - lhs_index.copy_to_operands(lhs, exprt(ID_unknown, index_type())); + const index_exprt lhs_index( + lhs, exprt(ID_unknown, index_type()), type.subtype()); if(rhs.id()==ID_unknown || rhs.id()==ID_invalid) @@ -1096,16 +1089,16 @@ void value_set_fit::assign( { assert(rhs.operands().size()==3); - exprt op0_index(ID_index, type.subtype()); - op0_index.copy_to_operands(rhs.op0(), exprt(ID_unknown, index_type())); + const index_exprt op0_index( + rhs.op0(), exprt(ID_unknown, index_type()), type.subtype()); assign(lhs_index, op0_index, ns); assign(lhs_index, rhs.op2(), ns); } else { - exprt rhs_index(ID_index, type.subtype()); - rhs_index.copy_to_operands(rhs, exprt(ID_unknown, index_type())); + const index_exprt rhs_index( + rhs, exprt(ID_unknown, index_type()), type.subtype()); assign(lhs_index, rhs_index, ns); } } @@ -1371,7 +1364,7 @@ void value_set_fit::do_function_call( const std::string identifier="value_set::" + id2string(function) + "::" + "argument$"+std::to_string(i); add_var(identifier, ""); - exprt dummy_lhs=symbol_exprt(identifier, arguments[i].type()); + const symbol_exprt dummy_lhs(identifier, arguments[i].type()); assign(dummy_lhs, arguments[i], ns); } @@ -1394,7 +1387,7 @@ void value_set_fit::do_function_call( symbol_exprt("value_set::" + id2string(function) + "::" + "argument$"+std::to_string(i), it->type()); - exprt actual_lhs=symbol_exprt(identifier, it->type()); + const symbol_exprt actual_lhs(identifier, it->type()); assign(actual_lhs, v_expr, ns); i++; } diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index 13cf42abc3c..8255267d0ba 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -272,8 +272,7 @@ void value_set_fivrt::flatten_rec( if(fi==values.end()) { // this is some static object, keep it in. - exprt se(ID_symbol, o.type().subtype()); - se.set(ID_identifier, o.get(ID_identifier)); + const symbol_exprt se(o.get(ID_identifier), o.type().subtype()); insert_from(dest, se, 0); } else @@ -987,10 +986,8 @@ void value_set_fivrt::get_reference_set_sharing_rec( insert_from(dest, exprt(ID_unknown, expr.type())); else { - exprt index_expr(ID_index, expr.type()); - index_expr.operands().resize(2); - index_expr.op0()=object; - index_expr.op1()=from_integer(0, index_type()); + index_exprt index_expr( + object, from_integer(0, index_type()), expr.type()); // adjust type? if(object.type().id()!="#REF#" && @@ -1047,9 +1044,7 @@ void value_set_fivrt::get_reference_set_sharing_rec( { offsett o = it->second; - exprt member_expr(ID_member, expr.type()); - member_expr.copy_to_operands(object); - member_expr.set(ID_component_name, component_name); + member_exprt member_expr(object, component_name, expr.type()); // adjust type? if(ns.follow(struct_op.type())!=ns.follow(object.type())) @@ -1117,9 +1112,7 @@ void value_set_fivrt::assign( if(subtype.id()==ID_code) continue; - exprt lhs_member(ID_member, subtype); - lhs_member.set(ID_component_name, name); - lhs_member.copy_to_operands(lhs); + const member_exprt lhs_member(lhs, name, subtype); exprt rhs_member; @@ -1177,8 +1170,8 @@ void value_set_fivrt::assign( } else if(type.id()==ID_array) { - exprt lhs_index(ID_index, type.subtype()); - lhs_index.copy_to_operands(lhs, exprt(ID_unknown, index_type())); + const index_exprt lhs_index( + lhs, exprt(ID_unknown, index_type()), type.subtype()); if(rhs.id()==ID_unknown || rhs.id()==ID_invalid) @@ -1207,16 +1200,16 @@ void value_set_fivrt::assign( { assert(rhs.operands().size()==3); - exprt op0_index(ID_index, type.subtype()); - op0_index.copy_to_operands(rhs.op0(), exprt(ID_unknown, index_type())); + const index_exprt op0_index( + rhs.op0(), exprt(ID_unknown, index_type()), type.subtype()); assign(lhs_index, op0_index, ns, add_to_sets); assign(lhs_index, rhs.op2(), ns, true); } else { - exprt rhs_index(ID_index, type.subtype()); - rhs_index.copy_to_operands(rhs, exprt(ID_unknown, index_type())); + const index_exprt rhs_index( + rhs, exprt(ID_unknown, index_type()), type.subtype()); assign(lhs_index, rhs_index, ns, true); } } @@ -1517,8 +1510,7 @@ void value_set_fivrt::do_function_call( const std::string identifier="value_set::" + id2string(function) + "::" + "argument$"+std::to_string(i); add_var(identifier, ""); - exprt dummy_lhs=symbol_exprt(identifier, arguments[i].type()); -// std::cout << arguments[i] << '\n'; + const symbol_exprt dummy_lhs(identifier, arguments[i].type()); assign(dummy_lhs, arguments[i], ns, true); @@ -1551,7 +1543,7 @@ void value_set_fivrt::do_function_call( symbol_exprt("value_set::" + id2string(function) + "::" + "argument$"+std::to_string(i), it->type()); - exprt actual_lhs=symbol_exprt(identifier, it->type()); + const symbol_exprt actual_lhs(identifier, it->type()); assign(actual_lhs, v_expr, ns, true); i++; } diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 57eef42a5bb..631c628ccd9 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -679,10 +679,8 @@ void value_set_fivrnst::get_reference_set_rec( insert_from(dest, exprt(ID_unknown, expr.type())); else { - exprt index_expr(ID_index, expr.type()); - index_expr.operands().resize(2); - index_expr.op0()=object; - index_expr.op1()=from_integer(0, index_type()); + index_exprt index_expr( + object, from_integer(0, index_type()), expr.type()); // adjust type? if(ns.follow(object.type())!=array_type) @@ -738,9 +736,7 @@ void value_set_fivrnst::get_reference_set_rec( { offsett o = it->second; - exprt member_expr(ID_member, expr.type()); - member_expr.copy_to_operands(object); - member_expr.set(ID_component_name, component_name); + member_exprt member_expr(object, component_name, expr.type()); // adjust type? if(ns.follow(struct_op.type())!=ns.follow(object.type())) @@ -808,9 +804,7 @@ void value_set_fivrnst::assign( if(subtype.id()==ID_code) continue; - exprt lhs_member(ID_member, subtype); - lhs_member.set(ID_component_name, name); - lhs_member.copy_to_operands(lhs); + member_exprt lhs_member(lhs, name, subtype); exprt rhs_member; @@ -868,8 +862,8 @@ void value_set_fivrnst::assign( } else if(type.id()==ID_array) { - exprt lhs_index(ID_index, type.subtype()); - lhs_index.copy_to_operands(lhs, exprt(ID_unknown, index_type())); + const index_exprt lhs_index( + lhs, exprt(ID_unknown, index_type()), type.subtype()); if(rhs.id()==ID_unknown || rhs.id()==ID_invalid) @@ -898,16 +892,16 @@ void value_set_fivrnst::assign( { assert(rhs.operands().size()==3); - exprt op0_index(ID_index, type.subtype()); - op0_index.copy_to_operands(rhs.op0(), exprt(ID_unknown, index_type())); + const index_exprt op0_index( + rhs.op0(), exprt(ID_unknown, index_type()), type.subtype()); assign(lhs_index, op0_index, ns, add_to_sets); assign(lhs_index, rhs.op2(), ns, true); } else { - exprt rhs_index(ID_index, type.subtype()); - rhs_index.copy_to_operands(rhs, exprt(ID_unknown, index_type())); + const index_exprt rhs_index( + rhs, exprt(ID_unknown, index_type()), type.subtype()); assign(lhs_index, rhs_index, ns, true); } } @@ -1172,8 +1166,7 @@ void value_set_fivrnst::do_function_call( const std::string identifier="value_set::" + id2string(function) + "::" + "argument$"+std::to_string(i); add_var(identifier, ""); - exprt dummy_lhs=symbol_exprt(identifier, arguments[i].type()); -// std::cout << arguments[i] << '\n'; + const symbol_exprt dummy_lhs(identifier, arguments[i].type()); assign(dummy_lhs, arguments[i], ns, true); @@ -1206,7 +1199,7 @@ void value_set_fivrnst::do_function_call( symbol_exprt("value_set::" + id2string(function) + "::" + "argument$"+std::to_string(i), it->type()); - exprt actual_lhs=symbol_exprt(identifier, it->type()); + const symbol_exprt actual_lhs(identifier, it->type()); assign(actual_lhs, v_expr, ns, true); i++; } diff --git a/src/solvers/cvc/cvc_conv.cpp b/src/solvers/cvc/cvc_conv.cpp index 4762bf64215..a14edaf2b2d 100644 --- a/src/solvers/cvc/cvc_conv.cpp +++ b/src/solvers/cvc/cvc_conv.cpp @@ -508,8 +508,7 @@ void cvc_convt::convert_array_index(const exprt &expr) } else { - exprt tmp(ID_typecast, index_type()); - tmp.copy_to_operands(expr); + const typecast_exprt tmp(expr, index_type()); convert_expr(tmp); } } diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index ff7c92abf94..24403fceb13 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -191,7 +191,7 @@ exprt boolbvt::bv_get_rec( if(sub_width!=0 && width%sub_width==0) { std::size_t size=width/sub_width; - exprt value(ID_vector, type); + vector_exprt value(to_vector_type(type)); value.reserve_operands(size); for(std::size_t i=0; idistance); // check if first 'distance'-many bits are zeros - const exprt prefix= - extractbits_exprt(fraction, fraction_bits-1, fraction_bits-distance, - unsignedbv_typet(distance)); - exprt prefix_is_zero=equal_exprt(prefix, from_integer(0, prefix.type())); + const extractbits_exprt prefix( + fraction, + fraction_bits - 1, + fraction_bits - distance, + unsignedbv_typet(distance)); + const equal_exprt prefix_is_zero(prefix, from_integer(0, prefix.type())); // If so, shift the zeros out left by 'distance'. // Otherwise, leave as is. - const exprt shifted= - shl_exprt(fraction, distance); + const shl_exprt shifted(fraction, distance); fraction= if_exprt(prefix_is_zero, shifted, fraction); @@ -953,14 +939,13 @@ void float_bvt::denormalization_shift( exponent=typecast_exprt(exponent, signedbv_typet(exponent_bits+1)); #endif - exprt distance=minus_exprt( - from_integer(-bias+1, exponent.type()), exponent); + const minus_exprt distance( + from_integer(-bias + 1, exponent.type()), exponent); // use sign bit - exprt denormal= - and_exprt( - not_exprt(sign_exprt(distance)), - notequal_exprt(distance, from_integer(0, distance.type()))); + const and_exprt denormal( + not_exprt(sign_exprt(distance)), + notequal_exprt(distance, from_integer(0, distance.type()))); #if 1 // Care must be taken to not loose information required for the @@ -1072,37 +1057,31 @@ exprt float_bvt::fraction_rounding_decision( { // We keep most-significant bits, and thus the tail is made // of least-significant bits. - exprt tail= - extractbits_exprt(fraction, extra_bits-2, 0, - unsignedbv_typet(extra_bits-2+1)); + const extractbits_exprt tail( + fraction, extra_bits - 2, 0, unsignedbv_typet(extra_bits - 2 + 1)); sticky_bit=notequal_exprt(tail, from_integer(0, tail.type())); } // the rounding bit is the last extra bit assert(extra_bits>=1); - exprt rounding_bit=extractbit_exprt(fraction, extra_bits-1); + const extractbit_exprt rounding_bit(fraction, extra_bits - 1); // we get one bit of the fraction for some rounding decisions - exprt rounding_least=extractbit_exprt(fraction, extra_bits); + const extractbit_exprt rounding_least(fraction, extra_bits); // round-to-nearest (ties to even) - exprt round_to_even= - and_exprt(rounding_bit, - or_exprt(rounding_least, sticky_bit)); + const and_exprt round_to_even( + rounding_bit, or_exprt(rounding_least, sticky_bit)); // round up - exprt round_to_plus_inf= - and_exprt(not_exprt(sign), - or_exprt(rounding_bit, sticky_bit)); + const and_exprt round_to_plus_inf( + not_exprt(sign), or_exprt(rounding_bit, sticky_bit)); // round down - exprt round_to_minus_inf= - and_exprt(sign, - or_exprt(rounding_bit, sticky_bit)); + const and_exprt round_to_minus_inf(sign, or_exprt(rounding_bit, sticky_bit)); // round to zero - exprt round_to_zero= - false_exprt(); + false_exprt round_to_zero; // now select appropriate one return if_exprt(rounding_mode_bits.round_to_even, round_to_even, @@ -1168,7 +1147,7 @@ void float_bvt::round_fraction( // post normalization of the fraction exprt integer_part1=result.fraction.back(); exprt integer_part0=result.fraction[result.fraction.size()-2]; - exprt new_integer_part=or_exprt(integer_part1, integer_part0); + const or_exprt new_integer_part(integer_part1, integer_part0); result.fraction.resize(result.fraction.size()-1); result.fraction.back()=new_integer_part; @@ -1182,8 +1161,7 @@ void float_bvt::round_fraction( // 2. If the number is the largest subnormal, the increment // can change the MSB making it normal. Thus the exponent // must be incremented but the fraction will be OK. - exprt oldMSB= - extractbit_exprt(result.fraction, fraction_size-1); + const extractbit_exprt old_msb(result.fraction, fraction_size - 1); // increment if 'increment' is true result.fraction= @@ -1191,14 +1169,11 @@ void float_bvt::round_fraction( typecast_exprt(increment, result.fraction.type())); // Normal overflow when old MSB == 1 and new MSB == 0 - exprt newMSB= - extractbit_exprt(result.fraction, fraction_size-1); - - exprt overflow=and_exprt(oldMSB, not_exprt(newMSB)); + const extractbit_exprt new_msb(result.fraction, fraction_size - 1); + const and_exprt overflow(old_msb, not_exprt(new_msb)); // Subnormal to normal transition when old MSB == 0 and new MSB == 1 - exprt subnormal_to_normal= - and_exprt(not_exprt(oldMSB), newMSB); + const and_exprt subnormal_to_normal(not_exprt(old_msb), new_msb); // In case of an overflow or subnormal to normal conversion, // the exponent has to be incremented. @@ -1254,26 +1229,20 @@ void float_bvt::round_exponent( // the exponent is garbage if the fractional is zero - exprt exponent_too_large= - and_exprt( - binary_relation_exprt(old_exponent, ID_ge, max_exponent), - notequal_exprt( - result.fraction, - from_integer(0, result.fraction.type()))); + const and_exprt exponent_too_large( + binary_relation_exprt(old_exponent, ID_ge, max_exponent), + notequal_exprt(result.fraction, from_integer(0, result.fraction.type()))); #if 1 // Directed rounding modes round overflow to the maximum normal // depending on the particular mode and the sign - exprt overflow_to_inf= - or_exprt(rounding_mode_bits.round_to_even, - or_exprt(and_exprt(rounding_mode_bits.round_to_plus_inf, - not_exprt(result.sign)), - and_exprt(rounding_mode_bits.round_to_minus_inf, - result.sign))); - - exprt set_to_max= - and_exprt(exponent_too_large, not_exprt(overflow_to_inf)); + const or_exprt overflow_to_inf( + rounding_mode_bits.round_to_even, + or_exprt( + and_exprt(rounding_mode_bits.round_to_plus_inf, not_exprt(result.sign)), + and_exprt(rounding_mode_bits.round_to_minus_inf, result.sign))); + const and_exprt set_to_max(exponent_too_large, not_exprt(overflow_to_inf)); exprt largest_normal_exponent= from_integer( @@ -1313,8 +1282,8 @@ float_bvt::biased_floatt float_bvt::bias( // strip off the hidden bit assert(to_unsignedbv_type(src.fraction.type()).get_width()==spec.f+1); - exprt hidden_bit=extractbit_exprt(src.fraction, spec.f); - exprt denormal=not_exprt(hidden_bit); + const extractbit_exprt hidden_bit(src.fraction, spec.f); + const not_exprt denormal(hidden_bit); result.fraction= extractbits_exprt( @@ -1391,23 +1360,20 @@ exprt float_bvt::pack( assert(to_unsignedbv_type(src.exponent.type()).get_width()==spec.e); // do sign -- we make this 'false' for NaN - exprt sign_bit= - if_exprt(src.NaN, false_exprt(), src.sign); + const if_exprt sign_bit(src.NaN, false_exprt(), src.sign); // the fraction is zero in case of infinity, // and one in case of NaN - exprt fraction= - if_exprt(src.NaN, from_integer(1, src.fraction.type()), - if_exprt(src.infinity, from_integer(0, src.fraction.type()), - src.fraction)); + const if_exprt fraction( + src.NaN, + from_integer(1, src.fraction.type()), + if_exprt(src.infinity, from_integer(0, src.fraction.type()), src.fraction)); - exprt infinity_or_NaN= - or_exprt(src.NaN, src.infinity); + const or_exprt infinity_or_NaN(src.NaN, src.infinity); // do exponent - exprt exponent= - if_exprt(infinity_or_NaN, from_integer(-1, src.exponent.type()), - src.exponent); + const if_exprt exponent( + infinity_or_NaN, from_integer(-1, src.exponent.type()), src.exponent); // stitch all three together return concatenation_exprt( @@ -1431,7 +1397,7 @@ exprt float_bvt::sticky_right_shift( for(std::size_t stage=0; stagesecond.first; unsigned index=it->second.second; - exprt extract_expr(ID_extractbit, typet(ID_bool)); - extract_expr.copy_to_operands(sym); - - typet uint_type(ID_unsignedbv); - uint_type.set(ID_width, 32); - extract_expr.copy_to_operands(from_integer(index, uint_type)); + extractbit_exprt extract_expr(sym, from_integer(index, integer_typet())); if(l.sign()) extract_expr.negate(); @@ -328,7 +323,7 @@ const exprt qbf_bdd_certificatet::f_get(literalt l) int *cube; DdGen *generator; - exprt result=or_exprt(); + or_exprt result; Cudd_ForeachPrime( bdd_manager->getManager(), @@ -337,7 +332,7 @@ const exprt qbf_bdd_certificatet::f_get(literalt l) generator, cube) { - exprt prime=and_exprt(); + and_exprt prime; #if 0 std::cout << "CUBE: "; diff --git a/src/solvers/qbf/qbf_squolem_core.cpp b/src/solvers/qbf/qbf_squolem_core.cpp index 04f5c7ae3c6..fd2106711ce 100644 --- a/src/solvers/qbf/qbf_squolem_core.cpp +++ b/src/solvers/qbf/qbf_squolem_core.cpp @@ -198,11 +198,7 @@ const exprt qbf_squolem_coret::f_get(literalt l) const exprt &sym=it->second.first; unsigned index=it->second.second; - exprt extract_expr(ID_extractbit, typet(ID_bool)); - extract_expr.copy_to_operands(sym); - typet uint_type(ID_unsignedbv); - uint_type.set(ID_width, 32); - extract_expr.copy_to_operands(from_integer(index, uint_type)); + extractbit_exprt extract_expr(sym, from_integer(index, integer_typet())); if(l.sign()) extract_expr.negate(); @@ -257,7 +253,7 @@ const exprt qbf_squolem_coret::f_get_cnf(WitnessStack *wsp) while(p!=NULL) { - exprt clause=or_exprt(); + or_exprt clause; for(unsigned i=0; isize; i++) { @@ -299,7 +295,7 @@ const exprt qbf_squolem_coret::f_get_dnf(WitnessStack *wsp) while(p!=NULL) { - exprt cube=and_exprt(); + and_exprt cube; for(unsigned i=0; isize; i++) { diff --git a/src/solvers/qbf/qdimacs_core.cpp b/src/solvers/qbf/qdimacs_core.cpp index e729d8ece58..c46d06729ff 100644 --- a/src/solvers/qbf/qdimacs_core.cpp +++ b/src/solvers/qbf/qdimacs_core.cpp @@ -83,8 +83,7 @@ void qdimacs_coret::simplify_extractbits(exprt &expr) const new_operands.push_back(*oit); } - exprt new_value(ID_constant, it->first.type()); - new_value.set(ID_value, value_string); + const constant_exprt new_value(value_string, it->first.type()); new_operands.push_back(equality_exprt(it->first, new_value)); #if 0 diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index 7e084f872f8..54afb59ca0d 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -27,8 +27,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com exprt get_exponent( const exprt &src, const ieee_float_spect &spec) { - exprt exp_bits=extractbits_exprt( - src, spec.f+spec.e-1, spec.f, unsignedbv_typet(spec.e)); + const extractbits_exprt exp_bits( + src, spec.f + spec.e - 1, spec.f, unsignedbv_typet(spec.e)); // Exponent is in biased form (numbers from -128 to 127 are encoded with // integer from 0 to 255) we have to remove the bias. diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index 6a2c7d0d8a3..b8dbfaa95ec 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -151,15 +151,13 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix( lemmas.push_back(a1); symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type); - exprt qvar_shifted=plus_exprt( - qvar, minus_exprt(s1.length(), s0.length())); + const plus_exprt qvar_shifted(qvar, minus_exprt(s1.length(), s0.length())); string_constraintt a2( qvar, s0.length(), issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])); constraints.push_back(a2); symbol_exprt witness=fresh_exist_index("witness_not_suffix", index_type); - exprt shifted=plus_exprt( - witness, minus_exprt(s1.length(), s0.length())); + const plus_exprt shifted(witness, minus_exprt(s1.length(), s0.length())); or_exprt constr3( and_exprt( s0.axiom_for_length_gt(s1.length()), @@ -221,7 +219,7 @@ exprt string_constraint_generatort::add_axioms_for_contains( lemmas.push_back(a3); symbol_exprt qvar=fresh_univ_index("QA_contains", index_type); - exprt qvar_shifted=plus_exprt(qvar, startpos); + const plus_exprt qvar_shifted(qvar, startpos); string_constraintt a4( qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted])); constraints.push_back(a4); diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index e589ff5c65d..1271c11184a 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -346,7 +346,7 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case( lemmas.push_back(a1); symbol_exprt idx1=fresh_univ_index("QA_upper_case1", index_type); - exprt is_lower_case=and_exprt( + const and_exprt is_lower_case( binary_relation_exprt(char_a, ID_le, str[idx1]), binary_relation_exprt(str[idx1], ID_le, char_z)); minus_exprt diff(char_A, char_a); @@ -356,9 +356,10 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case( constraints.push_back(a2); symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type); - exprt is_not_lower_case=not_exprt(and_exprt( - binary_relation_exprt(char_a, ID_le, str[idx2]), - binary_relation_exprt(str[idx2], ID_le, char_z))); + const not_exprt is_not_lower_case( + and_exprt( + binary_relation_exprt(char_a, ID_le, str[idx2]), + binary_relation_exprt(str[idx2], ID_le, char_z))); equal_exprt eq(res[idx2], str[idx2]); implies_exprt body2(is_not_lower_case, eq); string_constraintt a3(idx2, res.length(), body2); diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 920f0de801a..2842fb3ab13 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -160,8 +160,8 @@ exprt string_constraint_generatort::add_axioms_from_int_with_radix( } const typet &char_type = res.content().type().subtype(); - exprt radix_as_char=typecast_exprt(radix, char_type); - exprt radix_input_type=typecast_exprt(radix, type); + const typecast_exprt radix_as_char(radix, char_type); + const typecast_exprt radix_input_type(radix, type); const bool strict_formatting=true; add_axioms_for_correct_number_format( diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 882b2b28e5d..20ff4a5c5da 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1824,10 +1824,9 @@ static std::pair> check_axioms( implies_exprt instance(axiom.premise(), axiom.body()); replace_expr(axiom.univ_var(), val, instance); // We are not sure the index set contains only positive numbers - exprt bounds=and_exprt( + and_exprt bounds( axiom.univ_within_bounds(), - binary_relation_exprt( - from_integer(0, val.type()), ID_le, val)); + binary_relation_exprt(from_integer(0, val.type()), ID_le, val)); replace_expr(axiom.univ_var(), val, bounds); const implies_exprt counter(bounds, instance); @@ -2308,10 +2307,9 @@ static exprt instantiate( implies_exprt instance(axiom.premise(), axiom.body()); replace_expr(axiom.univ_var(), r, instance); // We are not sure the index set contains only positive numbers - exprt bounds=and_exprt( + and_exprt bounds( axiom.univ_within_bounds(), - binary_relation_exprt( - from_integer(0, val.type()), ID_le, val)); + binary_relation_exprt(from_integer(0, val.type()), ID_le, val)); replace_expr(axiom.univ_var(), r, bounds); return implies_exprt(bounds, instance); } diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp index da24fead7f5..b52c86a5428 100644 --- a/src/solvers/smt1/smt1_conv.cpp +++ b/src/solvers/smt1/smt1_conv.cpp @@ -174,6 +174,7 @@ exprt smt1_convt::ce_value( } else if(type.id()==ID_array) { + const array_typet &array_type = to_array_type(type); const typet &subtype=ns.follow(type.subtype()); // arrays in structs are flat, no index @@ -182,12 +183,12 @@ exprt smt1_convt::ce_value( // we can only do fixed-size arrays mp_integer size; - if(!to_integer(to_array_type(type).size(), size)) + if(!to_integer(array_type.size(), size)) { std::size_t size_int=integer2unsigned(size); std::size_t sub_width=value.size()/size_int; - exprt array_list(ID_array, type); - array_list.operands().resize(size_int); + array_exprt array_list(array_type); + array_list.reserve_operands(size_int); std::size_t offset=value.size(); @@ -195,8 +196,7 @@ exprt smt1_convt::ce_value( { offset-=sub_width; std::string sub_value=value.substr(offset, sub_width); - array_list.operands()[i]= - ce_value(subtype, "", sub_value, true); + array_list.copy_to_operands(ce_value(subtype, "", sub_value, true)); } return array_list; @@ -244,8 +244,7 @@ void smt1_convt::array_index(const exprt &expr) typet t=array_index_type(); if(t==expr.type()) return convert_expr(expr, true); - exprt tmp(ID_typecast, t); - tmp.copy_to_operands(expr); + const typecast_exprt tmp(expr, t); convert_expr(tmp, true); } @@ -322,8 +321,7 @@ void smt1_convt::convert_address_of_rec( mp_integer offset=member_offset(struct_type, component_name, ns); assert(offset>=0); - typet index_type(ID_unsignedbv); - index_type.set(ID_width, boolbv_width(result_type)); + const unsignedbv_typet index_type(boolbv_width(result_type)); out << "(bvadd "; convert_address_of_rec(struct_op, result_type); @@ -3090,11 +3088,10 @@ exprt smt1_convt::binary2struct( if(total_width==0) throw "failed to get struct width"; - exprt e(ID_struct, type); - e.operands().resize(components.size()); + struct_exprt e(type); + e.reserve_operands(components.size()); std::size_t index=binary.size(); - std::size_t i=0; for(const auto &comp : components) { const typet &sub_type=ns.follow(comp.type()); @@ -3107,7 +3104,7 @@ exprt smt1_convt::binary2struct( index-=sub_size; std::string cval=binary.substr(index, sub_size); - e.operands()[i++]=ce_value(sub_type, "", cval, true); + e.copy_to_operands(ce_value(sub_type, "", cval, true)); } return e; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index f1b2d2cd127..0a79bfb9f89 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -378,7 +378,7 @@ exprt smt2_convt::parse_union( exprt value=parse_rec(src, bv_typet(width)); if(value.is_nil()) return nil_exprt(); - exprt converted=typecast_exprt(value, first.type()); + const typecast_exprt converted(value, first.type()); return union_exprt(first.get_name(), converted, type); } @@ -695,13 +695,12 @@ void smt2_convt::convert_byte_update(const byte_update_exprt &expr) mp_integer mask=power(2, value_width)-1; exprt one_mask=from_integer(mask, unsignedbv_typet(total_width)); - exprt distance=mult_exprt( - expr.offset(), - from_integer(8, expr.offset().type())); + const mult_exprt distance( + expr.offset(), from_integer(8, expr.offset().type())); - exprt and_expr=bitand_exprt(expr.op(), bitnot_exprt(one_mask)); - exprt ext_value=typecast_exprt(expr.value(), one_mask.type()); - exprt or_expr=bitor_exprt(and_expr, shl_exprt(ext_value, distance)); + const bitand_exprt and_expr(expr.op(), bitnot_exprt(one_mask)); + const typecast_exprt ext_value(expr.value(), one_mask.type()); + const bitor_exprt or_expr(and_expr, shl_exprt(ext_value, distance)); unflatten(wheret::BEGIN, expr.type()); flatten2bv(or_expr); @@ -2277,7 +2276,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) else if(src_type.id()==ID_c_bool) { // turn into proper bool - exprt tmp=typecast_exprt(src, bool_typet()); + const typecast_exprt tmp(src, bool_typet()); convert_typecast(typecast_exprt(tmp, dest_type)); } else diff --git a/src/util/expr.cpp b/src/util/expr.cpp index ad4c0a4e856..a990ec357d2 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -87,10 +87,7 @@ void exprt::copy_to_operands( void exprt::make_typecast(const typet &_type) { - exprt new_expr(ID_typecast); - - new_expr.move_to_operands(*this); - new_expr.set(ID_type, _type); + typecast_exprt new_expr(*this, _type); swap(new_expr); } @@ -218,8 +215,7 @@ void exprt::negate() } else { - exprt tmp(ID_unary_minus, type()); - tmp.move_to_operands(*this); + unary_minus_exprt tmp(*this); swap(tmp); } } diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 614aa4fa320..27104f2292c 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -326,8 +326,7 @@ exprt size_of_expr( if(size.type()!=sub.type()) size.make_typecast(sub.type()); - exprt result=mult_exprt(size, sub); - + mult_exprt result(size, sub); simplify(result, ns); return result; @@ -347,7 +346,7 @@ exprt size_of_expr( if(size.type()!=sub.type()) size.make_typecast(sub.type()); - exprt result=mult_exprt(size, sub); + mult_exprt result(size, sub); simplify(result, ns); return result; @@ -360,7 +359,7 @@ exprt size_of_expr( const exprt size=from_integer(2, sub.type()); - exprt result=mult_exprt(size, sub); + mult_exprt result(size, sub); simplify(result, ns); return result; diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index e0ef139be4a..312166f0088 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -94,47 +94,30 @@ exprt good_pointer_def( const pointer_typet &pointer_type=to_pointer_type(ns.follow(pointer.type())); const typet &dereference_type=pointer_type.subtype(); - exprt good_dynamic_tmp1= - or_exprt( - not_exprt(malloc_object(pointer, ns)), - and_exprt( - not_exprt( - dynamic_object_lower_bound( - pointer, - ns, - nil_exprt())), - not_exprt( - dynamic_object_upper_bound( - pointer, - dereference_type, - ns, - size_of_expr(dereference_type, ns))))); - - exprt good_dynamic_tmp2= - and_exprt(not_exprt(deallocated(pointer, ns)), - good_dynamic_tmp1); - - exprt good_dynamic= - or_exprt(not_exprt(dynamic_object(pointer)), - good_dynamic_tmp2); - - exprt not_null= - not_exprt(null_pointer(pointer)); - - exprt not_invalid= - not_exprt(invalid_pointer(pointer)); - - exprt bad_other= - or_exprt(object_lower_bound(pointer, ns, nil_exprt()), - object_upper_bound( - pointer, - dereference_type, - ns, - size_of_expr(dereference_type, ns))); - - exprt good_other= - or_exprt(dynamic_object(pointer), - not_exprt(bad_other)); + const or_exprt good_dynamic_tmp1( + not_exprt(malloc_object(pointer, ns)), + and_exprt( + not_exprt(dynamic_object_lower_bound(pointer, ns, nil_exprt())), + not_exprt( + dynamic_object_upper_bound( + pointer, dereference_type, ns, size_of_expr(dereference_type, ns))))); + + const and_exprt good_dynamic_tmp2( + not_exprt(deallocated(pointer, ns)), good_dynamic_tmp1); + + const or_exprt good_dynamic( + not_exprt(dynamic_object(pointer)), good_dynamic_tmp2); + + const not_exprt not_null(null_pointer(pointer)); + + const not_exprt not_invalid(invalid_pointer(pointer)); + + const or_exprt bad_other( + object_lower_bound(pointer, ns, nil_exprt()), + object_upper_bound( + pointer, dereference_type, ns, size_of_expr(dereference_type, ns))); + + const or_exprt good_other(dynamic_object(pointer), not_exprt(bad_other)); return and_exprt( not_null, diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 3ff5a7c5ced..f39237d6b48 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -430,8 +430,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr) if(expr.op0().id()==ID_if && expr.op0().operands().size()==3) { - exprt tmp_op1=typecast_exprt(expr.op0().op1(), expr_type); - exprt tmp_op2=typecast_exprt(expr.op0().op2(), expr_type); + typecast_exprt tmp_op1(expr.op0().op1(), expr_type); + typecast_exprt tmp_op2(expr.op0().op2(), expr_type); simplify_typecast(tmp_op1); simplify_typecast(tmp_op2); expr=if_exprt(expr.op0().op0(), tmp_op1, tmp_op2, expr_type); @@ -1545,7 +1545,7 @@ exprt simplify_exprt::bits2expr( const struct_typet::componentst &components= struct_type.components(); - exprt result=struct_exprt(type); + struct_exprt result(type); result.reserve_operands(components.size()); mp_integer m_offset_bits=0; @@ -1582,7 +1582,7 @@ exprt simplify_exprt::bits2expr( integer2size_t(pointer_offset_bits(type.subtype(), ns)); assert(el_size>0); - exprt result=array_exprt(array_type); + array_exprt result(array_type); result.reserve_operands(n_el); for(std::size_t i=0; i(op0()); @@ -4820,6 +4828,11 @@ class forall_exprt:public quantifier_exprt forall_exprt():quantifier_exprt(ID_forall) { } + + forall_exprt(const symbol_exprt &_symbol, const exprt &_where) + : quantifier_exprt(ID_forall, _symbol, _where) + { + } }; /*! \brief An exists expression @@ -4830,6 +4843,11 @@ class exists_exprt:public quantifier_exprt exists_exprt():quantifier_exprt(ID_exists) { } + + exists_exprt(const symbol_exprt &_symbol, const exprt &_where) + : quantifier_exprt(ID_exists, _symbol, _where) + { + } }; /*! \brief The popcount (counting the number of bits set to 1) expression