From 1bac4847dfd40117488ed3faef11f4a5f6e88b0f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 11 Feb 2018 20:17:58 +0000 Subject: [PATCH 1/5] cleanout decision_proceduret::in_core --- src/util/decision_procedure.cpp | 6 ------ src/util/decision_procedure.h | 3 --- 2 files changed, 9 deletions(-) diff --git a/src/util/decision_procedure.cpp b/src/util/decision_procedure.cpp index 61f30f626b4..132f1b0fc5c 100644 --- a/src/util/decision_procedure.cpp +++ b/src/util/decision_procedure.cpp @@ -11,10 +11,4 @@ Author: Daniel Kroening, kroening@kroening.com #include "decision_procedure.h" -#include -bool decision_proceduret::in_core(const exprt &expr) -{ - UNREACHABLE; - return true; -} diff --git a/src/util/decision_procedure.h b/src/util/decision_procedure.h index 65caffab17e..b966cb96dd6 100644 --- a/src/util/decision_procedure.h +++ b/src/util/decision_procedure.h @@ -52,9 +52,6 @@ class decision_proceduret:public messaget return dec_solve(); } - // old-style, will go away - virtual bool in_core(const exprt &expr); - // return a textual description of the decision procedure virtual std::string decision_procedure_text() const=0; From 77c8b9c5911c4e079884e9883e596db2633ea749 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 11 Feb 2018 20:25:45 +0000 Subject: [PATCH 2/5] remove translation for certain boolean program constructs --- src/goto-programs/goto_convert.cpp | 86 -------------------------- src/goto-programs/goto_convert_class.h | 2 - 2 files changed, 88 deletions(-) diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 505cf4c1e79..899e4cd7d33 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -515,10 +515,6 @@ void goto_convertt::convert( convert_atomic_begin(code, dest); else if(statement==ID_atomic_end) convert_atomic_end(code, dest); - else if(statement==ID_bp_enforce) - convert_bp_enforce(code, dest); - else if(statement==ID_bp_abortif) - convert_bp_abortif(code, dest); else if(statement==ID_cpp_delete || statement=="cpp_delete[]") convert_cpp_delete(code, dest); @@ -1604,88 +1600,6 @@ void goto_convertt::convert_atomic_end( copy(code, ATOMIC_END, dest); } -void goto_convertt::convert_bp_enforce( - const codet &code, - goto_programt &dest) -{ - if(code.operands().size()!=2) - { - error().source_location=code.find_source_location(); - error() << "bp_enfroce expects two arguments" << eom; - throw 0; - } - - // do an assume - exprt op=code.op0(); - - clean_expr(op, dest); - - goto_programt::targett t=dest.add_instruction(ASSUME); - t->guard=op; - t->source_location=code.source_location(); - - // change the assignments - - goto_programt tmp; - convert(to_code(code.op1()), tmp); - - if(!op.is_true()) - { - exprt constraint(op); - make_next_state(constraint); - - Forall_goto_program_instructions(it, tmp) - { - if(it->is_assign()) - { - assert(it->code.get(ID_statement)==ID_assign); - - // add constrain - codet constrain(ID_bp_constrain); - constrain.reserve_operands(2); - constrain.move_to_operands(it->code); - constrain.copy_to_operands(constraint); - it->code.swap(constrain); - - it->type=OTHER; - } - else if(it->is_other() && - it->code.get(ID_statement)==ID_bp_constrain) - { - // add to constraint - assert(it->code.operands().size()==2); - it->code.op1()= - and_exprt(it->code.op1(), constraint); - } - } - } - - dest.destructive_append(tmp); -} - -void goto_convertt::convert_bp_abortif( - const codet &code, - goto_programt &dest) -{ - if(code.operands().size()!=1) - { - error().source_location=code.find_source_location(); - error() << "bp_abortif expects one argument" << eom; - throw 0; - } - - // do an assert - exprt op=code.op0(); - - clean_expr(op, dest); - - op.make_not(); - - goto_programt::targett t=dest.add_instruction(ASSERT); - t->guard.swap(op); - t->source_location=code.source_location(); -} - void goto_convertt::convert_ifthenelse( const code_ifthenelset &code, goto_programt &dest) diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 1084f8353b1..4c5541a0108 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -234,8 +234,6 @@ class goto_convertt:public messaget void convert_end_thread(const codet &code, goto_programt &dest); void convert_atomic_begin(const codet &code, goto_programt &dest); void convert_atomic_end(const codet &code, goto_programt &dest); - void convert_bp_enforce(const codet &code, goto_programt &dest); - void convert_bp_abortif(const codet &code, goto_programt &dest); void convert_msc_try_finally(const codet &code, goto_programt &dest); void convert_msc_try_except(const codet &code, goto_programt &dest); void convert_msc_leave(const codet &code, goto_programt &dest); From 63f09acedf603ea8da1f219786802db093c6db80 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 11 Feb 2018 20:26:19 +0000 Subject: [PATCH 3/5] remove unused function make_next_state --- src/util/expr_util.cpp | 9 --------- src/util/expr_util.h | 5 ----- 2 files changed, 14 deletions(-) diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 001e58ee19c..2ce8c19f086 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -17,15 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "namespace.h" #include "arith_tools.h" -void make_next_state(exprt &expr) -{ - Forall_operands(it, expr) - make_next_state(*it); - - if(expr.id()==ID_symbol) - expr.id(ID_next_symbol); -} - exprt make_binary(const exprt &expr) { const exprt::operandst &operands=expr.operands(); diff --git a/src/util/expr_util.h b/src/util/expr_util.h index e0b1f4aaf26..2a836bebaa1 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -28,11 +28,6 @@ class symbolt; class typet; class namespacet; -/// \deprecated This function will eventually be removed. Use functions -/// from \ref util/std_expr.h instead. - -void make_next_state(exprt &); - /// splits an expression with >=3 operands into nested binary expressions exprt make_binary(const exprt &); From 733f3b8f76592c931f38838892a57bc562c96a2e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 11 Feb 2018 20:26:37 +0000 Subject: [PATCH 4/5] remove old-style constructor for member_exprt --- src/util/std_expr.h | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 42c8811aca9..0191c9593bf 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -3837,11 +3837,6 @@ inline void validate_expr(const array_update_exprt &value) class member_exprt:public unary_exprt { public: - // deprecated, and will go away -- use either of the two below - explicit member_exprt(const typet &_type):unary_exprt(ID_member, _type) - { - } - member_exprt( const exprt &op, const irep_idt &component_name, From 11714b2e7c6e170f5f75ec9209320219881c7898 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 11 Feb 2018 20:33:23 +0000 Subject: [PATCH 5/5] use constant_exprt version of to_integer --- src/util/format_constant.cpp | 2 +- src/util/xml_expr.cpp | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/util/format_constant.cpp b/src/util/format_constant.cpp index 85778504e47..768d103f9b1 100644 --- a/src/util/format_constant.cpp +++ b/src/util/format_constant.cpp @@ -25,7 +25,7 @@ std::string format_constantt::operator()(const exprt &expr) expr.type().id()==ID_signedbv) { mp_integer i; - if(to_integer(expr, i)) + if(to_integer(to_constant_expr(expr), i)) return "(number conversion failed)"; return integer2string(i); diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp index 3b9c8a719ba..319a463b914 100644 --- a/src/util/xml_expr.cpp +++ b/src/util/xml_expr.cpp @@ -159,7 +159,8 @@ xmlt xml( std::size_t width=to_bitvector_type(type).get_width(); result.name="integer"; - result.set_attribute("binary", expr.get_string(ID_value)); + result.set_attribute("binary", + id2string(to_constant_expr(expr).get_value())); result.set_attribute("width", width); const typet &underlying_type= @@ -182,7 +183,7 @@ xmlt xml( result.set_attribute("c_type", sig+"long long int"); mp_integer i; - if(!to_integer(expr, i)) + if(!to_integer(to_constant_expr(expr), i)) result.data=integer2string(i); } else if(type.id()==ID_c_enum) @@ -193,7 +194,7 @@ xmlt xml( result.set_attribute("c_type", "enum"); mp_integer i; - if(!to_integer(expr, i)) + if(!to_integer(to_constant_expr(expr), i)) result.data=integer2string(i); } else if(type.id()==ID_c_enum_tag)