From 314ed539e1dce6ee81a31a850a4cfff838eddcb6 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Fri, 13 Apr 2018 10:52:29 +0100 Subject: [PATCH] Correcting the value of ID_null_object --- src/analyses/ai.cpp | 2 +- src/analyses/flow_insensitive_analysis.cpp | 2 +- src/analyses/goto_rw.cpp | 14 +++++++------- src/analyses/invariant_set.cpp | 8 ++++---- src/analyses/static_analysis.cpp | 4 ++-- src/ansi-c/expr2c.cpp | 5 +---- src/goto-programs/goto_convert_function_call.cpp | 2 +- src/goto-programs/interpreter.cpp | 2 +- src/goto-programs/string_abstraction.cpp | 4 ++-- src/goto-symex/symex_assign.cpp | 12 ++++++------ src/goto-symex/symex_other.cpp | 2 +- src/pointer-analysis/value_set.cpp | 6 +++--- src/pointer-analysis/value_set_dereference.cpp | 2 +- src/pointer-analysis/value_set_fi.cpp | 4 ++-- src/pointer-analysis/value_set_fivr.cpp | 4 ++-- src/pointer-analysis/value_set_fivrns.cpp | 4 ++-- src/solvers/flattening/bv_pointers.cpp | 2 +- src/util/irep_ids.def | 2 +- .../pointer-analysis/custom_value_set_analysis.cpp | 2 +- 19 files changed, 40 insertions(+), 43 deletions(-) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index dedb2da9a3c..86c181374af 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -506,7 +506,7 @@ bool ai_baset::do_function_call_rec( // We can't really do this here -- we rely on // these being removed by some previous analysis. } - else if(function.id()=="NULL-object") + else if(function.id() == ID_null_object) { // ignore, can't be a function } diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp index b8ad09a4b5b..42a110e42a4 100644 --- a/src/analyses/flow_insensitive_analysis.cpp +++ b/src/analyses/flow_insensitive_analysis.cpp @@ -371,7 +371,7 @@ bool flow_insensitive_analysis_baset::do_function_call_rec( } } } - else if(function.id()=="NULL-object") + else if(function.id() == ID_null_object) { // ignore, can't be a function } diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index be0f162c539..1b65690349d 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -242,7 +242,7 @@ void rw_range_sett::get_objects_index( const range_spect &range_start, const range_spect &size) { - if(expr.array().id()=="NULL-object") + if(expr.array().id() == ID_null_object) return; range_spect sub_size=0; @@ -413,10 +413,10 @@ void rw_range_sett::get_objects_typecast( void rw_range_sett::get_objects_address_of(const exprt &object) { - if(object.id()==ID_string_constant || - object.id()==ID_label || - object.id()==ID_array || - object.id()=="NULL-object") + if(object.id() == ID_string_constant || + object.id() == ID_label || + object.id() == ID_array || + object.id() == ID_null_object) // constant, nothing to do return; else if(object.id()==ID_symbol) @@ -558,8 +558,8 @@ void rw_range_sett::get_objects_rec( forall_operands(it, expr) get_objects_rec(mode, *it); } - else if(expr.id()=="NULL-object" || - expr.id()==ID_string_constant) + else if(expr.id() == ID_null_object || + expr.id() == ID_string_constant) { // dereferencing may yield some weird ones, ignore these } diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index e1819908938..526ceb88231 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -1036,10 +1036,10 @@ void invariant_sett::modifies(const exprt &lhs) assert(lhs.operands().size()==2); modifies(lhs.op0()); } - else if(lhs.id()=="NULL-object" || - lhs.id()=="is_zero_string" || - lhs.id()=="zero_string" || - lhs.id()=="zero_string_length") + else if(lhs.id() == ID_null_object || + lhs.id() == "is_zero_string" || + lhs.id() == "zero_string" || + lhs.id() == "zero_string_length") { // ignore } diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp index 27acbbc365c..0ee8ef3841b 100644 --- a/src/analyses/static_analysis.cpp +++ b/src/analyses/static_analysis.cpp @@ -397,8 +397,8 @@ void static_analysis_baset::do_function_call_rec( } } } - else if(function.id()=="NULL-object" || - function.id()==ID_integer_address) + else if(function.id() == ID_null_object || + function.id() == ID_integer_address) { // ignore, can't be a function } diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index a0b79883fad..79eb472e9f9 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3555,10 +3555,7 @@ std::string expr2ct::convert_with_precedence( else if(src.id()=="pointer_difference") return convert_pointer_difference(src, precedence=16); - else if(src.id()=="NULL-object") - return "NULL-object"; - - else if(src.id()==ID_null_object) + else if(src.id() == ID_null_object) return "NULL-object"; else if(src.id()==ID_integer_address || diff --git a/src/goto-programs/goto_convert_function_call.cpp b/src/goto-programs/goto_convert_function_call.cpp index 85d5d75358d..f1511b76a77 100644 --- a/src/goto-programs/goto_convert_function_call.cpp +++ b/src/goto-programs/goto_convert_function_call.cpp @@ -71,7 +71,7 @@ void goto_convertt::do_function_call( do_function_call_symbol( new_lhs, to_symbol_expr(new_function), new_arguments, dest); } - else if(new_function.id()=="NULL-object") + else if(new_function.id() == ID_null_object) { } else if(new_function.id()==ID_dereference || diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index e72b7454ff5..1b24e7f443a 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -862,7 +862,7 @@ void interpretert::build_memory_map() { // put in a dummy for NULL memory.resize(1); - inverse_memory_map[0]="NULL-OBJECT"; + inverse_memory_map[0] = ID_null_object; num_dynamic_objects=0; dynamic_types.clear(); diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 005d6ab3a8f..7790d6bd471 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -894,7 +894,7 @@ exprt string_abstractiont::build_unknown(whatt what, bool write) typet type=build_type(what); if(write) - return exprt("NULL-object", type); + return exprt(ID_null_object, type); exprt result; @@ -916,7 +916,7 @@ exprt string_abstractiont::build_unknown(whatt what, bool write) exprt string_abstractiont::build_unknown(const typet &type, bool write) { if(write) - return exprt("NULL-object", type); + return exprt(ID_null_object, type); // create an uninitialized dummy symbol // because of a lack of contextual information we can't build a nice name diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index f8c38126d6d..2c95736ed42 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -150,11 +150,11 @@ void goto_symext::symex_assign_rec( else if(lhs.id()==ID_typecast) symex_assign_typecast( state, to_typecast_expr(lhs), full_lhs, rhs, guard, assignment_type); - else if(lhs.id()==ID_string_constant || - lhs.id()=="NULL-object" || - lhs.id()=="zero_string" || - lhs.id()=="is_zero_string" || - lhs.id()=="zero_string_length") + else if(lhs.id() == ID_string_constant || + lhs.id() == ID_null_object || + lhs.id() == "zero_string" || + lhs.id() == "is_zero_string" || + lhs.id() == "zero_string_length") { // ignore } @@ -355,7 +355,7 @@ void goto_symext::symex_assign_struct_member( { assert(lhs_struct.operands().size()==1); - if(lhs_struct.op0().id()=="NULL-object") + if(lhs_struct.op0().id() == ID_null_object) { // ignore, and give up return; diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 12959f1c5a3..f3cc50c32bb 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -34,7 +34,7 @@ void goto_symext::havoc_rec( lhs=dest; else lhs=if_exprt( - guard.as_expr(), dest, exprt("NULL-object", dest.type())); + guard.as_expr(), dest, exprt(ID_null_object, dest.type())); code_assignt assignment; assignment.lhs()=lhs; diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 9ad467b0b45..c9858d251cb 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -507,7 +507,7 @@ void value_sett::get_value_set_rec( if(expr.get(ID_value)==ID_NULL && expr_type.id()==ID_pointer) { - insert(dest, exprt("NULL-object", expr_type.subtype()), 0); + insert(dest, exprt(ID_null_object, expr_type.subtype()), 0); } else if(expr_type.id()==ID_unsignedbv || expr_type.id()==ID_signedbv) @@ -538,7 +538,7 @@ void value_sett::get_value_set_rec( // integer-to-pointer if(expr.op0().is_zero()) - insert(dest, exprt("NULL-object", expr_type.subtype()), 0); + insert(dest, exprt(ID_null_object, expr_type.subtype()), 0); else { // see if we have something for the integer @@ -1409,7 +1409,7 @@ void value_sett::assign_rec( // someone writes into a string-constant // evil guy } - else if(lhs.id()=="NULL-object") + else if(lhs.id() == ID_null_object) { // evil as well } diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index c29cd31fc3c..37f8cb95cd5 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -301,7 +301,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( valuet result; - if(root_object.id()=="NULL-object") + if(root_object.id() == ID_null_object) { if(options.get_bool_option("pointer-check")) { diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index c126c5da760..0f8179787c7 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -528,7 +528,7 @@ void value_set_fit::get_value_set_rec( if(expr.get(ID_value)==ID_NULL && expr.type().id()==ID_pointer) { - insert(dest, exprt("NULL-object", expr.type().subtype()), 0); + insert(dest, exprt(ID_null_object, expr.type().subtype()), 0); return; } } @@ -1318,7 +1318,7 @@ void value_set_fit::assign_rec( // someone writes into a string-constant // evil guy } - else if(lhs.id()=="NULL-object") + else if(lhs.id() == ID_null_object) { // evil as well } diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index 4e97223772d..8d0ad73e99c 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -645,7 +645,7 @@ void value_set_fivrt::get_value_set_rec( if(expr.get(ID_value)==ID_NULL && expr.type().id()==ID_pointer) { - insert_from(dest, exprt("NULL-object", expr.type().subtype()), 0); + insert_from(dest, exprt(ID_null_object, expr.type().subtype()), 0); return; } } @@ -1456,7 +1456,7 @@ void value_set_fivrt::assign_rec( // someone writes into a string-constant // evil guy } - else if(lhs.id()=="NULL-object") + else if(lhs.id() == ID_null_object) { // evil as well } diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 631c628ccd9..c88b352f825 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -434,7 +434,7 @@ void value_set_fivrnst::get_value_set_rec( if(expr.get(ID_value)==ID_NULL && expr.type().id()==ID_pointer) { - insert_from(dest, exprt("NULL-object", expr.type().subtype()), 0); + insert_from(dest, exprt(ID_null_object, expr.type().subtype()), 0); return; } } @@ -1112,7 +1112,7 @@ void value_set_fivrnst::assign_rec( // someone writes into a string-constant // evil guy } - else if(lhs.id()=="NULL-object") + else if(lhs.id() == ID_null_object) { // evil as well } diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 833ca000f81..5833a3e4549 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -116,7 +116,7 @@ bool bv_pointerst::convert_address_of_rec( add_addr(expr, bv); return false; } - else if(expr.id()=="NULL-object") + else if(expr.id() == ID_null_object) { encode(pointer_logic.get_null_object(), bv); return false; diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 33b961653b8..8a930137f4e 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -526,7 +526,7 @@ IREP_ID_ONE(object_size) IREP_ID_ONE(good_pointer) IREP_ID_ONE(integer_address) IREP_ID_ONE(integer_address_object) -IREP_ID_ONE(null_object) +IREP_ID_TWO(null_object, NULL-object) IREP_ID_ONE(static_object) IREP_ID_ONE(stack_object) IREP_ID_TWO(C_is_failed_symbol, #is_failed_symbol) diff --git a/unit/pointer-analysis/custom_value_set_analysis.cpp b/unit/pointer-analysis/custom_value_set_analysis.cpp index 991f3addf48..5fdc3197f38 100644 --- a/unit/pointer-analysis/custom_value_set_analysis.cpp +++ b/unit/pointer-analysis/custom_value_set_analysis.cpp @@ -320,7 +320,7 @@ SCENARIO("test_value_set_analysis", REQUIRE(exprs_with_id(normal_exprs_after, ID_dynamic_object)==1); REQUIRE(test_exprs_after.size()==1); - REQUIRE(exprs_with_id(test_exprs_after, "NULL-object")==1); + REQUIRE(exprs_with_id(test_exprs_after, ID_null_object)==1); } } }