From b290a9e030d41aae035ea194e0d27d008cf2d1f9 Mon Sep 17 00:00:00 2001 From: martin Date: Wed, 10 May 2017 19:11:11 +0100 Subject: [PATCH 1/8] A new macro based replacement for assert(). --- src/util/Makefile | 1 + src/util/invariant.cpp | 139 ++++++++++++++++++++++++++++++++++++++++ src/util/invariant.h | 142 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 282 insertions(+) create mode 100644 src/util/invariant.cpp create mode 100644 src/util/invariant.h diff --git a/src/util/Makefile b/src/util/Makefile index ce4489b18ce..d5030ef2a48 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -24,6 +24,7 @@ SRC = arith_tools.cpp \ guard.cpp \ identifier.cpp \ ieee_float.cpp \ + invariant.cpp \ irep.cpp \ irep_hash.cpp \ irep_hash_container.cpp \ diff --git a/src/util/invariant.cpp b/src/util/invariant.cpp new file mode 100644 index 00000000000..b0047cccf40 --- /dev/null +++ b/src/util/invariant.cpp @@ -0,0 +1,139 @@ +/*******************************************************************\ + +Module: + +Author: Martin Brain, martin.brain@diffblue.com + +\*******************************************************************/ + + +#include "invariant.h" + +#include +#include + +#ifdef CPROVER_INVARIANT_PRINT_STACK_TRACE +#include +#include +#endif + +// Backtraces compiler and C library specific +// So we should include something explicitly from the C library +// to check if the C library is glibc. +#include +#ifdef __GLIBC__ + +// GCC needs LINKFLAGS="-rdynamic" to give function names in the backtrace +#include +#include + + +/// Attempts to demangle the function name assuming the glibc +/// format of stack entry: +/// +/// path '(' mangled_name '+' offset ') [' address ']\0' +/// +/// \param out: The output stream +/// \param stack_entry: Description of the stack_entry +/// +/// \return True <=> the entry has been successfully demangled and printed. +static bool output_demangled_name( + std::ostream &out, + const char * const stack_entry) +{ + bool return_value=false; + + std::string working(stack_entry); + + std::string::size_type start=working.rfind('('); // Path may contain '(' ! + std::string::size_type end=working.find('+', start); + + if(start!=std::string::npos && + end!=std::string::npos && + start+1<=end-1) + { + std::string::size_type length=end-(start+1); + std::string mangled(working.substr(start+1, length)); + + int demangle_success=1; + char *demangled= + abi::__cxa_demangle(mangled.c_str(), NULL, 0, &demangle_success); + + if(demangle_success==0) + { + out << working.substr(0, start+1) + << demangled + << working.substr(end); + return_value=true; + } + + free(demangled); + } + + return return_value; +} +#endif + + +/// Checks that the given invariant condition holds and prints a back trace +/// and / or throws an exception depending on build configuration. +/// Does not return if condition is false. +/// Returns with no output or state change if true. +/// +/// \param file : C string giving the name of the file. +/// \param function : C string giving the name of the function. +/// \param line : The line number of the invariant +/// \param condition : The result of evaluating the invariant condition. +/// \param reason : C string giving the reason why the invariant should be true. +void check_invariant( + const char * const file, + const char * const function, + const int line, + const bool condition, + const char * const reason) +{ + if(condition) + return; + +#ifdef CPROVER_INVARIANT_PRINT_STACK_TRACE + std::ostream & out(std::cerr); +#else + std::ostringstream out; +#endif + + // Flush regularly so that errors during output will result in + // partial error logs rather than nothing + out << "Invariant check failed\n" << std::flush; + out << "File " << file + << " function " << function + << " line " << line + << '\n' << std::flush; + +#ifdef __GLIBC__ + out << "Backtrace\n" << std::flush; + + void * stack[50] = {}; + + std::size_t entries=backtrace(stack, sizeof(stack) / sizeof(void *)); + char **description=backtrace_symbols(stack, entries); + + for(std::size_t i=0; i + +/* +** Invariants document conditions that the programmer believes to +** be always true as a consequence of the system architecture and / or +** preceeding code. In principle it should be possible to (machine +** checked) verify them. The condition should be side-effect free and +** evaluate to a boolean. +** +** As well as the condition they have a text argument that should be +** used to say why they are true. The reason should be a string literals. +** Longer diagnostics should be output to error(). For example: +** +** INVARIANT(x > 0, "x negative and zero case handled by other branches"); +** +** To help classify different kinds of invariants, various short-hand +** macros are provided. +** +** Invariants are used to document and check design / implementation +** knowledge. They should *not* be used: +** - to validate user input or options +** (throw an exception or handle more gracefully) +** - to log information (use debug(), progress(), etc.) +** - as TODO notes (acceptable in private repositories but fix before PR) +** - to handle cases that are unlikely, tedious or expensive (ditto) +** - to modify the state of the system (i.e. no side effects) +** +** Invariants provide the following guarantee: +** IF the condition is false +** THEN an invariant_failed exception will be thrown +** OR there will be undefined behaviour +** +** Consequentally, programmers may assume that the condition of an +** invariant is true after it has been executed. Applications are +** encouraged to (at least) catch exceptions at the top level and +** output them. +** +** Various different approaches to checking (or not) the invariants +** and handling their failure are supported and can be configured with +** CPROVER_INVARIANT_* macros. +*/ + +class invariant_failedt: public std::logic_error +{ +public: + explicit invariant_failedt(const std::string& what) : logic_error(what) {} + explicit invariant_failedt(const char* what) : logic_error(what) {} +}; + + +#if defined(CPROVER_INVARIANT_CPROVER_ASSERT) +// Used to allow CPROVER to check itself +#define INVARIANT(CONDITION, REASON) \ + __CPROVER_assert((CONDITION), "Invariant : " REASON) + + +#elif defined(CPROVER_INVARIANT_DO_NOT_CHECK) +// For performance builds, invariants can be ignored +// This is *not* recommended as it can result in unpredictable behaviour +// including silently reporting incorrect results. +// This is also useful for checking side-effect freedom. +#define INVARIANT(CONDITION, REASON) do {} while(0) + + +#elif defined(CPROVER_INVARIANT_ASSERT) +// Not recommended but provided for backwards compatability +#include +// NOLINTNEXTLINE(*) +#define INVARIANT(CONDITION, REASON) assert((CONDITION) && (REASON)) + + +#else +// CPROVER_INVARIANT_PRINT_STACK_TRACE affects the implementation of +// this function but not it's generation from the macro + +void check_invariant( + const char * const file, + const char * const function, + const int line, + const bool condition, + const char * const reason); + +#ifdef _MSC_VER +#define INVARIANT(CONDITION, REASON) \ + check_invariant(__FILE__, __FUNCTION__, __LINE__, (CONDITION), (REASON)) +#else +#define INVARIANT(CONDITION, REASON) \ + check_invariant(__FILE__, __func__, __LINE__, (CONDITION), (REASON)) +#endif + + +#endif + + + +// Short hand macros + +// The condition should only contain (unmodified) arguments to the method. +// "The design of the system means that the arguments to this method +// will always meet this condition". +#define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition") + +// The condition should only contain variables that will be returned / +// output without further modification. +// "The implementation of this method means that the condition will hold". +#define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition") + +// The condition should only contain (unmodified) values that were +// changed by a previous method call. +// "The contract of the previous method call means the following +// condition holds". +#define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value") + +// This should be used to mark dead code +#define UNREACHABLE INVARIANT(false, "Unreachable") + +// This condition should be used to document that assumptions that are +// made on goto_functions, goto_programs, exprts, etc. being well formed. +// "The data structure is corrupt or malformed" +#define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON) + + +// Legacy annotations + +// The following should not be used in new code and are only intended +// to migrate documentation and "error handling" in older code +#define TODO INVARIANT(0, "Todo") +#define UNIMPLEMENTED INVARIANT(0, "Unimplemented") +#define UNHANDLED_CASE INVARIANT(0, "Unhandled case") + +#endif // CPROVER_UTIL_INVARIANT_H From 668dbfaac004eb43de8319c065df21aec0d68b46 Mon Sep 17 00:00:00 2001 From: martin Date: Wed, 10 May 2017 19:12:22 +0100 Subject: [PATCH 2/8] Abnormal termination is no longer an automatic test failure. This allows us to have tests that are intended to abort. Given that tests can (and mostly do) check the exit code this should not reduce the utility of the test system. --- regression/test.pl | 1 - 1 file changed, 1 deletion(-) diff --git a/regression/test.pl b/regression/test.pl index d27c663b0aa..0bf364b86c3 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -35,7 +35,6 @@ ($$$$$) print LOG " Core: $dumped_core\n"; if($signal_num != 0) { - $failed = 1; print "Killed by signal $signal_num"; if($dumped_core) { print " (code dumped)"; From 720e0f8ce7ba2480afca535dcfafab51ff285e8b Mon Sep 17 00:00:00 2001 From: martin Date: Wed, 10 May 2017 19:19:57 +0100 Subject: [PATCH 3/8] Add an (undocumented) option to test out what happens if an invariant fails. --- regression/cbmc/invariant-failure/main.c | 4 ++++ regression/cbmc/invariant-failure/test.desc | 10 ++++++++++ src/cbmc/cbmc_parse_options.cpp | 22 +++++++++++++++++++++ src/cbmc/cbmc_parse_options.h | 1 + 4 files changed, 37 insertions(+) create mode 100644 regression/cbmc/invariant-failure/main.c create mode 100644 regression/cbmc/invariant-failure/test.desc diff --git a/regression/cbmc/invariant-failure/main.c b/regression/cbmc/invariant-failure/main.c new file mode 100644 index 00000000000..f8b643afbf2 --- /dev/null +++ b/regression/cbmc/invariant-failure/main.c @@ -0,0 +1,4 @@ +int main() +{ + return 0; +} diff --git a/regression/cbmc/invariant-failure/test.desc b/regression/cbmc/invariant-failure/test.desc new file mode 100644 index 00000000000..9966d66547a --- /dev/null +++ b/regression/cbmc/invariant-failure/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--test-invariant-failure +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +Invariant check failed +^(Backtrace)|(Backtraces not supported)$ +-- +^warning: ignoring +^VERIFICATION SUCCESSFUL$ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 085672e4237..d2f1c178d8e 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -104,6 +105,27 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) exit(1); // should contemplate EX_USAGE from sysexits.h } + // Test only; do not use for input validation + if(cmdline.isset("test-invariant-failure")) + { + // Have to catch this as the default handling of uncaught exceptions + // on windows appears to be silent termination. + try + { + INVARIANT(0, "Test invariant failure"); + } + catch (const invariant_failedt &e) + { + std::cerr << e.what(); + exit(0); // should contemplate EX_OK from sysexits.h + } + catch (...) + { + error() << "Unexpected exception type\n"; + } + exit(1); + } + if(cmdline.isset("program-only")) options.set_option("program-only", true); diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 4d8e6753476..d95e60eb25b 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -63,6 +63,7 @@ class optionst; "(java-cp-include-files):" \ "(localize-faults)(localize-faults-method):" \ "(lazy-methods)" \ + "(test-invariant-failure)" \ "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) class cbmc_parse_optionst: From 975b5a355006677e2b75e6c961730d42f53dcc10 Mon Sep 17 00:00:00 2001 From: martin Date: Wed, 10 May 2017 20:29:03 +0100 Subject: [PATCH 4/8] Get the linter to check for assertions and give a deprecated warning. --- CODING_STANDARD | 3 +++ regression/cpp-linter/assert/main.cpp | 10 ++++++++++ regression/cpp-linter/assert/test.desc | 6 ++++++ scripts/cpplint.py | 22 ++++++++++++++++++++++ 4 files changed, 41 insertions(+) create mode 100644 regression/cpp-linter/assert/main.cpp create mode 100644 regression/cpp-linter/assert/test.desc diff --git a/CODING_STANDARD b/CODING_STANDARD index ebc2b31f594..0a86fd71b22 100644 --- a/CODING_STANDARD +++ b/CODING_STANDARD @@ -158,6 +158,9 @@ C++ features: - Use the auto keyword if and only if one of the following - The type is explictly repeated on the RHS (e.g. a constructor call) - Adding the type will increase confusion (e.g. iterators, function pointers) +- Avoid assert, if the condition is an actual invariant, use INVARIANT, + PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT. + If there are possible reasons why it might fail, throw an exception. Architecture-specific code: - Avoid if possible. diff --git a/regression/cpp-linter/assert/main.cpp b/regression/cpp-linter/assert/main.cpp new file mode 100644 index 00000000000..cceff0cb2ea --- /dev/null +++ b/regression/cpp-linter/assert/main.cpp @@ -0,0 +1,10 @@ +// Author: Martin Brain, martin.brain@diffblue.com + +#include +#include + +int main(int argc, char **argv) +{ + assert(0); + return 0; +} diff --git a/regression/cpp-linter/assert/test.desc b/regression/cpp-linter/assert/test.desc new file mode 100644 index 00000000000..cda85742156 --- /dev/null +++ b/regression/cpp-linter/assert/test.desc @@ -0,0 +1,6 @@ +CORE +main.cpp + +^main\.cpp:8: assert is deprecated, use INVARIANT instead \[build/deprecated\] \[4\] +^Total errors found: 1$ +^SIGNAL=0$ diff --git a/scripts/cpplint.py b/scripts/cpplint.py index 66fe60a3e04..64fab3758f9 100755 --- a/scripts/cpplint.py +++ b/scripts/cpplint.py @@ -4629,6 +4629,27 @@ def CheckAltTokens(filename, clean_lines, linenum, error): _ALT_TOKEN_REPLACEMENT[match.group(1)], match.group(1))) +def CheckAssert(filename, clean_lines, linenum, error): + """Check for uses of assert. + + Args: + filename: The name of the current file. + clean_lines: A CleansedLines instance containing the file. + linenum: The number of the line to check. + error: The function to call with any errors found. + """ + line = clean_lines.elided[linenum] + match = Match(r'.*\s+assert\(.*\).*', line) + if match: + if Match(r'.*\s+assert\((0|false)\).*', line): + error(filename, linenum, 'build/deprecated', 4, + 'assert is deprecated, use UNREACHABLE instead') + else: + error(filename, linenum, 'build/deprecated', 4, + 'assert is deprecated, use INVARIANT, PRECONDITION, CHECK_RETURN, etc. instead') + + + def GetLineWidth(line): """Determines the width of the line in column positions. @@ -4853,6 +4874,7 @@ def CheckStyle(filename, clean_lines, linenum, file_extension, nesting_state, CheckSpacingForFunctionCall(filename, clean_lines, linenum, error) CheckCheck(filename, clean_lines, linenum, error) CheckAltTokens(filename, clean_lines, linenum, error) + CheckAssert(filename, clean_lines, linenum, error) classinfo = nesting_state.InnermostClass() if classinfo: CheckSectionSpacing(filename, clean_lines, classinfo, linenum, error) From 0a6078806c81e09c15f2070d1fab7b534a54fecf Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 11 May 2017 15:20:34 +0100 Subject: [PATCH 5/8] Remove clashing parts of my previous implementation. --- src/solvers/smt2/smt2_conv.cpp | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index a514a992ecf..11f6b4c5dd1 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -34,7 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com // Mark different kinds of error condition // General -#define UNREACHABLE throw "Supposidly unreachable location reached" #define PARSERERROR(S) throw S // Error checking the expression type @@ -45,7 +45,7 @@ Author: Daniel Kroening, kroening@kroening.com #define UNEXPECTEDCASE(S) throw "Unexpected case: " S // General todos -#define TODO(S) throw "TODO: " S +#define SMT2_TODO(S) throw "TODO: " S void smt2_convt::print_assignment(std::ostream &out) const { @@ -952,7 +952,7 @@ void smt2_convt::convert_expr(const exprt &expr) out << "))"; // mk-, let } else - TODO("bitnot for vectors"); + SMT2_TODO("bitnot for vectors"); } else { @@ -1017,7 +1017,7 @@ void smt2_convt::convert_expr(const exprt &expr) out << "))"; // mk-, let } else - TODO("unary minus for vector"); + SMT2_TODO("unary minus for vector"); } else { @@ -1363,7 +1363,7 @@ void smt2_convt::convert_expr(const exprt &expr) assert(expr.operands().size()==1); out << "false"; // TODO - TODO("pointer_object_has_type not implemented"); + SMT2_TODO("pointer_object_has_type not implemented"); } else if(expr.id()==ID_string_constant) { @@ -1432,7 +1432,7 @@ void smt2_convt::convert_expr(const exprt &expr) convert_expr(tmp); out << ")) bin1)"; // bvlshr, extract, = #endif - TODO("smt2: extractbits with non-constant index"); + SMT2_TODO("smt2: extractbits with non-constant index"); } } else if(expr.id()==ID_replication) @@ -1944,7 +1944,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) // This conversion is non-trivial as it requires creating a // new bit-vector variable and then asserting that it converts // to the required floating-point number. - TODO("bit-wise floatbv to bv"); + SMT2_TODO("bit-wise floatbv to bv"); } else { @@ -2017,7 +2017,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) out << "(_ bv" << i << " " << to_width << ")"; } else - TODO("can't convert non-constant integer to bitvector"); + SMT2_TODO("can't convert non-constant integer to bitvector"); } else if(src_type.id()==ID_struct) // flatten a struct to a bit-vector { @@ -2207,7 +2207,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) } else if(dest_type.id()==ID_range) { - TODO("range typecast"); + SMT2_TODO("range typecast"); } else if(dest_type.id()==ID_floatbv) { @@ -3031,11 +3031,11 @@ void smt2_convt::convert_floatbv_plus(const ieee_float_op_exprt &expr) } else if(type.id()==ID_complex) { - TODO("+ for floatbv complex"); + SMT2_TODO("+ for floatbv complex"); } else if(type.id()==ID_vector) { - TODO("+ for floatbv vector"); + SMT2_TODO("+ for floatbv vector"); } else UNEXPECTEDCASE("unsupported type for +: "+type.id_string()); @@ -3093,7 +3093,7 @@ void smt2_convt::convert_minus(const minus_exprt &expr) } else if(expr.type().id()==ID_pointer) { - TODO("pointer subtraction"); + SMT2_TODO("pointer subtraction"); } else if(expr.type().id()==ID_vector) { @@ -3527,7 +3527,7 @@ void smt2_convt::convert_with(const with_exprt &expr) typecast_exprt index_tc(index, expr_type); // TODO: SMT2-ify - TODO("SMT2-ify"); + SMT2_TODO("SMT2-ify"); out << "(bvor "; out << "(band "; @@ -3565,7 +3565,7 @@ void smt2_convt::convert_update(const exprt &expr) { assert(expr.operands().size()==3); - TODO("smt2_convt::convert_update to be implemented"); + SMT2_TODO("smt2_convt::convert_update to be implemented"); } void smt2_convt::convert_index(const index_exprt &expr) @@ -3651,7 +3651,7 @@ void smt2_convt::convert_index(const index_exprt &expr) mp_integer index_int; if(to_integer(expr.index(), index_int)) { - TODO("non-constant index on vectors"); + SMT2_TODO("non-constant index on vectors"); } else { @@ -3662,7 +3662,7 @@ void smt2_convt::convert_index(const index_exprt &expr) } else { - TODO("index on vectors"); + SMT2_TODO("index on vectors"); } } else From 0560b334b972f5ba3b3bef3256e501e1638d0f52 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 12 May 2017 00:23:06 +0100 Subject: [PATCH 6/8] Convert the assertions in std_expr.h to invariants as a demonstration. Many of these are split into two invariants are there is the specific precondition (before calling to_div_expr it is your responsibility to check you have an exprt with id() == ID_div) and a general data structure invariant (all ID_div exprts should have exactly two operands). A few invariants are commented out as I believe they hold but they are not currently enforced. This commit should not change the functionality of the code. --- src/util/std_expr.h | 517 +++++++++++++++++++++++++++++++++----------- 1 file changed, 394 insertions(+), 123 deletions(-) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 1308daad3e4..c81c6d15d8e 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -17,8 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com * \date Sun Jul 31 21:54:44 BST 2011 */ -#include - +#include "invariant.h" #include "std_types.h" /*! \defgroup gr_std_expr Conversion to specific expressions @@ -59,7 +58,10 @@ class transt:public exprt */ inline const transt &to_trans_expr(const exprt &expr) { - assert(expr.id()==ID_trans && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_trans); + DATA_INVARIANT( + expr.operands().size()==3, + "Transition systems must have three operands"); return static_cast(expr); } @@ -68,7 +70,10 @@ inline const transt &to_trans_expr(const exprt &expr) */ inline transt &to_trans_expr(exprt &expr) { - assert(expr.id()==ID_trans && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_trans); + DATA_INVARIANT( + expr.operands().size()==3, + "Transition systems must have three operands"); return static_cast(expr); } @@ -196,7 +201,8 @@ class decorated_symbol_exprt:public symbol_exprt */ inline const symbol_exprt &to_symbol_expr(const exprt &expr) { - assert(expr.id()==ID_symbol && !expr.has_operands()); + PRECONDITION(expr.id()==ID_symbol); + DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands"); return static_cast(expr); } @@ -205,7 +211,8 @@ inline const symbol_exprt &to_symbol_expr(const exprt &expr) */ inline symbol_exprt &to_symbol_expr(exprt &expr) { - assert(expr.id()==ID_symbol && !expr.has_operands()); + PRECONDITION(expr.id()==ID_symbol); + DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands"); return static_cast(expr); } @@ -271,7 +278,9 @@ class unary_exprt:public exprt */ inline const unary_exprt &to_unary_expr(const exprt &expr) { - assert(expr.operands().size()==1); + DATA_INVARIANT( + expr.operands().size()==1, + "Unary expressions must have one operand"); return static_cast(expr); } @@ -280,7 +289,9 @@ inline const unary_exprt &to_unary_expr(const exprt &expr) */ inline unary_exprt &to_unary_expr(exprt &expr) { - assert(expr.operands().size()==1); + DATA_INVARIANT( + expr.operands().size()==1, + "Unary expressions must have one operand"); return static_cast(expr); } @@ -311,7 +322,10 @@ class abs_exprt:public unary_exprt */ inline const abs_exprt &to_abs_expr(const exprt &expr) { - assert(expr.id()==ID_abs && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_abs); + DATA_INVARIANT( + expr.operands().size()==1, + "Absolute value must have one operand"); return static_cast(expr); } @@ -320,7 +334,10 @@ inline const abs_exprt &to_abs_expr(const exprt &expr) */ inline abs_exprt &to_abs_expr(exprt &expr) { - assert(expr.id()==ID_abs && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_abs); + DATA_INVARIANT( + expr.operands().size()==1, + "Absolute value must have one operand"); return static_cast(expr); } @@ -358,7 +375,10 @@ class unary_minus_exprt:public unary_exprt */ inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr) { - assert(expr.id()==ID_unary_minus && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_unary_minus); + DATA_INVARIANT( + expr.operands().size()==1, + "Unary minus must have one operand"); return static_cast(expr); } @@ -367,7 +387,10 @@ inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr) */ inline unary_minus_exprt &to_unary_minus_expr(exprt &expr) { - assert(expr.id()==ID_unary_minus && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_unary_minus); + DATA_INVARIANT( + expr.operands().size()==1, + "Unary minus must have one operand"); return static_cast(expr); } @@ -500,7 +523,9 @@ class binary_exprt:public exprt */ inline const binary_exprt &to_binary_expr(const exprt &expr) { - assert(expr.operands().size()==2); + DATA_INVARIANT( + expr.operands().size()==2, + "Binary expressions must have two operands"); return static_cast(expr); } @@ -509,7 +534,9 @@ inline const binary_exprt &to_binary_expr(const exprt &expr) */ inline binary_exprt &to_binary_expr(exprt &expr) { - assert(expr.operands().size()==2); + DATA_INVARIANT( + expr.operands().size()==2, + "Binary expressions must have two operands"); return static_cast(expr); } @@ -591,7 +618,9 @@ class binary_relation_exprt:public binary_predicate_exprt */ inline const binary_relation_exprt &to_binary_relation_expr(const exprt &expr) { - assert(expr.operands().size()==2); + DATA_INVARIANT( + expr.operands().size()==2, + "Binary relations must have two operands"); return static_cast(expr); } @@ -600,7 +629,9 @@ inline const binary_relation_exprt &to_binary_relation_expr(const exprt &expr) */ inline binary_relation_exprt &to_binary_relation_expr(exprt &expr) { - assert(expr.operands().size()==2); + DATA_INVARIANT( + expr.operands().size()==2, + "Binary relations must have two operands"); return static_cast(expr); } @@ -703,7 +734,10 @@ class plus_exprt:public multi_ary_exprt */ inline const plus_exprt &to_plus_expr(const exprt &expr) { - assert(expr.id()==ID_plus && expr.operands().size()>=2); + PRECONDITION(expr.id()==ID_plus); + DATA_INVARIANT( + expr.operands().size()>=2, + "Plus must have two or more operands"); return static_cast(expr); } @@ -712,7 +746,10 @@ inline const plus_exprt &to_plus_expr(const exprt &expr) */ inline plus_exprt &to_plus_expr(exprt &expr) { - assert(expr.id()==ID_plus && expr.operands().size()>=2); + PRECONDITION(expr.id()==ID_plus); + DATA_INVARIANT( + expr.operands().size()>=2, + "Plus must have two or more operands"); return static_cast(expr); } @@ -745,7 +782,10 @@ class minus_exprt:public binary_exprt */ inline const minus_exprt &to_minus_expr(const exprt &expr) { - assert(expr.id()==ID_minus && expr.operands().size()>=2); + PRECONDITION(expr.id()==ID_minus); + DATA_INVARIANT( + expr.operands().size()>=2, + "Minus must have two or more operands"); return static_cast(expr); } @@ -754,7 +794,10 @@ inline const minus_exprt &to_minus_expr(const exprt &expr) */ inline minus_exprt &to_minus_expr(exprt &expr) { - assert(expr.id()==ID_minus && expr.operands().size()>=2); + PRECONDITION(expr.id()==ID_minus); + DATA_INVARIANT( + expr.operands().size()>=2, + "Minus must have two or more operands"); return static_cast(expr); } @@ -787,7 +830,10 @@ class mult_exprt:public multi_ary_exprt */ inline const mult_exprt &to_mult_expr(const exprt &expr) { - assert(expr.id()==ID_mult && expr.operands().size()>=2); + PRECONDITION(expr.id()==ID_mult); + DATA_INVARIANT( + expr.operands().size()>=2, + "Multiply must have two or more operands"); return static_cast(expr); } @@ -796,7 +842,10 @@ inline const mult_exprt &to_mult_expr(const exprt &expr) */ inline mult_exprt &to_mult_expr(exprt &expr) { - assert(expr.id()==ID_mult && expr.operands().size()>=2); + PRECONDITION(expr.id()==ID_mult); + DATA_INVARIANT( + expr.operands().size()>=2, + "Multiply must have two or more operands"); return static_cast(expr); } @@ -829,7 +878,10 @@ class div_exprt:public binary_exprt */ inline const div_exprt &to_div_expr(const exprt &expr) { - assert(expr.id()==ID_div && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_div); + DATA_INVARIANT( + expr.operands().size()==2, + "Divide must have two operands"); return static_cast(expr); } @@ -838,7 +890,10 @@ inline const div_exprt &to_div_expr(const exprt &expr) */ inline div_exprt &to_div_expr(exprt &expr) { - assert(expr.id()==ID_div && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_div); + DATA_INVARIANT( + expr.operands().size()==2, + "Divide must have two operands"); return static_cast(expr); } @@ -871,7 +926,8 @@ class mod_exprt:public binary_exprt */ inline const mod_exprt &to_mod_expr(const exprt &expr) { - assert(expr.id()==ID_mod && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_mod); + DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands"); return static_cast(expr); } @@ -880,7 +936,8 @@ inline const mod_exprt &to_mod_expr(const exprt &expr) */ inline mod_exprt &to_mod_expr(exprt &expr) { - assert(expr.id()==ID_mod && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_mod); + DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands"); return static_cast(expr); } @@ -913,7 +970,8 @@ class rem_exprt:public binary_exprt */ inline const rem_exprt &to_rem_expr(const exprt &expr) { - assert(expr.id()==ID_rem && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_rem); + DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands"); return static_cast(expr); } @@ -922,7 +980,8 @@ inline const rem_exprt &to_rem_expr(const exprt &expr) */ inline rem_exprt &to_rem_expr(exprt &expr) { - assert(expr.id()==ID_rem && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_rem); + DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands"); return static_cast(expr); } @@ -955,7 +1014,8 @@ class power_exprt:public binary_exprt */ inline const power_exprt &to_power_expr(const exprt &expr) { - assert(expr.id()==ID_power && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_power); + DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands"); return static_cast(expr); } @@ -964,7 +1024,8 @@ inline const power_exprt &to_power_expr(const exprt &expr) */ inline power_exprt &to_power_expr(exprt &expr) { - assert(expr.id()==ID_power && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_power); + DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands"); return static_cast(expr); } @@ -997,7 +1058,10 @@ class factorial_power_exprt:public binary_exprt */ inline const factorial_power_exprt &to_factorial_power_expr(const exprt &expr) { - assert(expr.id()==ID_factorial_power && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_factorial_power); + DATA_INVARIANT( + expr.operands().size()==2, + "Factorial power must have two operands"); return static_cast(expr); } @@ -1006,7 +1070,10 @@ inline const factorial_power_exprt &to_factorial_power_expr(const exprt &expr) */ inline factorial_power_exprt &to_factorial_expr(exprt &expr) { - assert(expr.id()==ID_factorial_power && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_factorial_power); + DATA_INVARIANT( + expr.operands().size()==2, + "Factorial power must have two operands"); return static_cast(expr); } @@ -1037,7 +1104,8 @@ class equal_exprt:public binary_relation_exprt */ inline const equal_exprt &to_equal_expr(const exprt &expr) { - assert(expr.id()==ID_equal && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_equal); + DATA_INVARIANT(expr.operands().size()==2, "Equality must have two operands"); return static_cast(expr); } @@ -1046,7 +1114,8 @@ inline const equal_exprt &to_equal_expr(const exprt &expr) */ inline equal_exprt &to_equal_expr(exprt &expr) { - assert(expr.id()==ID_equal && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_equal); + DATA_INVARIANT(expr.operands().size()==2, "Equality must have two operands"); return static_cast(expr); } @@ -1077,7 +1146,10 @@ class notequal_exprt:public binary_relation_exprt */ inline const notequal_exprt &to_notequal_expr(const exprt &expr) { - assert(expr.id()==ID_notequal && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_notequal); + DATA_INVARIANT( + expr.operands().size()==2, + "Inequality must have two operands"); return static_cast(expr); } @@ -1086,7 +1158,10 @@ inline const notequal_exprt &to_notequal_expr(const exprt &expr) */ inline notequal_exprt &to_notequal_expr(exprt &expr) { - assert(expr.id()==ID_notequal && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_notequal); + DATA_INVARIANT( + expr.operands().size()==2, + "Inequality must have two operands"); return static_cast(expr); } @@ -1153,7 +1228,10 @@ class index_exprt:public exprt */ inline const index_exprt &to_index_expr(const exprt &expr) { - assert(expr.id()==ID_index && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_index); + DATA_INVARIANT( + expr.operands().size()==2, + "Array index must have two operands"); return static_cast(expr); } @@ -1162,7 +1240,10 @@ inline const index_exprt &to_index_expr(const exprt &expr) */ inline index_exprt &to_index_expr(exprt &expr) { - assert(expr.id()==ID_index && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_index); + DATA_INVARIANT( + expr.operands().size()==2, + "Array index must have two operands"); return static_cast(expr); } @@ -1204,7 +1285,10 @@ class array_of_exprt:public unary_exprt */ inline const array_of_exprt &to_array_of_expr(const exprt &expr) { - assert(expr.id()==ID_array_of && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_array_of); + DATA_INVARIANT( + expr.operands().size()==1, + "'Array of' must have one operand"); return static_cast(expr); } @@ -1213,7 +1297,10 @@ inline const array_of_exprt &to_array_of_expr(const exprt &expr) */ inline array_of_exprt &to_array_of_expr(exprt &expr) { - assert(expr.id()==ID_array_of && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_array_of); + DATA_INVARIANT( + expr.operands().size()==1, + "'Array of' must have one operand"); return static_cast(expr); } @@ -1244,7 +1331,7 @@ class array_exprt:public exprt */ inline const array_exprt &to_array_expr(const exprt &expr) { - assert(expr.id()==ID_array); + PRECONDITION(expr.id()==ID_array); return static_cast(expr); } @@ -1253,11 +1340,11 @@ inline const array_exprt &to_array_expr(const exprt &expr) */ inline array_exprt &to_array_expr(exprt &expr) { - assert(expr.id()==ID_array); + PRECONDITION(expr.id()==ID_array); return static_cast(expr); } -/*! \brief array constructor from list of elements +/*! \brief vector constructor from list of elements */ class vector_exprt:public exprt { @@ -1284,7 +1371,7 @@ class vector_exprt:public exprt */ inline const vector_exprt &to_vector_expr(const exprt &expr) { - assert(expr.id()==ID_vector); + PRECONDITION(expr.id()==ID_vector); return static_cast(expr); } @@ -1293,7 +1380,7 @@ inline const vector_exprt &to_vector_expr(const exprt &expr) */ inline vector_exprt &to_vector_expr(exprt &expr) { - assert(expr.id()==ID_vector); + PRECONDITION(expr.id()==ID_vector); return static_cast(expr); } @@ -1353,7 +1440,10 @@ class union_exprt:public unary_exprt */ inline const union_exprt &to_union_expr(const exprt &expr) { - assert(expr.id()==ID_union && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_union); + DATA_INVARIANT( + expr.operands().size()==1, + "Union constructor must have one operand"); return static_cast(expr); } @@ -1362,7 +1452,10 @@ inline const union_exprt &to_union_expr(const exprt &expr) */ inline union_exprt &to_union_expr(exprt &expr) { - assert(expr.id()==ID_union && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_union); + DATA_INVARIANT( + expr.operands().size()==1, + "Union constructor must have one operand"); return static_cast(expr); } @@ -1393,7 +1486,7 @@ class struct_exprt:public exprt */ inline const struct_exprt &to_struct_expr(const exprt &expr) { - assert(expr.id()==ID_struct); + PRECONDITION(expr.id()==ID_struct); return static_cast(expr); } @@ -1402,7 +1495,7 @@ inline const struct_exprt &to_struct_expr(const exprt &expr) */ inline struct_exprt &to_struct_expr(exprt &expr) { - assert(expr.id()==ID_struct); + PRECONDITION(expr.id()==ID_struct); return static_cast(expr); } @@ -1459,7 +1552,10 @@ class complex_exprt:public binary_exprt */ inline const complex_exprt &to_complex_expr(const exprt &expr) { - assert(expr.id()==ID_complex && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_complex); + DATA_INVARIANT( + expr.operands().size()==2, + "Complex constructor must have two operands"); return static_cast(expr); } @@ -1468,7 +1564,10 @@ inline const complex_exprt &to_complex_expr(const exprt &expr) */ inline complex_exprt &to_complex_expr(exprt &expr) { - assert(expr.id()==ID_complex && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_complex); + DATA_INVARIANT( + expr.operands().size()==2, + "Complex constructor must have two operands"); return static_cast(expr); } @@ -1535,7 +1634,10 @@ class object_descriptor_exprt:public exprt inline const object_descriptor_exprt &to_object_descriptor_expr( const exprt &expr) { - assert(expr.id()==ID_object_descriptor && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_object_descriptor); + DATA_INVARIANT( + expr.operands().size()==2, + "Object descriptor must have two operands"); return static_cast(expr); } @@ -1544,7 +1646,10 @@ inline const object_descriptor_exprt &to_object_descriptor_expr( */ inline object_descriptor_exprt &to_object_descriptor_expr(exprt &expr) { - assert(expr.id()==ID_object_descriptor && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_object_descriptor); + DATA_INVARIANT( + expr.operands().size()==2, + "Object descriptor must have two operands"); return static_cast(expr); } @@ -1596,7 +1701,10 @@ class dynamic_object_exprt:public exprt inline const dynamic_object_exprt &to_dynamic_object_expr( const exprt &expr) { - assert(expr.id()==ID_dynamic_object && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_dynamic_object); + DATA_INVARIANT( + expr.operands().size()==2, + "Dynamic object must have two operands"); return static_cast(expr); } @@ -1605,7 +1713,10 @@ inline const dynamic_object_exprt &to_dynamic_object_expr( */ inline dynamic_object_exprt &to_dynamic_object_expr(exprt &expr) { - assert(expr.id()==ID_dynamic_object && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_dynamic_object); + DATA_INVARIANT( + expr.operands().size()==2, + "Dynamic object must have two operands"); return static_cast(expr); } @@ -1648,7 +1759,10 @@ class typecast_exprt:public exprt */ inline const typecast_exprt &to_typecast_expr(const exprt &expr) { - assert(expr.id()==ID_typecast && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_typecast); + DATA_INVARIANT( + expr.operands().size()==1, + "Typecast must have one operand"); return static_cast(expr); } @@ -1657,7 +1771,10 @@ inline const typecast_exprt &to_typecast_expr(const exprt &expr) */ inline typecast_exprt &to_typecast_expr(exprt &expr) { - assert(expr.id()==ID_typecast && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_typecast); + DATA_INVARIANT( + expr.operands().size()==1, + "Typecast must have one operand"); return static_cast(expr); } @@ -1711,7 +1828,10 @@ class floatbv_typecast_exprt:public binary_exprt */ inline const floatbv_typecast_exprt &to_floatbv_typecast_expr(const exprt &expr) { - assert(expr.id()==ID_floatbv_typecast && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_floatbv_typecast); + DATA_INVARIANT( + expr.operands().size()==2, + "Float typecast must have two operands"); return static_cast(expr); } @@ -1720,7 +1840,10 @@ inline const floatbv_typecast_exprt &to_floatbv_typecast_expr(const exprt &expr) */ inline floatbv_typecast_exprt &to_floatbv_typecast_expr(exprt &expr) { - assert(expr.id()==ID_floatbv_typecast && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_floatbv_typecast); + DATA_INVARIANT( + expr.operands().size()==2, + "Float typecast must have two operands"); return static_cast(expr); } @@ -1779,7 +1902,10 @@ exprt conjunction(const exprt::operandst &); */ inline const and_exprt &to_and_expr(const exprt &expr) { - assert(expr.id()==ID_and); + PRECONDITION(expr.id()==ID_and); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "And must have two or more operands"); return static_cast(expr); } @@ -1788,7 +1914,10 @@ inline const and_exprt &to_and_expr(const exprt &expr) */ inline and_exprt &to_and_expr(exprt &expr) { - assert(expr.id()==ID_and); + PRECONDITION(expr.id()==ID_and); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "And must have two or more operands"); return static_cast(expr); } @@ -1819,7 +1948,8 @@ class implies_exprt:public binary_exprt */ inline const implies_exprt &to_implies_expr(const exprt &expr) { - assert(expr.id()==ID_implies && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_implies); + DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands"); return static_cast(expr); } @@ -1828,7 +1958,8 @@ inline const implies_exprt &to_implies_expr(const exprt &expr) */ inline implies_exprt &to_implies_expr(exprt &expr) { - assert(expr.id()==ID_implies && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_implies); + DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands"); return static_cast(expr); } @@ -1887,7 +2018,10 @@ exprt disjunction(const exprt::operandst &); */ inline const or_exprt &to_or_expr(const exprt &expr) { - assert(expr.id()==ID_or); + PRECONDITION(expr.id()==ID_or); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "Or must have two or more operands"); return static_cast(expr); } @@ -1896,7 +2030,10 @@ inline const or_exprt &to_or_expr(const exprt &expr) */ inline or_exprt &to_or_expr(exprt &expr) { - assert(expr.id()==ID_or); + PRECONDITION(expr.id()==ID_or); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "Or must have two or more operands"); return static_cast(expr); } @@ -1943,7 +2080,10 @@ class bitor_exprt:public multi_ary_exprt */ inline const bitor_exprt &to_bitor_expr(const exprt &expr) { - assert(expr.id()==ID_bitor); + PRECONDITION(expr.id()==ID_bitor); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "Bit-wise or must have two or more operands"); return static_cast(expr); } @@ -1952,7 +2092,10 @@ inline const bitor_exprt &to_bitor_expr(const exprt &expr) */ inline bitor_exprt &to_bitor_expr(exprt &expr) { - assert(expr.id()==ID_bitor); + PRECONDITION(expr.id()==ID_bitor); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "Bit-wise or must have two or more operands"); return static_cast(expr); } @@ -1983,7 +2126,10 @@ class bitxor_exprt:public multi_ary_exprt */ inline const bitxor_exprt &to_bitxor_expr(const exprt &expr) { - assert(expr.id()==ID_bitxor); + PRECONDITION(expr.id()==ID_bitxor); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "Bit-wise xor must have two or more operands"); return static_cast(expr); } @@ -1992,7 +2138,10 @@ inline const bitxor_exprt &to_bitxor_expr(const exprt &expr) */ inline bitxor_exprt &to_bitxor_expr(exprt &expr) { - assert(expr.id()==ID_bitxor); + PRECONDITION(expr.id()==ID_bitxor); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "Bit-wise xor must have two or more operands"); return static_cast(expr); } @@ -2024,7 +2173,10 @@ class bitand_exprt:public multi_ary_exprt */ inline const bitand_exprt &to_bitand_expr(const exprt &expr) { - assert(expr.id()==ID_bitand); + PRECONDITION(expr.id()==ID_bitand); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "Bit-wise and must have two or more operands"); return static_cast(expr); } @@ -2033,7 +2185,10 @@ inline const bitand_exprt &to_bitand_expr(const exprt &expr) */ inline bitand_exprt &to_bitand_expr(exprt &expr) { - assert(expr.id()==ID_bitand); + PRECONDITION(expr.id()==ID_bitand); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "Bit-wise and must have two or more operands"); return static_cast(expr); } @@ -2094,7 +2249,9 @@ class shift_exprt:public binary_exprt */ inline const shift_exprt &to_shift_expr(const exprt &expr) { - assert(expr.operands().size()==2); + DATA_INVARIANT( + expr.operands().size()==2, + "Shifts must have two operands"); return static_cast(expr); } @@ -2103,7 +2260,9 @@ inline const shift_exprt &to_shift_expr(const exprt &expr) */ inline shift_exprt &to_shift_expr(exprt &expr) { - assert(expr.operands().size()==2); + DATA_INVARIANT( + expr.operands().size()==2, + "Shifts must have two operands"); return static_cast(expr); } @@ -2221,7 +2380,10 @@ class replication_exprt:public binary_exprt */ inline const replication_exprt &to_replication_expr(const exprt &expr) { - assert(expr.id()==ID_replication && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_replication); + DATA_INVARIANT( + expr.operands().size()==2, + "Bit-wise replication must have two operands"); return static_cast(expr); } @@ -2230,7 +2392,10 @@ inline const replication_exprt &to_replication_expr(const exprt &expr) */ inline replication_exprt &to_replication_expr(exprt &expr) { - assert(expr.id()==ID_replication && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_replication); + DATA_INVARIANT( + expr.operands().size()==2, + "Bit-wise replication must have two operands"); return static_cast(expr); } @@ -2286,7 +2451,10 @@ class extractbit_exprt:public binary_predicate_exprt */ inline const extractbit_exprt &to_extractbit_expr(const exprt &expr) { - assert(expr.id()==ID_extractbit && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_extractbit); + DATA_INVARIANT( + expr.operands().size()==2, + "Extract bit must have two operands"); return static_cast(expr); } @@ -2295,7 +2463,10 @@ inline const extractbit_exprt &to_extractbit_expr(const exprt &expr) */ inline extractbit_exprt &to_extractbit_expr(exprt &expr) { - assert(expr.id()==ID_extractbit && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_extractbit); + DATA_INVARIANT( + expr.operands().size()==2, + "Extract bit must have two operands"); return static_cast(expr); } @@ -2368,7 +2539,10 @@ class extractbits_exprt:public exprt */ inline const extractbits_exprt &to_extractbits_expr(const exprt &expr) { - assert(expr.id()==ID_extractbits && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_extractbits); + DATA_INVARIANT( + expr.operands().size()==3, + "Extract bits must have three operands"); return static_cast(expr); } @@ -2377,7 +2551,10 @@ inline const extractbits_exprt &to_extractbits_expr(const exprt &expr) */ inline extractbits_exprt &to_extractbits_expr(exprt &expr) { - assert(expr.id()==ID_extractbits && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_extractbits); + DATA_INVARIANT( + expr.operands().size()==3, + "Extract bits must have three operands"); return static_cast(expr); } @@ -2421,7 +2598,8 @@ class address_of_exprt:public exprt */ inline const address_of_exprt &to_address_of_expr(const exprt &expr) { - assert(expr.id()==ID_address_of && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_address_of); + DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand"); return static_cast(expr); } @@ -2430,7 +2608,8 @@ inline const address_of_exprt &to_address_of_expr(const exprt &expr) */ inline address_of_exprt &to_address_of_expr(exprt &expr) { - assert(expr.id()==ID_address_of && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_address_of); + DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand"); return static_cast(expr); } @@ -2472,7 +2651,8 @@ class not_exprt:public exprt */ inline const not_exprt &to_not_expr(const exprt &expr) { - assert(expr.id()==ID_not && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_not); + DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand"); return static_cast(expr); } @@ -2481,7 +2661,8 @@ inline const not_exprt &to_not_expr(const exprt &expr) */ inline not_exprt &to_not_expr(exprt &expr) { - assert(expr.id()==ID_not && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_not); + DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand"); return static_cast(expr); } @@ -2536,7 +2717,10 @@ class dereference_exprt:public exprt */ inline const dereference_exprt &to_dereference_expr(const exprt &expr) { - assert(expr.id()==ID_dereference && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_dereference); + DATA_INVARIANT( + expr.operands().size()==1, + "Dereference must have one operand"); return static_cast(expr); } @@ -2545,7 +2729,10 @@ inline const dereference_exprt &to_dereference_expr(const exprt &expr) */ inline dereference_exprt &to_dereference_expr(exprt &expr) { - assert(expr.id()==ID_dereference && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_dereference); + DATA_INVARIANT( + expr.operands().size()==1, + "Dereference must have one operand"); return static_cast(expr); } @@ -2618,7 +2805,10 @@ class if_exprt:public exprt */ inline const if_exprt &to_if_expr(const exprt &expr) { - assert(expr.id()==ID_if && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_if); + DATA_INVARIANT( + expr.operands().size()==3, + "If-then-else must have three operands"); return static_cast(expr); } @@ -2627,7 +2817,10 @@ inline const if_exprt &to_if_expr(const exprt &expr) */ inline if_exprt &to_if_expr(exprt &expr) { - assert(expr.id()==ID_if && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_if); + DATA_INVARIANT( + expr.operands().size()==3, + "If-then-else must have three operands"); return static_cast(expr); } @@ -2695,7 +2888,10 @@ class with_exprt:public exprt */ inline const with_exprt &to_with_expr(const exprt &expr) { - assert(expr.id()==ID_with && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_with); + DATA_INVARIANT( + expr.operands().size()==3, + "Array/structure update must have three operands"); return static_cast(expr); } @@ -2704,7 +2900,10 @@ inline const with_exprt &to_with_expr(const exprt &expr) */ inline with_exprt &to_with_expr(exprt &expr) { - assert(expr.id()==ID_with && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_with); + DATA_INVARIANT( + expr.operands().size()==3, + "Array/structure update must have three operands"); return static_cast(expr); } @@ -2740,7 +2939,10 @@ class index_designatort:public exprt */ inline const index_designatort &to_index_designator(const exprt &expr) { - assert(expr.id()==ID_index_designator && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_index_designator); + DATA_INVARIANT( + expr.operands().size()==1, + "Index designator must have one operand"); return static_cast(expr); } @@ -2749,7 +2951,10 @@ inline const index_designatort &to_index_designator(const exprt &expr) */ inline index_designatort &to_index_designator(exprt &expr) { - assert(expr.id()==ID_index_designator && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_index_designator); + DATA_INVARIANT( + expr.operands().size()==1, + "Index designator must have one operand"); return static_cast(expr); } @@ -2780,7 +2985,10 @@ class member_designatort:public exprt */ inline const member_designatort &to_member_designator(const exprt &expr) { - assert(expr.id()==ID_member_designator && expr.operands().size()==0); + PRECONDITION(expr.id()==ID_member_designator); + DATA_INVARIANT( + !expr.has_operands(), + "Member designator must not have operands"); return static_cast(expr); } @@ -2789,7 +2997,10 @@ inline const member_designatort &to_member_designator(const exprt &expr) */ inline member_designatort &to_member_designator(exprt &expr) { - assert(expr.id()==ID_member_designator && expr.operands().size()==0); + PRECONDITION(expr.id()==ID_member_designator); + DATA_INVARIANT( + !expr.has_operands(), + "Member designator must not have operands"); return static_cast(expr); } @@ -2866,7 +3077,10 @@ class update_exprt:public exprt */ inline const update_exprt &to_update_expr(const exprt &expr) { - assert(expr.id()==ID_update && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_update); + DATA_INVARIANT( + expr.operands().size()==3, + "Array/structure update must have three operands"); return static_cast(expr); } @@ -2875,7 +3089,10 @@ inline const update_exprt &to_update_expr(const exprt &expr) */ inline update_exprt &to_update_expr(exprt &expr) { - assert(expr.id()==ID_update && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_update); + DATA_INVARIANT( + expr.operands().size()==3, + "Array/structure update must have three operands"); return static_cast(expr); } @@ -2942,7 +3159,10 @@ class array_update_exprt:public exprt */ inline const array_update_exprt &to_array_update_expr(const exprt &expr) { - assert(expr.id()==ID_array_update && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_array_update); + DATA_INVARIANT( + expr.operands().size()==3, + "Array update must have three operands"); return static_cast(expr); } @@ -2951,7 +3171,10 @@ inline const array_update_exprt &to_array_update_expr(const exprt &expr) */ inline array_update_exprt &to_array_update_expr(exprt &expr) { - assert(expr.id()==ID_array_update && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_array_update); + DATA_INVARIANT( + expr.operands().size()==3, + "Array update must have three operands"); return static_cast(expr); } #endif @@ -3048,7 +3271,10 @@ class member_exprt:public exprt */ inline const member_exprt &to_member_expr(const exprt &expr) { - assert(expr.id()==ID_member && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_member); + DATA_INVARIANT( + expr.operands().size()==1, + "Extract member must have one operand"); return static_cast(expr); } @@ -3057,7 +3283,10 @@ inline const member_exprt &to_member_expr(const exprt &expr) */ inline member_exprt &to_member_expr(exprt &expr) { - assert(expr.id()==ID_member && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_member); + DATA_INVARIANT( + expr.operands().size()==1, + "Extract member must have one operand"); return static_cast(expr); } @@ -3088,7 +3317,8 @@ class isnan_exprt:public unary_predicate_exprt */ inline const isnan_exprt &to_isnan_expr(const exprt &expr) { - assert(expr.id()==ID_isnan && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_isnan); + DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand"); return static_cast(expr); } @@ -3097,7 +3327,8 @@ inline const isnan_exprt &to_isnan_expr(const exprt &expr) */ inline isnan_exprt &to_isnan_expr(exprt &expr) { - assert(expr.id()==ID_isnan && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_isnan); + DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand"); return static_cast(expr); } @@ -3128,7 +3359,10 @@ class isinf_exprt:public unary_predicate_exprt */ inline const isinf_exprt &to_isinf_expr(const exprt &expr) { - assert(expr.id()==ID_isinf && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_isinf); + DATA_INVARIANT( + expr.operands().size()==1, + "Is infinite must have one operand"); return static_cast(expr); } @@ -3137,7 +3371,10 @@ inline const isinf_exprt &to_isinf_expr(const exprt &expr) */ inline isinf_exprt &to_isinf_expr(exprt &expr) { - assert(expr.id()==ID_isinf && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_isinf); + DATA_INVARIANT( + expr.operands().size()==1, + "Is infinite must have one operand"); return static_cast(expr); } @@ -3168,7 +3405,8 @@ class isfinite_exprt:public unary_predicate_exprt */ inline const isfinite_exprt &to_isfinite_expr(const exprt &expr) { - assert(expr.id()==ID_isfinite && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_isfinite); + DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand"); return static_cast(expr); } @@ -3177,7 +3415,8 @@ inline const isfinite_exprt &to_isfinite_expr(const exprt &expr) */ inline isfinite_exprt &to_isfinite_expr(exprt &expr) { - assert(expr.id()==ID_isfinite && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_isfinite); + DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand"); return static_cast(expr); } @@ -3208,7 +3447,8 @@ class isnormal_exprt:public unary_predicate_exprt */ inline const isnormal_exprt &to_isnormal_expr(const exprt &expr) { - assert(expr.id()==ID_isnormal && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_isnormal); + DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand"); return static_cast(expr); } @@ -3217,7 +3457,8 @@ inline const isnormal_exprt &to_isnormal_expr(const exprt &expr) */ inline isnormal_exprt &to_isnormal_expr(exprt &expr) { - assert(expr.id()==ID_isnormal && expr.operands().size()==1); + PRECONDITION(expr.id()==ID_isnormal); + DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand"); return static_cast(expr); } @@ -3248,7 +3489,10 @@ class ieee_float_equal_exprt:public binary_relation_exprt */ inline const ieee_float_equal_exprt &to_ieee_float_equal_expr(const exprt &expr) { - assert(expr.id()==ID_ieee_float_equal && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_ieee_float_equal); + DATA_INVARIANT( + expr.operands().size()==2, + "IEEE equality must have two operands"); return static_cast(expr); } @@ -3257,11 +3501,14 @@ inline const ieee_float_equal_exprt &to_ieee_float_equal_expr(const exprt &expr) */ inline ieee_float_equal_exprt &to_ieee_float_equal_expr(exprt &expr) { - assert(expr.id()==ID_ieee_float_equal && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_ieee_float_equal); + DATA_INVARIANT( + expr.operands().size()==2, + "IEEE equality must have two operands"); return static_cast(expr); } -/*! \brief IEEE-floating-point disequality +/*! \brief IEEE floating-point disequality */ class ieee_float_notequal_exprt:public binary_relation_exprt { @@ -3290,7 +3537,10 @@ class ieee_float_notequal_exprt:public binary_relation_exprt inline const ieee_float_notequal_exprt &to_ieee_float_notequal_expr( const exprt &expr) { - assert(expr.id()==ID_ieee_float_notequal && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_ieee_float_notequal); + DATA_INVARIANT( + expr.operands().size()==2, + "IEEE inequality must have two operands"); return static_cast(expr); } @@ -3299,11 +3549,14 @@ inline const ieee_float_notequal_exprt &to_ieee_float_notequal_expr( */ inline ieee_float_notequal_exprt &to_ieee_float_notequal_expr(exprt &expr) { - assert(expr.id()==ID_ieee_float_notequal && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_ieee_float_notequal); + DATA_INVARIANT( + expr.operands().size()==2, + "IEEE inequality must have two operands"); return static_cast(expr); } -/*! \brief IEEE-floating-point disequality +/*! \brief IEEE floating-point operations */ class ieee_float_op_exprt:public exprt { @@ -3366,7 +3619,9 @@ class ieee_float_op_exprt:public exprt */ inline const ieee_float_op_exprt &to_ieee_float_op_expr(const exprt &expr) { - assert(expr.operands().size()==3); + DATA_INVARIANT( + expr.operands().size()==3, + "IEEE float operations must have three arguments"); return static_cast(expr); } @@ -3375,7 +3630,9 @@ inline const ieee_float_op_exprt &to_ieee_float_op_expr(const exprt &expr) */ inline ieee_float_op_exprt &to_ieee_float_op_expr(exprt &expr) { - assert(expr.operands().size()==3); + DATA_INVARIANT( + expr.operands().size()==3, + "IEEE float operations must have three arguments"); return static_cast(expr); } @@ -3439,7 +3696,7 @@ class constant_exprt:public exprt */ inline const constant_exprt &to_constant_expr(const exprt &expr) { - assert(expr.id()==ID_constant); + PRECONDITION(expr.id()==ID_constant); return static_cast(expr); } @@ -3448,7 +3705,7 @@ inline const constant_exprt &to_constant_expr(const exprt &expr) */ inline constant_exprt &to_constant_expr(exprt &expr) { - assert(expr.id()==ID_constant); + PRECONDITION(expr.id()==ID_constant); return static_cast(expr); } @@ -3541,7 +3798,10 @@ class function_application_exprt:public exprt inline const function_application_exprt &to_function_application_expr( const exprt &expr) { - assert(expr.id()==ID_function_application && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_function_application); + DATA_INVARIANT( + expr.operands().size()==2, + "Function application must have two operands"); return static_cast(expr); } @@ -3550,7 +3810,10 @@ inline const function_application_exprt &to_function_application_expr( */ inline function_application_exprt &to_function_application_expr(exprt &expr) { - assert(expr.id()==ID_function_application && expr.operands().size()==2); + PRECONDITION(expr.id()==ID_function_application); + DATA_INVARIANT( + expr.operands().size()==2, + "Function application must have two operands"); return static_cast(expr); } @@ -3593,7 +3856,10 @@ class concatenation_exprt:public exprt */ inline const concatenation_exprt &to_concatenation_expr(const exprt &expr) { - assert(expr.id()==ID_concatenation); + PRECONDITION(expr.id()==ID_concatenation); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "Concatenation must have two or more operands"); return static_cast(expr); } @@ -3602,7 +3868,10 @@ inline const concatenation_exprt &to_concatenation_expr(const exprt &expr) */ inline concatenation_exprt &to_concatenation_expr(exprt &expr) { - assert(expr.id()==ID_concatenation); + PRECONDITION(expr.id()==ID_concatenation); + // DATA_INVARIANT( + // expr.operands().size()>=2, + // "Concatenation must have two or more operands"); return static_cast(expr); } @@ -3671,7 +3940,8 @@ class let_exprt:public exprt */ inline const let_exprt &to_let_expr(const exprt &expr) { - assert(expr.id()==ID_let && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_let); + DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands"); return static_cast(expr); } @@ -3680,7 +3950,8 @@ inline const let_exprt &to_let_expr(const exprt &expr) */ inline let_exprt &to_let_expr(exprt &expr) { - assert(expr.id()==ID_let && expr.operands().size()==3); + PRECONDITION(expr.id()==ID_let); + DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands"); return static_cast(expr); } From f77b8433a2372219e1baad86ba61c07ef81da692 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 12 May 2017 00:25:04 +0100 Subject: [PATCH 7/8] Add conversion functions for ID_bitnot. --- src/util/std_expr.h | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index c81c6d15d8e..e2ed2ad433d 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2052,6 +2052,36 @@ class bitnot_exprt:public unary_exprt } }; +/*! \brief Cast a generic exprt to a \ref bitnot_exprt + * + * This is an unchecked conversion. \a expr must be known to be \ref + * bitnot_exprt. + * + * \param expr Source expression + * \return Object of type \ref bitnot_exprt + * + * \ingroup gr_std_expr +*/ +inline const bitnot_exprt &to_bitnot_expr(const exprt &expr) +{ + PRECONDITION(expr.id()==ID_bitnot); + // DATA_INVARIANT(expr.operands().size()==1, + // "Bit-wise not must have one operand"); + return static_cast(expr); +} + +/*! \copydoc to_bitnot_expr(const exprt &) + * \ingroup gr_std_expr +*/ +inline bitnot_exprt &to_bitnot_expr(exprt &expr) +{ + PRECONDITION(expr.id()==ID_bitnot); + // DATA_INVARIANT(expr.operands().size()==1, + // "Bit-wise not must have one operand"); + return static_cast(expr); +} + + /*! \brief Bit-wise OR */ class bitor_exprt:public multi_ary_exprt From cbe7de397fcbf581607303d80bc7067fa9420a58 Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 11 May 2017 20:31:32 +0100 Subject: [PATCH 8/8] Replace assertions in some core libraries. These also serve as examples of which annotations to use. --- src/util/expr.cpp | 12 ++++++------ src/util/expr_util.cpp | 14 +++++++------- src/util/irep.cpp | 23 ++++++++++++++--------- 3 files changed, 27 insertions(+), 22 deletions(-) diff --git a/src/util/expr.cpp b/src/util/expr.cpp index f6b4b0cad4c..cc022538949 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -9,14 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Expression Representation -#include - #include #include "string2int.h" #include "mp_arith.h" #include "fixedbv.h" #include "ieee_float.h" +#include "invariant.h" #include "expr.h" #include "rational.h" #include "rational_tools.h" @@ -203,7 +202,7 @@ void exprt::negate() else { make_nil(); - assert(false); + UNREACHABLE; } } else @@ -211,7 +210,8 @@ void exprt::negate() if(id()==ID_unary_minus) { exprt tmp; - assert(operands().size()==1); + DATA_INVARIANT(operands().size()==1, + "Unary minus must have one operand"); tmp.swap(op0()); swap(tmp); } @@ -245,7 +245,7 @@ bool exprt::is_zero() const { rationalt rat_value; if(to_rational(*this, rat_value)) - assert(false); + CHECK_RETURN(false); return rat_value.is_zero(); } else if(type_id==ID_unsignedbv || @@ -291,7 +291,7 @@ bool exprt::is_one() const { rationalt rat_value; if(to_rational(*this, rat_value)) - assert(false); + CHECK_RETURN(false); return rat_value.is_one(); } else if(type_id==ID_unsignedbv || type_id==ID_signedbv) diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index deab962d7ae..7370b165eab 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -36,14 +36,14 @@ exprt make_binary(const exprt &expr) const typet &type=expr.type(); exprt previous=operands.front(); - assert(previous.type()==type); + PRECONDITION(previous.type()==type); for(exprt::operandst::const_iterator it=++operands.begin(); it!=operands.end(); ++it) { - assert(it->type()==type); + PRECONDITION(it->type()==type); exprt tmp=expr; tmp.operands().clear(); @@ -59,7 +59,7 @@ exprt make_binary(const exprt &expr) with_exprt make_with_expr(const update_exprt &src) { const exprt::operandst &designator=src.designator(); - assert(!designator.empty()); + PRECONDITION(!designator.empty()); with_exprt result; exprt *dest=&result; @@ -78,7 +78,7 @@ with_exprt make_with_expr(const update_exprt &src) // to_member_designator(*it).get_component_name(); } else - assert(false); + UNREACHABLE; *dest=tmp; dest=&to_with_expr(*dest).new_value(); @@ -108,7 +108,7 @@ exprt is_not_zero( src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal; exprt zero=from_integer(0, src_type); - assert(zero.is_not_nil()); + CHECK_RETURN(zero.is_not_nil()); binary_exprt comparison(src, id, zero, bool_typet()); comparison.add_source_location()=src.source_location(); @@ -142,8 +142,8 @@ bool has_subexpr(const exprt &src, const irep_idt &id) if_exprt lift_if(const exprt &src, std::size_t operand_number) { - assert(operand_number #include +#include "invariant.h" + #include "string2int.h" #include "irep.h" #include "string_hash.h" @@ -87,7 +88,7 @@ void irept::detach() remove_ref(old_data); } - assert(data->ref_count==1); + POSTCONDITION(data->ref_count==1); #ifdef IREP_DEBUG std::cout << "DETACH2: " << data << '\n'; @@ -105,7 +106,7 @@ void irept::remove_ref(dt *old_data) nonrecursive_destructor(old_data); #else - assert(old_data->ref_count!=0); + PRECONDITION(old_data->ref_count!=0); #ifdef IREP_DEBUG std::cout << "R: " << old_data << " " << old_data->ref_count << '\n'; @@ -147,7 +148,7 @@ void irept::nonrecursive_destructor(dt *old_data) if(d==&empty_d) continue; - assert(d->ref_count!=0); + INVARIANT(d->ref_count!=0, "All contents of the stack must be in use"); d->ref_count--; if(d->ref_count==0) @@ -456,7 +457,8 @@ bool irept::ordering(const irept &other) const return false; } - assert(it1==X.sub.end() && it2==Y.sub.end()); + INVARIANT(it1==X.sub.end() && it2==Y.sub.end(), + "Unequal lengths will return before this"); } if(X.named_sub.size()