diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index fdbeead99bc..88241eb3e9c 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -650,19 +650,14 @@ void dump_ct::cleanup_decl( std::list &local_static, std::list &local_type_decls) { - exprt value=nil_exprt(); - - if(decl.operands().size()==2) - { - value=decl.op1(); - decl.operands().resize(1); - } - goto_programt tmp; tmp.add(goto_programt::make_decl(decl.symbol())); - if(value.is_not_nil()) - tmp.add(goto_programt::make_assignment(decl.symbol(), value)); + if(optionalt value = decl.initial_value()) + { + decl.set_initial_value({}); + tmp.add(goto_programt::make_assignment(decl.symbol(), std::move(*value))); + } tmp.add(goto_programt::make_end_function()); diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index eb37f44ee2d..379414c0bb3 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -477,7 +477,7 @@ goto_programt::const_targett goto_program2codet::convert_decl( { if(next->is_assign()) { - d.copy_to_operands(next->get_assign().rhs()); + d.set_initial_value({next->get_assign().rhs()}); } else { diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index b352abc987e..b461b7f0c6f 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -199,13 +199,21 @@ class goto_programt const code_declt &get_decl() const { PRECONDITION(is_decl()); - return to_code_decl(code); + const auto &decl = expr_checked_cast(code); + INVARIANT( + !decl.initial_value(), + "code_declt in goto program may not contain initialization."); + return decl; } /// Set the declaration for DECL void set_decl(code_declt c) { PRECONDITION(is_decl()); + INVARIANT( + !c.initial_value(), + "Initialization must be separated from code_declt before adding to " + "goto_instructiont."); code = std::move(c); } diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp index c8ce71ae28b..750100cb7aa 100644 --- a/src/goto-programs/wp.cpp +++ b/src/goto-programs/wp.cpp @@ -226,6 +226,7 @@ exprt wp_decl( const exprt &post, const namespacet &ns) { + PRECONDITION(!code.initial_value()); // Model decl(var) as var = nondet() const exprt &var = code.symbol(); side_effect_expr_nondett nondet(var.type(), source_locationt()); diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index fe6c3eb1689..313eb8b1241 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -354,11 +354,14 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr) { return os << "dead " << format(to_code_dead(code).symbol()) << ";"; } - else if(statement == ID_decl) + else if(const auto decl = expr_try_dynamic_cast(code)) { - const auto &declaration_symb = to_code_decl(code).symbol(); - return os << "decl " << format(declaration_symb.type()) << " " - << format(declaration_symb) << ";"; + const auto &declaration_symb = decl->symbol(); + os << "decl " << format(declaration_symb.type()) << " " + << format(declaration_symb); + if(const optionalt initial_value = decl->initial_value()) + os << " = " << format(*initial_value); + return os << ";"; } else if(statement == ID_function_call) { diff --git a/src/util/std_code.h b/src/util/std_code.h index f27d3189377..ffa1c698e15 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -420,6 +420,38 @@ class code_declt:public codet return symbol().get_identifier(); } + /// Returns the initial value to which the declared variable is initialized, + /// or empty in the case where no initialisation is included. + /// \note: Initial values may be present in the front end but they must be + /// separated into a separate assignment when used in a `goto_instructiont`. + optionalt initial_value() const + { + if(operands().size() < 2) + return {}; + return {op1()}; + } + + /// Sets the value to which this declaration initializes the declared + /// variable. Empty optional maybe passed to remove existing initialisation. + /// \note: Initial values may be present in the front end but they must be + /// separated into a separate assignment when used in a `goto_instructiont`. + void set_initial_value(optionalt initial_value) + { + if(!initial_value) + { + operands().resize(1); + } + else if(operands().size() < 2) + { + PRECONDITION(operands().size() == 1); + add_to_operands(std::move(*initial_value)); + } + else + { + op1() = std::move(*initial_value); + } + } + static void check( const codet &code, const validation_modet vm = validation_modet::INVARIANT) diff --git a/unit/Makefile b/unit/Makefile index ff37116bb75..0a582855351 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -90,6 +90,7 @@ SRC += analyses/ai/ai.cpp \ util/expr.cpp \ util/expr_iterator.cpp \ util/file_util.cpp \ + util/format.cpp \ util/format_number_range.cpp \ util/get_base_name.cpp \ util/graph.cpp \ diff --git a/unit/util/format.cpp b/unit/util/format.cpp new file mode 100644 index 00000000000..caf2d15139b --- /dev/null +++ b/unit/util/format.cpp @@ -0,0 +1,22 @@ +/*******************************************************************\ + + Module: Unit tests for `format` function. + + Author: DiffBlue Limited. + +\*******************************************************************/ + +#include +#include +#include + +#include + +TEST_CASE("Format a declaration statement.", "[core][util][format]") +{ + const signedbv_typet int_type{32}; + code_declt declaration{symbol_exprt{"foo", int_type}}; + REQUIRE(format_to_string(declaration) == "decl signedbv[32] foo;"); + declaration.set_initial_value({int_type.zero_expr()}); + REQUIRE(format_to_string(declaration) == "decl signedbv[32] foo = 0;"); +}