From 5cebbc3cc2308c691f71ef6685998033cd180bc9 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 24 Jul 2017 15:35:50 +0100 Subject: [PATCH] Revert "Improved invariants" --- .travis.yml | 2 +- regression/Makefile | 1 - regression/cbmc/invariant-failure/main.c | 4 + .../invariant-failure/test.desc | 6 +- regression/invariants/.gitignore | 1 - regression/invariants/Makefile | 32 ---- regression/invariants/driver.cpp | 88 ---------- .../invariants/invariant-failure10/test.desc | 13 -- .../invariants/invariant-failure11/test.desc | 12 -- .../invariants/invariant-failure12/test.desc | 13 -- .../invariants/invariant-failure2/test.desc | 13 -- .../invariants/invariant-failure3/test.desc | 12 -- .../invariants/invariant-failure4/test.desc | 13 -- .../invariants/invariant-failure5/test.desc | 12 -- .../invariants/invariant-failure6/test.desc | 13 -- .../invariants/invariant-failure7/test.desc | 12 -- .../invariants/invariant-failure8/test.desc | 13 -- .../invariants/invariant-failure9/test.desc | 12 -- src/cbmc/cbmc_parse_options.cpp | 21 +++ src/cbmc/cbmc_parse_options.h | 1 + src/util/invariant.cpp | 80 +++++---- src/util/invariant.h | 164 +++--------------- 22 files changed, 95 insertions(+), 443 deletions(-) create mode 100644 regression/cbmc/invariant-failure/main.c rename regression/{invariants => cbmc}/invariant-failure/test.desc (62%) delete mode 100644 regression/invariants/.gitignore delete mode 100644 regression/invariants/Makefile delete mode 100644 regression/invariants/driver.cpp delete mode 100644 regression/invariants/invariant-failure10/test.desc delete mode 100644 regression/invariants/invariant-failure11/test.desc delete mode 100644 regression/invariants/invariant-failure12/test.desc delete mode 100644 regression/invariants/invariant-failure2/test.desc delete mode 100644 regression/invariants/invariant-failure3/test.desc delete mode 100644 regression/invariants/invariant-failure4/test.desc delete mode 100644 regression/invariants/invariant-failure5/test.desc delete mode 100644 regression/invariants/invariant-failure6/test.desc delete mode 100644 regression/invariants/invariant-failure7/test.desc delete mode 100644 regression/invariants/invariant-failure8/test.desc delete mode 100644 regression/invariants/invariant-failure9/test.desc diff --git a/.travis.yml b/.travis.yml index 1145190171c..0cf80acccf5 100644 --- a/.travis.yml +++ b/.travis.yml @@ -159,7 +159,7 @@ install: script: - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ; - COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\"" && + COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" && eval ${PRE_COMMAND} ${COMMAND} - COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" && eval ${PRE_COMMAND} ${COMMAND} diff --git a/regression/Makefile b/regression/Makefile index 87dcd7c93f3..b6d109b604a 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -6,7 +6,6 @@ DIRS = ansi-c \ goto-instrument \ goto-instrument-typedef \ goto-diff \ - invariants \ test-script \ # Empty last line 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/invariants/invariant-failure/test.desc b/regression/cbmc/invariant-failure/test.desc similarity index 62% rename from regression/invariants/invariant-failure/test.desc rename to regression/cbmc/invariant-failure/test.desc index 70628a2e064..9966d66547a 100644 --- a/regression/invariants/invariant-failure/test.desc +++ b/regression/cbmc/invariant-failure/test.desc @@ -1,10 +1,8 @@ CORE -dummy_parameter.c -string +main.c +--test-invariant-failure ^EXIT=(0|127|134|137)$ ^SIGNAL=0$ ---- begin invariant violation report --- -Test invariant failure Invariant check failed ^(Backtrace)|(Backtraces not supported)$ -- diff --git a/regression/invariants/.gitignore b/regression/invariants/.gitignore deleted file mode 100644 index e54525b1ee9..00000000000 --- a/regression/invariants/.gitignore +++ /dev/null @@ -1 +0,0 @@ -driver diff --git a/regression/invariants/Makefile b/regression/invariants/Makefile deleted file mode 100644 index b561a960830..00000000000 --- a/regression/invariants/Makefile +++ /dev/null @@ -1,32 +0,0 @@ -default: tests.log - -SRC = driver.cpp - -INCLUDES = -I ../../src - -OBJ += ../../src/util/util$(LIBEXT) - -include ../../src/config.inc -include ../../src/common - -test: driver$(EXEEXT) - @if ! ../test.pl -c ../driver ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi - -tests.log: ../test.pl driver$(EXEEXT) - @if ! ../test.pl -c ../driver ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.c" "$$dir/*.out"; \ - fi; \ - done; - -driver$(EXEEXT): $(OBJ) - $(LINKBIN) diff --git a/regression/invariants/driver.cpp b/regression/invariants/driver.cpp deleted file mode 100644 index 824ae588c03..00000000000 --- a/regression/invariants/driver.cpp +++ /dev/null @@ -1,88 +0,0 @@ -/*******************************************************************\ - -Module: Invariant violation testing - -Author: Chris Smowton, chris.smowton@diffblue.com - -\*******************************************************************/ - -/// \file -/// Invariant violation testing - -#include -#include -#include - -/// An example of structured invariants-- this contains fields to -/// describe the error to a catcher, and also produces a human-readable -/// message containing all the information for use by the current aborting -/// invariant implementation and/or any generic error catcher in the future. -class structured_error_testt: public invariant_failedt -{ - std::string pretty_print(int code, const std::string &desc) - { - std::ostringstream ret; - ret << "Error code: " << code - << "\nDescription: " << desc; - return ret.str(); - } - -public: - const int error_code; - const std::string description; - - structured_error_testt( - const std::string &file, - const std::string &function, - int line, - const std::string &backtrace, - int code, - const std::string &_description): - invariant_failedt( - file, - function, - line, - backtrace, - pretty_print(code, _description)), - error_code(code), - description(_description) - { - } -}; - -/// Causes an invariant failure dependent on first argument value. -/// One ignored argument is accepted to conform with the test.pl script, -/// which would be the input source file for other cbmc driver programs. -/// Returns 1 on unexpected arguments. -int main(int argc, char** argv) -{ - if(argc!=3) - return 1; - std::string arg=argv[1]; - if(arg=="structured") - INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT - else if(arg=="string") - INVARIANT(false, "Test invariant failure"); - else if(arg=="precondition-structured") - PRECONDITION_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT - else if(arg=="precondition-string") - PRECONDITION(false); - else if(arg=="postcondition-structured") - POSTCONDITION_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT - else if(arg=="postcondition-string") - POSTCONDITION(false); - else if(arg=="check-return-structured") - CHECK_RETURN_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT - else if(arg=="check-return-string") - CHECK_RETURN(false); - else if(arg=="unreachable-structured") - UNREACHABLE_STRUCTURED(structured_error_testt, 1, "Structured error"); // NOLINT - else if(arg=="unreachable-string") - UNREACHABLE; - else if(arg=="data-invariant-structured") - DATA_INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT - else if(arg=="data-invariant-string") - DATA_INVARIANT(false, "Test invariant failure"); - else - return 1; -} diff --git a/regression/invariants/invariant-failure10/test.desc b/regression/invariants/invariant-failure10/test.desc deleted file mode 100644 index fae345f2b2a..00000000000 --- a/regression/invariants/invariant-failure10/test.desc +++ /dev/null @@ -1,13 +0,0 @@ -CORE -dummy_parameter.c -unreachable-structured -^EXIT=(0|127|134|137)$ -^SIGNAL=0$ ---- begin invariant violation report --- -Invariant check failed -Error code: 1 -Description: Structured error -^(Backtrace)|(Backtraces not supported)$ --- -^warning: ignoring -^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure11/test.desc b/regression/invariants/invariant-failure11/test.desc deleted file mode 100644 index fc160b21308..00000000000 --- a/regression/invariants/invariant-failure11/test.desc +++ /dev/null @@ -1,12 +0,0 @@ -CORE -dummy_parameter.c -data-invariant-string -^EXIT=(0|127|134|137)$ -^SIGNAL=0$ ---- begin invariant violation report --- -Test invariant failure -Invariant check failed -^(Backtrace)|(Backtraces not supported)$ --- -^warning: ignoring -^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure12/test.desc b/regression/invariants/invariant-failure12/test.desc deleted file mode 100644 index 498af6f2cc5..00000000000 --- a/regression/invariants/invariant-failure12/test.desc +++ /dev/null @@ -1,13 +0,0 @@ -CORE -dummy_parameter.c -data-invariant-structured -^EXIT=(0|127|134|137)$ -^SIGNAL=0$ ---- begin invariant violation report --- -Invariant check failed -Error code: 1 -Description: Structured error -^(Backtrace)|(Backtraces not supported)$ --- -^warning: ignoring -^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure2/test.desc b/regression/invariants/invariant-failure2/test.desc deleted file mode 100644 index daadab22c44..00000000000 --- a/regression/invariants/invariant-failure2/test.desc +++ /dev/null @@ -1,13 +0,0 @@ -CORE -dummy_parameter.c -structured -^EXIT=(0|127|134|137)$ -^SIGNAL=0$ ---- begin invariant violation report --- -Invariant check failed -Error code: 1 -Description: Structured error -^(Backtrace)|(Backtraces not supported)$ --- -^warning: ignoring -^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure3/test.desc b/regression/invariants/invariant-failure3/test.desc deleted file mode 100644 index 42aba0fc5bd..00000000000 --- a/regression/invariants/invariant-failure3/test.desc +++ /dev/null @@ -1,12 +0,0 @@ -CORE -dummy_parameter.c -precondition-string -^EXIT=(0|127|134|137)$ -^SIGNAL=0$ ---- begin invariant violation report --- -Precondition -Invariant check failed -^(Backtrace)|(Backtraces not supported)$ --- -^warning: ignoring -^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure4/test.desc b/regression/invariants/invariant-failure4/test.desc deleted file mode 100644 index 6339338d491..00000000000 --- a/regression/invariants/invariant-failure4/test.desc +++ /dev/null @@ -1,13 +0,0 @@ -CORE -dummy_parameter.c -precondition-structured -^EXIT=(0|127|134|137)$ -^SIGNAL=0$ ---- begin invariant violation report --- -Invariant check failed -Error code: 1 -Description: Structured error -^(Backtrace)|(Backtraces not supported)$ --- -^warning: ignoring -^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure5/test.desc b/regression/invariants/invariant-failure5/test.desc deleted file mode 100644 index f6f6971351f..00000000000 --- a/regression/invariants/invariant-failure5/test.desc +++ /dev/null @@ -1,12 +0,0 @@ -CORE -dummy_parameter.c -postcondition-string -^EXIT=(0|127|134|137)$ -^SIGNAL=0$ ---- begin invariant violation report --- -Postcondition -Invariant check failed -^(Backtrace)|(Backtraces not supported)$ --- -^warning: ignoring -^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure6/test.desc b/regression/invariants/invariant-failure6/test.desc deleted file mode 100644 index 1b83f2630b1..00000000000 --- a/regression/invariants/invariant-failure6/test.desc +++ /dev/null @@ -1,13 +0,0 @@ -CORE -dummy_parameter.c -postcondition-structured -^EXIT=(0|127|134|137)$ -^SIGNAL=0$ ---- begin invariant violation report --- -Invariant check failed -Error code: 1 -Description: Structured error -^(Backtrace)|(Backtraces not supported)$ --- -^warning: ignoring -^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure7/test.desc b/regression/invariants/invariant-failure7/test.desc deleted file mode 100644 index 9b25a5ac5e8..00000000000 --- a/regression/invariants/invariant-failure7/test.desc +++ /dev/null @@ -1,12 +0,0 @@ -CORE -dummy_parameter.c -check-return-string -^EXIT=(0|127|134|137)$ -^SIGNAL=0$ ---- begin invariant violation report --- -Check return value -Invariant check failed -^(Backtrace)|(Backtraces not supported)$ --- -^warning: ignoring -^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure8/test.desc b/regression/invariants/invariant-failure8/test.desc deleted file mode 100644 index 1165b32a25f..00000000000 --- a/regression/invariants/invariant-failure8/test.desc +++ /dev/null @@ -1,13 +0,0 @@ -CORE -dummy_parameter.c -check-return-structured -^EXIT=(0|127|134|137)$ -^SIGNAL=0$ ---- begin invariant violation report --- -Invariant check failed -Error code: 1 -Description: Structured error -^(Backtrace)|(Backtraces not supported)$ --- -^warning: ignoring -^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure9/test.desc b/regression/invariants/invariant-failure9/test.desc deleted file mode 100644 index 38aebd70d61..00000000000 --- a/regression/invariants/invariant-failure9/test.desc +++ /dev/null @@ -1,12 +0,0 @@ -CORE -dummy_parameter.c -unreachable-string -^EXIT=(0|127|134|137)$ -^SIGNAL=0$ ---- begin invariant violation report --- -Unreachable -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 2e21dae825b..b4099967f85 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -106,6 +106,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: diff --git a/src/util/invariant.cpp b/src/util/invariant.cpp index d3f750041a3..5e63639556c 100644 --- a/src/util/invariant.cpp +++ b/src/util/invariant.cpp @@ -12,7 +12,10 @@ Author: Martin Brain, martin.brain@diffblue.com #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 @@ -36,7 +39,7 @@ Author: Martin Brain, martin.brain@diffblue.com /// \return True <=> the entry has been successfully demangled and printed. static bool output_demangled_name( std::ostream &out, - const std::string &stack_entry) + const char * const stack_entry) { bool return_value=false; @@ -72,11 +75,40 @@ static bool output_demangled_name( #endif -/// Prints a back trace to 'out' -/// \param out: Stream to print backtrace -void print_backtrace( - std::ostream &out) +/// 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; @@ -97,39 +129,11 @@ void print_backtrace( #else out << "Backtraces not supported\n" << std::flush; #endif -} -/// Returns a backtrace -/// \return backtrace with a file / function / line header. -std::string get_backtrace() -{ - std::ostringstream ostr; - print_backtrace(ostr); - return ostr.str(); -} - -/// Dump exception report to stderr -void report_exception_to_stderr(const invariant_failedt &reason) -{ - std::cerr << "--- begin invariant violation report ---\n"; - std::cerr << reason.what() << '\n'; - std::cerr << "--- end invariant violation report ---\n"; -} -std::string invariant_failedt::get_invariant_failed_message( - const std::string &file, - const std::string &function, - int line, - const std::string &backtrace, - const std::string &reason) -{ - std::ostringstream out; - out << "Invariant check failed\n" - << "File " << file - << " function " << function - << " line " << line << '\n' - << "Reason: " << reason - << "Backtrace:\n" - << backtrace << '\n'; - return out.str(); +#ifdef CPROVER_INVARIANT_PRINT_STACK_TRACE + abort(); +#else + throw invariant_failedt(out.str()); +#endif } diff --git a/src/util/invariant.h b/src/util/invariant.h index 325020a0d6e..e5bc07b3d5c 100644 --- a/src/util/invariant.h +++ b/src/util/invariant.h @@ -10,9 +10,6 @@ Author: Martin Brain, martin.brain@diffblue.com #define CPROVER_UTIL_INVARIANT_H #include -#include -#include -#include /* ** Invariants document conditions that the programmer believes to @@ -45,7 +42,7 @@ Author: Martin Brain, martin.brain@diffblue.com ** 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 +** invariant is true after it has been executed. Applications are ** encouraged to (at least) catch exceptions at the top level and ** output them. ** @@ -54,64 +51,14 @@ Author: Martin Brain, martin.brain@diffblue.com ** CPROVER_INVARIANT_* macros. */ -/// A logic error, augmented with a distinguished field to hold a backtrace. -/// Classes that extend this one should share the same initial constructor -/// parameters: their constructor signature should be of the form: -/// my_invariantt::my_invariantt( -/// const std::string &file, -/// const std::string &function, -/// int line, -/// const std::string &backtrace, -/// T1 arg1, -/// T2 arg2 ... -/// Tn argn) -/// It should pretty-print the T1 ... Tn arguments and pass it as `reason` to -/// invariant_failedt's constructor, or else simply pass a reason string -/// through. -/// Conforming to this pattern allows the class to be used with the INVARIANT -/// family of macros, allowing constructs like -/// `INVARIANT(x==y, my_invariantt, (T1)actual1, (T2)actual2, ...)` -/// class invariant_failedt: public std::logic_error { - private: - std::string get_invariant_failed_message( - const std::string &file, - const std::string &function, - int line, - const std::string &backtrace, - const std::string &reason); - - public: - - const std::string file; - const std::string function; - const int line; - const std::string backtrace; - const std::string reason; - - invariant_failedt( - const std::string &_file, - const std::string &_function, - int _line, - const std::string &_backtrace, - const std::string &_reason): - logic_error( - get_invariant_failed_message( - _file, - _function, - _line, - _backtrace, - _reason)), - file(_file), - function(_function), - line(_line), - backtrace(_backtrace), - reason(_reason) - { - } +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) \ @@ -123,129 +70,66 @@ class invariant_failedt: public std::logic_error // 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) +#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), true)) - -#else - -void print_backtrace(std::ostream &out); - -std::string get_backtrace(); +#define INVARIANT(CONDITION, REASON) assert((CONDITION) && (REASON)) -void report_exception_to_stderr(const invariant_failedt &); -/// Takes a backtrace, gives it to the reason structure, then aborts, printing -/// reason.what() (which therefore includes the backtrace). -/// In future this may throw `reason` instead of aborting. -/// \param ET : (template type parameter), type of exception to construct -/// \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 params : (variadic) parameters to forward to ET's constructor -/// its backtrace member will be set before it is used. -template -typename std::enable_if::value>::type -invariant_violated_structured( - const std::string &file, - const std::string &function, - const int line, - Params &&... params) -{ - std::string backtrace=get_backtrace(); - ET to_throw(file, function, line, backtrace, std::forward(params)...); - // We now have a structured exception ready to use; - // in future this is the place to put a 'throw'. - report_exception_to_stderr(to_throw); - abort(); -} +#else +// CPROVER_INVARIANT_PRINT_STACK_TRACE affects the implementation of +// this function but not it's generation from the macro -/// Takes a backtrace, constructs an invariant_violatedt from reason and the -/// backtrace, aborts printing the invariant's description. -/// In future this may throw rather than aborting. -/// \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 reason : brief description of the invariant violation. -inline void invariant_violated_string( - const std::string &file, - const std::string &function, +void check_invariant( + const char * const file, + const char * const function, const int line, - const std::string &reason) -{ - invariant_violated_structured( - file, - function, - line, - reason); -} + const bool condition, + const char * const reason); -// These require a trailing semicolon by the user, such that INVARIANT -// behaves syntactically like a function call. -// NOLINT as macro definitions confuse the linter it seems. #ifdef _MSC_VER -#define __this_function__ __FUNCTION__ +#define INVARIANT(CONDITION, REASON) \ + check_invariant(__FILE__, __FUNCTION__, __LINE__, (CONDITION), (REASON)) #else -#define __this_function__ __func__ +#define INVARIANT(CONDITION, REASON) \ + check_invariant(__FILE__, __func__, __LINE__, (CONDITION), (REASON)) #endif -#define INVARIANT(CONDITION, REASON) \ - do /* NOLINT */ \ - { \ - if(!(CONDITION)) \ - invariant_violated_string(__FILE__, __this_function__, __LINE__, (REASON)); /* NOLINT */ \ - } while(0) -#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ - do /* NOLINT */ \ - { \ - if(!(CONDITION)) \ - invariant_violated_structured(__FILE__, __this_function__, __LINE__, __VA_ARGS__); /* NOLINT */ \ - } while(0) +#endif + -#endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block -// Short hand macros. The second variant of each one permits including an -// explanation or structured exception, in which case they are synonyms -// for INVARIANT. +// 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") -#define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) // 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") -#define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) // 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") -#define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) // This should be used to mark dead code #define UNREACHABLE INVARIANT(false, "Unreachable") -#define UNREACHABLE_STRUCTURED(TYPENAME, ...) \ - INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__) // 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) -#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) + // Legacy annotations