From 584e6c0170aa75807507c4a4d773c6977bc80084 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Mon, 24 Jun 2019 19:17:06 +0100 Subject: [PATCH 1/2] Add `code_inputt` class to wrap around `ID_input` based ireps This commit adds a higher level interface for `ID_input` based ireps. This gives us a central place to document instances of these and a central place to put the code for constructing and checking them. This makes it possible to find documentation about them and avoids duplicating the code for constructing and checking them. --- jbmc/src/java_bytecode/java_entry_point.cpp | 15 ++----- src/ansi-c/ansi_c_entry_point.cpp | 11 +---- src/ansi-c/expr2c.cpp | 2 +- src/cpp/library/cprover.h | 3 +- src/goto-programs/builtin_functions.cpp | 6 +-- src/goto-symex/symex_other.cpp | 2 +- src/pointer-analysis/value_set.cpp | 2 +- src/pointer-analysis/value_set_fi.cpp | 2 +- src/pointer-analysis/value_set_fivr.cpp | 2 +- src/pointer-analysis/value_set_fivrns.cpp | 2 +- src/util/allocate_objects.cpp | 9 +--- src/util/std_code.cpp | 31 ++++++++++++++ src/util/std_code.h | 47 +++++++++++++++++++++ 13 files changed, 94 insertions(+), 40 deletions(-) diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index ee4f50b780f..c8847bb4f09 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -311,7 +311,7 @@ std::pair> java_build_arguments( // we iterate through all the parameters of the function under test, allocate // an object for that parameter (recursively allocating other objects - // necessary to initialize it), and declare such object as an ID_input + // necessary to initialize it), and mark such object using `code_inputt`. for(std::size_t param_number=0; param_number> java_build_arguments( } // record as an input - codet input(ID_input); - input.operands().resize(2); - input.op0()= - address_of_exprt( - index_exprt( - string_constantt(base_name), - from_integer(0, index_type()))); - input.op1()=main_arguments[param_number]; - input.add_source_location()=function.location; - - init_code.add(std::move(input)); + init_code.add( + code_inputt{base_name, main_arguments[param_number], function.location}); } return make_pair(init_code, main_arguments); diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 763de5ed10e..20d48ab1642 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -333,15 +333,8 @@ bool generate_ansi_c_start_function( init_code.add(code_assumet(std::move(le))); } - { - // record argc as an input - codet input(ID_input); - input.operands().resize(2); - input.op0()=address_of_exprt( - index_exprt(string_constantt("argc"), from_integer(0, index_type()))); - input.op1()=argc_symbol.symbol_expr(); - init_code.add(std::move(input)); - } + // record argc as an input + init_code.add(code_inputt{"argc", argc_symbol.symbol_expr()}); if(parameters.size()==3) { diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 6b138d473a2..45ff2f781b4 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -2867,7 +2867,7 @@ std::string expr2ct::convert_code( if(statement==ID_fence) return convert_code_fence(src, indent); - if(statement==ID_input) + if(can_cast_expr(src)) return convert_code_input(src, indent); if(statement==ID_output) diff --git a/src/cpp/library/cprover.h b/src/cpp/library/cprover.h index d4a3b53fc7e..02e28bbd561 100644 --- a/src/cpp/library/cprover.h +++ b/src/cpp/library/cprover.h @@ -22,7 +22,8 @@ void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__)); void __CPROVER_assert(__CPROVER_bool assertion, const char *description); void __CPROVER_precondition(__CPROVER_bool assertion, const char *description); -void __CPROVER_input(const char *id, ...); +// NOLINTNEXTLINE(build/deprecated) +void __CPROVER_input(const char *description, ...); void __CPROVER_output(const char *id, ...); // concurrency-related diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index acb501c1e07..63309ffe925 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -316,10 +316,6 @@ void goto_convertt::do_input( const exprt::operandst &arguments, goto_programt &dest) { - codet input_code(ID_input); - input_code.operands()=arguments; - input_code.add_source_location()=function.source_location(); - if(arguments.size()<2) { error().source_location=function.find_source_location(); @@ -327,7 +323,7 @@ void goto_convertt::do_input( throw 0; } - copy(input_code, OTHER, dest); + copy(code_inputt{arguments, function.source_location()}, OTHER, dest); } void goto_convertt::do_output( diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 829da7a54cb..7476a873c29 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -97,7 +97,7 @@ void goto_symext::symex_other( const codet clean_code = to_code(clean_expr(code, state, false)); symex_printf(state, clean_code); } - else if(statement==ID_input) + else if(can_cast_expr(code)) { const codet clean_code = to_code(clean_expr(code, state, false)); symex_input(state, clean_code); diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 9a2bbf5c3ad..88f1b34e8cb 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1634,7 +1634,7 @@ void value_sett::apply_code_rec( else if(statement==ID_fence) { } - else if(statement==ID_input || statement==ID_output) + else if(can_cast_expr(code) || statement == ID_output) { // doesn't do anything } diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 9037eb147e5..b8a47e09125 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -1400,7 +1400,7 @@ void value_set_fit::apply_code(const codet &code, const namespacet &ns) statement==ID_array_set) { } - else if(statement==ID_input || statement==ID_output) + else if(can_cast_expr(code) || statement == ID_output) { // doesn't do anything } diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index cfe874a0caf..49a76b5e3ab 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -1528,7 +1528,7 @@ void value_set_fivrt::apply_code(const codet &code, const namespacet &ns) assign(lhs, code_return.return_value(), ns); } } - else if(statement==ID_input || statement==ID_output) + else if(can_cast_expr(code) || statement == ID_output) { // doesn't do anything } diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 0ee50e1dfa5..aaa2c7f0758 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -1192,7 +1192,7 @@ void value_set_fivrnst::apply_code(const codet &code, const namespacet &ns) assign(lhs, code_return.return_value(), ns); } } - else if(statement==ID_input || statement==ID_output) + else if(can_cast_expr(code) || statement == ID_output) { // doesn't do anything } diff --git a/src/util/allocate_objects.cpp b/src/util/allocate_objects.cpp index 684dc33d8ba..ba0c129a57f 100644 --- a/src/util/allocate_objects.cpp +++ b/src/util/allocate_objects.cpp @@ -247,13 +247,8 @@ void allocate_objectst::mark_created_symbols_as_input(code_blockt &init_code) // INPUT("", ); for(symbolt const *symbol_ptr : symbols_created) { - codet input_code(ID_input); - input_code.operands().resize(2); - input_code.op0() = address_of_exprt(index_exprt( - string_constantt(symbol_ptr->base_name), from_integer(0, index_type()))); - input_code.op1() = symbol_ptr->symbol_expr(); - input_code.add_source_location() = source_location; - init_code.add(std::move(input_code)); + init_code.add(code_inputt{ + symbol_ptr->base_name, symbol_ptr->symbol_expr(), source_location}); } } diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp index f7bee9327a2..af916245938 100644 --- a/src/util/std_code.cpp +++ b/src/util/std_code.cpp @@ -11,7 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_code.h" +#include "arith_tools.h" +#include "c_types.h" #include "std_expr.h" +#include "string_constant.h" /// If this `codet` is a \ref code_blockt (i.e.\ it represents a block of /// statements), return the unmodified input. Otherwise (i.e.\ the `codet` @@ -167,3 +170,31 @@ void code_function_bodyt::set_parameter_identifiers( sub.back().set(ID_identifier, id); } } + +code_inputt::code_inputt( + std::vector arguments, + optionalt location) + : codet{ID_input, std::move(arguments)} +{ + if(location) + add_source_location() = std::move(*location); + check(*this, validation_modet::INVARIANT); +} + +code_inputt::code_inputt( + const irep_idt &description, + exprt expression, + optionalt location) + : code_inputt{{address_of_exprt(index_exprt( + string_constantt(description), + from_integer(0, index_type()))), + std::move(expression)}, + std::move(location)} +{ +} + +void code_inputt::check(const codet &code, const validation_modet vm) +{ + DATA_CHECK( + vm, code.operands().size() >= 2, "input must have at least two operands"); +} diff --git a/src/util/std_code.h b/src/util/std_code.h index 9c9c1caf901..201a4c4b939 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -631,6 +631,53 @@ inline code_assertt &to_code_assert(codet &code) return ret; } +/// A `codet` representing the declaration that an input of a particular +/// description has a value which corresponds to the value of a given expression +/// (or expressions). +/// When working with the C front end, calls to the `__CPROVER_input` intrinsic +/// can be added to the input code in order add instructions of this type to the +/// goto program. +/// The first argument is expected to be a C string denoting the input +/// identifier. The second argument is the expression for the input value. +class code_inputt : public codet +{ +public: + /// This constructor is for support of calls to `__CPROVER_input` in user + /// code. Where the first first argument is a description which may be any + /// `const char *` and one or more corresponding expression arguments follow. + explicit code_inputt( + std::vector arguments, + optionalt location = {}); + + /// This constructor is intended for generating input instructions as part of + /// synthetic entry point code, rather than as part of user code. + /// \param description: This is used to construct an expression for a pointer + /// to a string constant containing the description text. This expression + /// is then used as the first argument. + /// \param expression: This expression corresponds to a value which should be + /// recorded as an input. + /// \param location: A location to associate with this instruction. + code_inputt( + const irep_idt &description, + exprt expression, + optionalt location = {}); + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT); +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_input); +} + +inline void validate_expr(const code_inputt &input) +{ + code_inputt::check(input); +} + /// Create a fatal assertion, which checks a condition and then halts if it does /// not hold. Equivalent to `ASSERT(condition); ASSUME(condition)`. /// From 061761898a6785826df3d104027532b26b02f185 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 25 Jun 2019 19:47:28 +0100 Subject: [PATCH 2/2] Add `code_outputt` class to wrap around `ID_output` based ireps This commit adds a higher level interface for `ID_output` based ireps. This gives us a central place to document instances of these and a central place to put the code for constructing and checking them. This makes it possible to find documentation about them and avoids duplicating the code for constructing and checking them. --- jbmc/src/java_bytecode/java_entry_point.cpp | 32 ++++---------- jbmc/src/java_bytecode/java_entry_point.h | 4 +- src/ansi-c/ansi_c_entry_point.cpp | 17 ++------ src/ansi-c/expr2c.cpp | 2 +- src/cpp/library/cprover.h | 3 +- src/goto-programs/builtin_functions.cpp | 6 +-- src/goto-programs/interpreter.cpp | 2 +- src/goto-symex/symex_other.cpp | 2 +- src/pointer-analysis/value_set.cpp | 2 +- src/pointer-analysis/value_set_fi.cpp | 2 +- src/pointer-analysis/value_set_fivr.cpp | 2 +- src/pointer-analysis/value_set_fivrns.cpp | 2 +- src/util/std_code.cpp | 28 +++++++++++++ src/util/std_code.h | 46 +++++++++++++++++++++ 14 files changed, 96 insertions(+), 54 deletions(-) diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index c8847bb4f09..9692933627f 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -458,13 +458,8 @@ static optionalt record_return_value( const symbolt &return_symbol = symbol_table.lookup_ref(JAVA_ENTRY_POINT_RETURN_SYMBOL); - codet output(ID_output); - output.operands().resize(2); - output.op0() = address_of_exprt(index_exprt( - string_constantt(return_symbol.base_name), from_integer(0, index_type()))); - output.op1() = return_symbol.symbol_expr(); - output.add_source_location() = function.location; - return output; + return code_outputt{ + return_symbol.base_name, return_symbol.symbol_expr(), function.location}; } static code_blockt record_pointer_parameters( @@ -486,14 +481,8 @@ static code_blockt record_pointer_parameters( if(!can_cast_type(p_symbol.type)) continue; - codet output(ID_output); - output.operands().resize(2); - output.op0() = address_of_exprt(index_exprt( - string_constantt(p_symbol.base_name), from_integer(0, index_type()))); - output.op1() = arguments[param_number]; - output.add_source_location() = function.location; - - init_code.add(std::move(output)); + init_code.add(code_outputt{ + p_symbol.base_name, arguments[param_number], function.location}); } return init_code; } @@ -502,20 +491,13 @@ static codet record_exception( const symbolt &function, const symbol_table_baset &symbol_table) { - // record exceptional return variable as output - codet output(ID_output); - output.operands().resize(2); - // retrieve the exception variable const symbolt &exc_symbol = symbol_table.lookup_ref(JAVA_ENTRY_POINT_EXCEPTION_SYMBOL); - output.op0()=address_of_exprt( - index_exprt(string_constantt(exc_symbol.base_name), - from_integer(0, index_type()))); - output.op1()=exc_symbol.symbol_expr(); - output.add_source_location()=function.location; - return output; + // record exceptional return variable as output + return code_outputt{ + exc_symbol.base_name, exc_symbol.symbol_expr(), function.location}; } main_function_resultt get_main_symbol( diff --git a/jbmc/src/java_bytecode/java_entry_point.h b/jbmc/src/java_bytecode/java_entry_point.h index 29303a08d59..945532e1aa2 100644 --- a/jbmc/src/java_bytecode/java_entry_point.h +++ b/jbmc/src/java_bytecode/java_entry_point.h @@ -33,8 +33,8 @@ using build_argumentst = /// /// 1. Allocates and initializes the parameters of the method under test. /// 2. Call it and save its return variable in the variable 'return'. -/// 3. Declare variable 'return' as an output variable (codet with id -/// ID_output), together with other objects possibly altered by the execution +/// 3. Declare variable 'return' as an output variable using a `code_outputt`, +/// together with other objects possibly altered by the execution of /// the method under test (in `java_record_outputs`) /// /// When \p assume_init_pointers_not_null is false, the generated parameter diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 20d48ab1642..05426f8b5e2 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -59,22 +59,11 @@ void record_function_outputs( if(has_return_value) { - // record return value - codet output(ID_output); - output.operands().resize(2); - const symbolt &return_symbol = symbol_table.lookup_ref("return'"); - output.op0()= - address_of_exprt( - index_exprt( - string_constantt(return_symbol.base_name), - from_integer(0, index_type()))); - - output.op1()=return_symbol.symbol_expr(); - output.add_source_location()=function.location; - - init_code.add(std::move(output)); + // record return value + init_code.add(code_outputt{ + return_symbol.base_name, return_symbol.symbol_expr(), function.location}); } #if 0 diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 45ff2f781b4..722bd74ffcf 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -2870,7 +2870,7 @@ std::string expr2ct::convert_code( if(can_cast_expr(src)) return convert_code_input(src, indent); - if(statement==ID_output) + if(can_cast_expr(src)) return convert_code_output(src, indent); if(statement==ID_assume) diff --git a/src/cpp/library/cprover.h b/src/cpp/library/cprover.h index 02e28bbd561..82d909fb275 100644 --- a/src/cpp/library/cprover.h +++ b/src/cpp/library/cprover.h @@ -24,7 +24,8 @@ void __CPROVER_precondition(__CPROVER_bool assertion, const char *description); // NOLINTNEXTLINE(build/deprecated) void __CPROVER_input(const char *description, ...); -void __CPROVER_output(const char *id, ...); +// NOLINTNEXTLINE(build/deprecated) +void __CPROVER_output(const char *description, ...); // concurrency-related void __CPROVER_atomic_begin(); diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 63309ffe925..025ac24f0ac 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -331,10 +331,6 @@ void goto_convertt::do_output( const exprt::operandst &arguments, goto_programt &dest) { - codet output_code(ID_output); - output_code.operands()=arguments; - output_code.add_source_location()=function.source_location(); - if(arguments.size()<2) { error().source_location=function.find_source_location(); @@ -342,7 +338,7 @@ void goto_convertt::do_output( throw 0; } - copy(output_code, OTHER, dest); + copy(code_outputt{arguments, function.source_location()}, OTHER, dest); } void goto_convertt::do_atomic_begin( diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 9d33d88451e..b51ad3537ad 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -408,7 +408,7 @@ void interpretert::execute_other() assign(address, rhs); } } - else if(statement==ID_output) + else if(can_cast_expr(pc->get_other())) { return; } diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 7476a873c29..2239878146d 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -102,7 +102,7 @@ void goto_symext::symex_other( const codet clean_code = to_code(clean_expr(code, state, false)); symex_input(state, clean_code); } - else if(statement==ID_output) + else if(can_cast_expr(code)) { const codet clean_code = to_code(clean_expr(code, state, false)); symex_output(state, clean_code); diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 88f1b34e8cb..87be2303a0f 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1634,7 +1634,7 @@ void value_sett::apply_code_rec( else if(statement==ID_fence) { } - else if(can_cast_expr(code) || statement == ID_output) + else if(can_cast_expr(code) || can_cast_expr(code)) { // doesn't do anything } diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index b8a47e09125..5a991ee8b71 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -1400,7 +1400,7 @@ void value_set_fit::apply_code(const codet &code, const namespacet &ns) statement==ID_array_set) { } - else if(can_cast_expr(code) || statement == ID_output) + else if(can_cast_expr(code) || can_cast_expr(code)) { // doesn't do anything } diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index 49a76b5e3ab..36839c3f601 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -1528,7 +1528,7 @@ void value_set_fivrt::apply_code(const codet &code, const namespacet &ns) assign(lhs, code_return.return_value(), ns); } } - else if(can_cast_expr(code) || statement == ID_output) + else if(can_cast_expr(code) || can_cast_expr(code)) { // doesn't do anything } diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index aaa2c7f0758..4d9494458de 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -1192,7 +1192,7 @@ void value_set_fivrnst::apply_code(const codet &code, const namespacet &ns) assign(lhs, code_return.return_value(), ns); } } - else if(can_cast_expr(code) || statement == ID_output) + else if(can_cast_expr(code) || can_cast_expr(code)) { // doesn't do anything } diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp index af916245938..32187987301 100644 --- a/src/util/std_code.cpp +++ b/src/util/std_code.cpp @@ -198,3 +198,31 @@ void code_inputt::check(const codet &code, const validation_modet vm) DATA_CHECK( vm, code.operands().size() >= 2, "input must have at least two operands"); } + +code_outputt::code_outputt( + std::vector arguments, + optionalt location) + : codet{ID_output, std::move(arguments)} +{ + if(location) + add_source_location() = std::move(*location); + check(*this, validation_modet::INVARIANT); +} + +code_outputt::code_outputt( + const irep_idt &description, + exprt expression, + optionalt location) + : code_outputt{{address_of_exprt(index_exprt( + string_constantt(description), + from_integer(0, index_type()))), + std::move(expression)}, + std::move(location)} +{ +} + +void code_outputt::check(const codet &code, const validation_modet vm) +{ + DATA_CHECK( + vm, code.operands().size() >= 2, "output must have at least two operands"); +} diff --git a/src/util/std_code.h b/src/util/std_code.h index 201a4c4b939..4d7d1299c94 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -678,6 +678,52 @@ inline void validate_expr(const code_inputt &input) code_inputt::check(input); } +/// A `codet` representing the declaration that an output of a particular +/// description has a value which corresponds to the value of a given expression +/// (or expressions). +/// When working with the C front end, calls to the `__CPROVER_output` intrinsic +/// can be added to the input code in order add instructions of this type to the +/// goto program. +/// The first argument is expected to be a C string denoting the output +/// identifier. The second argument is the expression for the output value. +class code_outputt : public codet +{ +public: + /// This constructor is for support of calls to `__CPROVER_output` in user + /// code. Where the first first argument is a description which may be any + /// `const char *` and one or more corresponding expression arguments follow. + explicit code_outputt( + std::vector arguments, + optionalt location = {}); + + /// This constructor is intended for generating output instructions as part of + /// synthetic entry point code, rather than as part of user code. + /// \param description: This is used to construct an expression for a pointer + /// to a string constant containing the description text. + /// \param expression: This expression corresponds to a value which should be + /// recorded as an output. + /// \param location: A location to associate with this instruction. + code_outputt( + const irep_idt &description, + exprt expression, + optionalt location = {}); + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT); +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_output); +} + +inline void validate_expr(const code_outputt &output) +{ + code_outputt::check(output); +} + /// Create a fatal assertion, which checks a condition and then halts if it does /// not hold. Equivalent to `ASSERT(condition); ASSUME(condition)`. ///