From 5e89759b594b786dd03c2ec2fc77733c25cdb3d6 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 1 Dec 2021 00:52:16 +0000 Subject: [PATCH 1/9] Adding support for check enable pragmas in the ansi-c lexer and parser Adding enable and disable pragmas for a same check at a same pragma stack level triggers an error. Enable and disable pragmas for a same check in different stack levels is allowed, and shadowing is managed when flattening the stack. --- src/ansi-c/ansi_c_parser.cpp | 53 ++++++++++++++++++++++++++++++++++++ src/ansi-c/ansi_c_parser.h | 36 ++++++++++++++++-------- src/ansi-c/scanner.l | 28 +++++++++++-------- 3 files changed, 94 insertions(+), 23 deletions(-) diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp index 61d2825e662..0ea0a6c5790 100644 --- a/src/ansi-c/ansi_c_parser.cpp +++ b/src/ansi-c/ansi_c_parser.cpp @@ -175,3 +175,56 @@ ansi_c_id_classt ansi_c_parsert::get_class(const typet &type) return ansi_c_id_classt::ANSI_C_SYMBOL; } + +bool ansi_c_parsert::pragma_cprover_empty() +{ + return pragma_cprover_stack.empty(); +} + +void ansi_c_parsert::pragma_cprover_push() +{ + pragma_cprover_stack.emplace_back(); +} + +void ansi_c_parsert::pragma_cprover_pop() +{ + pragma_cprover_stack.pop_back(); +} + +void ansi_c_parsert::pragma_cprover_add_check( + const irep_idt &name, + bool enabled) +{ + if(pragma_cprover_stack.empty()) + pragma_cprover_push(); + + pragma_cprover_stack.back()[name] = enabled; +} + +bool ansi_c_parsert::pragma_cprover_clash(const irep_idt &name, bool enabled) +{ + auto top = pragma_cprover_stack.back(); + auto found = top.find(name); + return found != top.end() && found->second != enabled; +} + +void ansi_c_parsert::set_pragma_cprover() +{ + // handle enable/disable shadowing + // by bottom-to-top flattening + std::map flattened; + + for(const auto &pragma_set : pragma_cprover_stack) + for(const auto &pragma : pragma_set) + flattened[pragma.first] = pragma.second; + + source_location.remove(ID_pragma); + + for(const auto &pragma : flattened) + { + std::string check_name = id2string(pragma.first); + std::string full_name = + (pragma.second ? "enable:" : "disable:") + check_name; + source_location.add_pragma(full_name); + } +} diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h index 2427a8b15a3..3573380530e 100644 --- a/src/ansi-c/ansi_c_parser.h +++ b/src/ansi-c/ansi_c_parser.h @@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANSI_C_ANSI_C_PARSER_H #define CPROVER_ANSI_C_ANSI_C_PARSER_H -#include +#include #include #include @@ -53,7 +53,7 @@ class ansi_c_parsert:public parsert parenthesis_counter=0; string_literal.clear(); pragma_pack.clear(); - pragma_cprover.clear(); + pragma_cprover_stack.clear(); // set up global scope scopes.clear(); @@ -66,7 +66,6 @@ class ansi_c_parsert:public parsert unsigned parenthesis_counter; std::string string_literal; std::list pragma_pack; - std::list> pragma_cprover; typedef configt::ansi_ct::flavourt modet; modet mode; @@ -143,15 +142,28 @@ class ansi_c_parsert:public parsert return identifier; } - void set_pragma_cprover() - { - source_location.remove(ID_pragma); - for(const auto &pragma_set : pragma_cprover) - { - for(const auto &pragma : pragma_set) - source_location.add_pragma(pragma); - } - } + /// \brief True iff the CPROVER pragma stack is empty + bool pragma_cprover_empty(); + + /// \brief Pushes an empty level in the CPROVER pragma stack + void pragma_cprover_push(); + + /// \brief Pops a level in the CPROVER pragma stack + void pragma_cprover_pop(); + + /// \brief Adds a check to the CPROVER pragma stack + void pragma_cprover_add_check(const irep_idt &name, bool enabled); + + /// Returns true iff the same check with polarity + /// is already present at top of the stack + bool pragma_cprover_clash(const irep_idt &name, bool enabled); + + /// \brief Tags \ref source_location with + /// the current CPROVER pragma stack + void set_pragma_cprover(); + +private: + std::list> pragma_cprover_stack; }; extern ansi_c_parsert ansi_c_parser; diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 295988fdf6f..55707814272 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -235,9 +235,10 @@ CPROVER_PREFIX "__CPROVER_" arith_check ("conversion"|"undefined-shift"|"nan"|"div-by-zero") enum_check "enum-range" pointer_primitive "pointer-primitive" -memory_check ("bounds"|"pointer"|"memory_leak") +memory_check ("bounds"|"pointer"|"memory-leak") overflow_check ("signed"|"unsigned"|"pointer"|"float")"-overflow" named_check ["]({arith_check}|{enum_check}|{memory_check}|{overflow_check}|{pointer_primitive})["] +enable_or_disable ("enable"|"disable") %x GRAMMAR %x COMMENT1 @@ -402,26 +403,31 @@ void ansi_c_scanner_init() /* CProver specific pragmas: hint to disable named checks */ {ws}"check"{ws}"push" { - PARSER.pragma_cprover.push_back({}); + PARSER.pragma_cprover_push(); } {ws}"check"{ws}"pop" { - if(!PARSER.pragma_cprover.empty()) + if(!PARSER.pragma_cprover_empty()) { - PARSER.pragma_cprover.pop_back(); + PARSER.pragma_cprover_pop(); PARSER.set_pragma_cprover(); } } -{ws}"check"{ws}"disable"{ws}{named_check} { +{ws}"check"{ws}{enable_or_disable}{ws}{named_check} { std::string tmp(yytext); + bool enable = tmp.find("enable")!=std::string::npos; std::string::size_type p = tmp.find('"') + 1; - std::string value = - std::string("disable:") + + std::string check_name = std::string(tmp, p, tmp.size() - p - 1) + std::string("-check"); - if(PARSER.pragma_cprover.empty()) - PARSER.pragma_cprover.push_back({value}); - else - PARSER.pragma_cprover.back().insert(value); + bool clash = PARSER.pragma_cprover_clash(check_name, enable); + if(clash) + { + yyansi_cerror( + "Found enable and disable pragmas for " + + id2string(check_name)); + return TOK_SCANNER_ERROR; + } + PARSER.pragma_cprover_add_check(check_name, enable); PARSER.set_pragma_cprover(); } From 4337f3878ec8765a65a2aa22fcebbd1a6349a643 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 1 Dec 2021 01:01:55 +0000 Subject: [PATCH 2/9] Adds a message_handlert to goto_check functions and goto_checkt. No change in behaviour expected. No need for specific tests. --- .../src/janalyzer/janalyzer_parse_options.cpp | 6 ++++- jbmc/src/jbmc/jbmc_parse_options.cpp | 6 ++++- jbmc/src/jdiff/jdiff_parse_options.cpp | 2 +- src/analyses/goto_check.cpp | 24 ++++++++++++------- src/analyses/goto_check.h | 10 +++++--- .../goto_instrument_parse_options.cpp | 2 +- src/goto-programs/process_goto_program.cpp | 2 +- 7 files changed, 35 insertions(+), 17 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index ca98361eafc..01b8fb82d14 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -705,7 +705,11 @@ void janalyzer_parse_optionst::process_goto_function( // add generic checks goto_check( - function.get_function_id(), function.get_goto_function(), ns, options); + function.get_function_id(), + function.get_goto_function(), + ns, + options, + ui_message_handler); } bool janalyzer_parse_optionst::can_generate_function_body(const irep_idt &name) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index af93b90a4f2..c6760d23736 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -812,7 +812,11 @@ void jbmc_parse_optionst::process_goto_function( // add generic checks goto_check( - function.get_function_id(), function.get_goto_function(), ns, options); + function.get_function_id(), + function.get_goto_function(), + ns, + options, + ui_message_handler); // Replace Java new side effects remove_java_new( diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index b193091ffee..0d132384342 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -278,7 +278,7 @@ bool jdiff_parse_optionst::process_goto_program( // add generic checks log.status() << "Generic Property Instrumentation" << messaget::eom; - goto_check(options, goto_model); + goto_check(options, goto_model, ui_message_handler); // checks don't know about adjusted float expressions adjust_float_expressions(goto_model); diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 1bdb812a092..a27106b38c9 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -48,9 +49,9 @@ class goto_checkt public: goto_checkt( const namespacet &_ns, - const optionst &_options): - ns(_ns), - local_bitvector_analysis(nullptr) + const optionst &_options, + message_handlert &_message_handler) + : ns(_ns), local_bitvector_analysis(nullptr), log(_message_handler) { no_enum_check = false; enable_bounds_check=_options.get_bool_option("bounds-check"); @@ -99,6 +100,8 @@ class goto_checkt std::unique_ptr local_bitvector_analysis; goto_programt::const_targett current_target; guard_managert guard_manager; + messaget log; + bool no_enum_check; /// Check an address-of expression: @@ -2378,18 +2381,20 @@ void goto_check( const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, - const optionst &options) + const optionst &options, + message_handlert &message_handler) { - goto_checkt goto_check(ns, options); + goto_checkt goto_check(ns, options, message_handler); goto_check.goto_check(function_identifier, goto_function); } void goto_check( const namespacet &ns, const optionst &options, - goto_functionst &goto_functions) + goto_functionst &goto_functions, + message_handlert &message_handler) { - goto_checkt goto_check(ns, options); + goto_checkt goto_check(ns, options, message_handler); goto_check.collect_allocations(goto_functions); @@ -2401,8 +2406,9 @@ void goto_check( void goto_check( const optionst &options, - goto_modelt &goto_model) + goto_modelt &goto_model, + message_handlert &message_handler) { const namespacet ns(goto_model.symbol_table); - goto_check(ns, options, goto_model.goto_functions); + goto_check(ns, options, goto_model.goto_functions, message_handler); } diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index 58f4a20696f..f214cfbdc4d 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -17,21 +17,25 @@ Author: Daniel Kroening, kroening@kroening.com class goto_modelt; class namespacet; class optionst; +class message_handlert; void goto_check( const namespacet &ns, const optionst &options, - goto_functionst &goto_functions); + goto_functionst &goto_functions, + message_handlert &message_handler); void goto_check( const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, - const optionst &options); + const optionst &options, + message_handlert &message_handler); void goto_check( const optionst &options, - goto_modelt &goto_model); + goto_modelt &goto_model, + message_handlert &message_handler); #define OPT_GOTO_CHECK \ "(bounds-check)(pointer-check)(memory-leak-check)" \ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 8bc4ff2b7a7..ccc9d3a1b65 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1332,7 +1332,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() } // add generic checks, if needed - goto_check(options, goto_model); + goto_check(options, goto_model, ui_message_handler); // check for uninitalized local variables if(cmdline.isset("uninitialized-check")) diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp index 68121ab9335..0252e121125 100644 --- a/src/goto-programs/process_goto_program.cpp +++ b/src/goto-programs/process_goto_program.cpp @@ -66,7 +66,7 @@ bool process_goto_program( // add generic checks log.status() << "Generic Property Instrumentation" << messaget::eom; - goto_check(options, goto_model); + goto_check(options, goto_model, log.get_message_handler()); // checks don't know about adjusted float expressions adjust_float_expressions(goto_model); From dc6daa886d636ba4efc6ea757dba309f0eec1fdc Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 1 Dec 2021 01:04:38 +0000 Subject: [PATCH 3/9] collect_allocations is now always on. Needed so that the data required to express pointer checks is always available to process a enable pragmas. --- src/analyses/goto_check.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index a27106b38c9..076c3da0c5b 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -292,12 +292,6 @@ class goto_checkt void goto_checkt::collect_allocations( const goto_functionst &goto_functions) { - if( - !enable_pointer_check && !enable_bounds_check && - !enable_pointer_overflow_check) - { - return; - } for(const auto &gf_entry : goto_functions.function_map) { From d59448dae8d1cf651665d770379db0427e6e3957 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 1 Dec 2021 01:21:49 +0000 Subject: [PATCH 4/9] Adding extra logic to flat_resett to detect and trigger errors on double updates with opposite values. --- src/analyses/goto_check.cpp | 35 ++++++++++++++++++++++++++++------- 1 file changed, 28 insertions(+), 7 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 076c3da0c5b..2d9a96272f2 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1848,22 +1848,42 @@ optionalt goto_checkt::rw_ok_check(exprt expr) return {}; } -/// Set a Boolean flag to a new value (via `set_flag`) and restore the previous -/// value when the entire object goes out of scope. +/// \brief Set a Boolean flag to a new value (via `set_flag`) and restore +/// the previous value when the entire object goes out of scope. +/// +/// \remarks Calls to set_value are tracked to allow detecting doubles sets +/// with different values and trigger an INVARIANT. class flag_resett { public: - /// Store the current value of \p flag and then set its value to \p new_value. - void set_flag(bool &flag, bool new_value) + explicit flag_resett(const goto_programt::instructiont &_instruction) + : instruction(_instruction) { + } + + /// \brief Store the current value of \p flag and + /// then set its value to \p new_value. + /// + /// \remarks an INVARIANT triggers iff the flag is set + /// more than once with different values. + void set_flag(bool &flag, bool new_value, const irep_idt &flag_name) + { + bool seen = flags_to_reset.find(&flag) != flags_to_reset.end(); + INVARIANT( + !(seen && flag != new_value), + "Flag " + id2string(flag_name) + + " set twice with incompatible values " + " at \n" + + instruction.source_location().pretty()); if(flag != new_value) { - flags_to_reset.emplace_back(&flag, flag); + flags_to_reset.emplace(&flag, flag); flag = new_value; } } - /// Restore the values of all flags that have been modified via `set_flag`. + /// \brief Restore the values of all flags that have been + /// modified via `set_flag`. ~flag_resett() { for(const auto &flag_pair : flags_to_reset) @@ -1871,7 +1891,8 @@ class flag_resett } private: - std::list> flags_to_reset; + const goto_programt::instructiont &instruction; + std::map flags_to_reset; }; void goto_checkt::goto_check( From 4c33a24dd648041c998c3f87d2afc71a9569846b Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 1 Dec 2021 01:29:48 +0000 Subject: [PATCH 5/9] Adds processing of enable pragmas with flag_resett --- src/analyses/goto_check.cpp | 58 +++++++++++++++++++++++++++---------- 1 file changed, 42 insertions(+), 16 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 2d9a96272f2..1356850e359 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1916,36 +1916,62 @@ void goto_checkt::goto_check( current_target = it; goto_programt::instructiont &i=*it; - flag_resett flag_resetter; + flag_resett resetter(i); const auto &pragmas = i.source_location().get_pragmas(); for(const auto &d : pragmas) { if(d.first == "disable:bounds-check") - flag_resetter.set_flag(enable_bounds_check, false); + resetter.set_flag(enable_bounds_check, false, d.first); else if(d.first == "disable:pointer-check") - flag_resetter.set_flag(enable_pointer_check, false); + resetter.set_flag(enable_pointer_check, false, d.first); else if(d.first == "disable:memory-leak-check") - flag_resetter.set_flag(enable_memory_leak_check, false); + resetter.set_flag(enable_memory_leak_check, false, d.first); else if(d.first == "disable:div-by-zero-check") - flag_resetter.set_flag(enable_div_by_zero_check, false); + resetter.set_flag(enable_div_by_zero_check, false, d.first); else if(d.first == "disable:enum-range-check") - flag_resetter.set_flag(enable_enum_range_check, false); + resetter.set_flag(enable_enum_range_check, false, d.first); else if(d.first == "disable:signed-overflow-check") - flag_resetter.set_flag(enable_signed_overflow_check, false); + resetter.set_flag(enable_signed_overflow_check, false, d.first); else if(d.first == "disable:unsigned-overflow-check") - flag_resetter.set_flag(enable_unsigned_overflow_check, false); + resetter.set_flag(enable_unsigned_overflow_check, false, d.first); else if(d.first == "disable:pointer-overflow-check") - flag_resetter.set_flag(enable_pointer_overflow_check, false); + resetter.set_flag(enable_pointer_overflow_check, false, d.first); else if(d.first == "disable:float-overflow-check") - flag_resetter.set_flag(enable_float_overflow_check, false); + resetter.set_flag(enable_float_overflow_check, false, d.first); else if(d.first == "disable:conversion-check") - flag_resetter.set_flag(enable_conversion_check, false); + resetter.set_flag(enable_conversion_check, false, d.first); else if(d.first == "disable:undefined-shift-check") - flag_resetter.set_flag(enable_undefined_shift_check, false); + resetter.set_flag(enable_undefined_shift_check, false, d.first); else if(d.first == "disable:nan-check") - flag_resetter.set_flag(enable_nan_check, false); + resetter.set_flag(enable_nan_check, false, d.first); else if(d.first == "disable:pointer-primitive-check") - flag_resetter.set_flag(enable_pointer_primitive_check, false); + resetter.set_flag(enable_pointer_primitive_check, false, d.first); + else if(d.first == "enable:bounds-check") + resetter.set_flag(enable_bounds_check, true, d.first); + else if(d.first == "enable:pointer-check") + resetter.set_flag(enable_pointer_check, true, d.first); + else if(d.first == "enable:memory_leak-check") + resetter.set_flag(enable_memory_leak_check, true, d.first); + else if(d.first == "enable:div-by-zero-check") + resetter.set_flag(enable_div_by_zero_check, true, d.first); + else if(d.first == "enable:enum-range-check") + resetter.set_flag(enable_enum_range_check, true, d.first); + else if(d.first == "enable:signed-overflow-check") + resetter.set_flag(enable_signed_overflow_check, true, d.first); + else if(d.first == "enable:unsigned-overflow-check") + resetter.set_flag(enable_unsigned_overflow_check, true, d.first); + else if(d.first == "enable:pointer-overflow-check") + resetter.set_flag(enable_pointer_overflow_check, true, d.first); + else if(d.first == "enable:float-overflow-check") + resetter.set_flag(enable_float_overflow_check, true, d.first); + else if(d.first == "enable:conversion-check") + resetter.set_flag(enable_conversion_check, true, d.first); + else if(d.first == "enable:undefined-shift-check") + resetter.set_flag(enable_undefined_shift_check, true, d.first); + else if(d.first == "enable:nan-check") + resetter.set_flag(enable_nan_check, true, d.first); + else if(d.first == "enable:pointer-primitive-check") + resetter.set_flag(enable_pointer_primitive_check, true, d.first); } new_code.clear(); @@ -2012,8 +2038,8 @@ void goto_checkt::goto_check( // Reset the no_enum_check with the flag reset for exception // safety { - flag_resett no_enum_check_flag_resetter; - no_enum_check_flag_resetter.set_flag(no_enum_check, true); + flag_resett resetter(i); + resetter.set_flag(no_enum_check, true, "no_enum_check"); check(assign_lhs); } From a219cf76a8b7eafb61b149d46486cf68488a6612 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 1 Dec 2021 01:33:30 +0000 Subject: [PATCH 6/9] Regression tests for enable pragmas --- regression/cbmc/pragma_cprover_enable1/main.c | 15 +++ .../cbmc/pragma_cprover_enable1/test.desc | 12 +++ regression/cbmc/pragma_cprover_enable2/main.c | 23 +++++ .../cbmc/pragma_cprover_enable2/test.desc | 14 +++ regression/cbmc/pragma_cprover_enable3/main.c | 20 ++++ .../cbmc/pragma_cprover_enable3/test.desc | 18 ++++ .../cbmc/pragma_cprover_enable_all/main.c | 92 +++++++++++++++++++ .../cbmc/pragma_cprover_enable_all/test.desc | 27 ++++++ .../main.c | 42 +++++++++ .../test.desc | 36 ++++++++ .../main.c | 42 +++++++++ .../test.desc | 43 +++++++++ .../main.c | 19 ++++ .../test.desc | 11 +++ 14 files changed, 414 insertions(+) create mode 100644 regression/cbmc/pragma_cprover_enable1/main.c create mode 100644 regression/cbmc/pragma_cprover_enable1/test.desc create mode 100644 regression/cbmc/pragma_cprover_enable2/main.c create mode 100644 regression/cbmc/pragma_cprover_enable2/test.desc create mode 100644 regression/cbmc/pragma_cprover_enable3/main.c create mode 100644 regression/cbmc/pragma_cprover_enable3/test.desc create mode 100644 regression/cbmc/pragma_cprover_enable_all/main.c create mode 100644 regression/cbmc/pragma_cprover_enable_all/test.desc create mode 100644 regression/cbmc/pragma_cprover_enable_disable_global_off/main.c create mode 100644 regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc create mode 100644 regression/cbmc/pragma_cprover_enable_disable_global_on/main.c create mode 100644 regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc create mode 100644 regression/cbmc/pragma_cprover_enable_disable_multiple/main.c create mode 100644 regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc diff --git a/regression/cbmc/pragma_cprover_enable1/main.c b/regression/cbmc/pragma_cprover_enable1/main.c new file mode 100644 index 00000000000..473534f3f11 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable1/main.c @@ -0,0 +1,15 @@ +int main() +{ + int x; + int y[1]; + +#pragma CPROVER check push +#pragma CPROVER check enable "bounds" +#pragma CPROVER check enable "signed-overflow" + // generate assertions for the following statement + x = x + y[1]; +#pragma CPROVER check pop + // but do not generate assertions for this one + x = y[1]; + return x; +} diff --git a/regression/cbmc/pragma_cprover_enable1/test.desc b/regression/cbmc/pragma_cprover_enable1/test.desc new file mode 100644 index 00000000000..8113775430e --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable1/test.desc @@ -0,0 +1,12 @@ +CORE +main.c + +^\[main\.array_bounds\.1\] line \d+ array 'y' upper bound.*FAILURE$ +^\[main\.overflow\.1\] line \d+ arithmetic overflow on signed.*FAILURE$ +^\*\* 2 of 2 failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Checks that we can selectively activate checks using pragmas. diff --git a/regression/cbmc/pragma_cprover_enable2/main.c b/regression/cbmc/pragma_cprover_enable2/main.c new file mode 100644 index 00000000000..6c59fe18282 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable2/main.c @@ -0,0 +1,23 @@ +int foo(int x) +{ + return x; +} + +int main() +{ + int m, n; + +#pragma CPROVER check push +#pragma CPROVER check enable "signed-overflow" + // generate assertions for the following statements + int x = m = n + n; + ++n; + n++; + n += 1; + foo(x + n); +#pragma CPROVER check pop + // but do not generate assertions for these + x = n + n; + foo(x + n); + return x; +} diff --git a/regression/cbmc/pragma_cprover_enable2/test.desc b/regression/cbmc/pragma_cprover_enable2/test.desc new file mode 100644 index 00000000000..9ddbded4bb7 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable2/test.desc @@ -0,0 +1,14 @@ +CORE +main.c + +^\[main\.overflow\.1\] line 13 arithmetic overflow on signed \+ in n \+ n: FAILURE$ +^\[main\.overflow\.2\] line 14 arithmetic overflow on signed \+ in n \+ 1: FAILURE$ +^\[main\.overflow\.3\] line 15 arithmetic overflow on signed \+ in n \+ 1: FAILURE$ +^\[main\.overflow\.4\] line 16 arithmetic overflow on signed \+ in n \+ 1: FAILURE$ +^\[main\.overflow\.5\] line 17 arithmetic overflow on signed \+ in x \+ n: FAILURE$ +^\*\* 5 of 5 failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc/pragma_cprover_enable3/main.c b/regression/cbmc/pragma_cprover_enable3/main.c new file mode 100644 index 00000000000..b58963e731c --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable3/main.c @@ -0,0 +1,20 @@ +#include + +int main() +{ + char *p = malloc(sizeof(*p)); + char *q; + +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-primitive" + // generate checks for the following statements and fail + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + + // but do not generate checks on the following statements + if(__CPROVER_same_object(p, q)) + { + } +} diff --git a/regression/cbmc/pragma_cprover_enable3/test.desc b/regression/cbmc/pragma_cprover_enable3/test.desc new file mode 100644 index 00000000000..32e6a926064 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable3/test.desc @@ -0,0 +1,18 @@ +CORE +main.c + +^main.c function main$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^\[main.pointer_primitives.\d+\] line 17 +-- diff --git a/regression/cbmc/pragma_cprover_enable_all/main.c b/regression/cbmc/pragma_cprover_enable_all/main.c new file mode 100644 index 00000000000..626f6388a01 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_all/main.c @@ -0,0 +1,92 @@ +#include +#include + +bool nondet_bool(); + +typedef enum ABC +{ + A = 0, + B = 1, + C = 2 +} ABC; + +int main() +{ +#pragma CPROVER check push +#pragma CPROVER check disable "bounds" +#pragma CPROVER check disable "pointer" +#pragma CPROVER check disable "div-by-zero" +#pragma CPROVER check disable "enum-range" +#pragma CPROVER check disable "signed-overflow" +#pragma CPROVER check disable "unsigned-overflow" +#pragma CPROVER check disable "pointer-overflow" +#pragma CPROVER check disable "float-overflow" +#pragma CPROVER check disable "conversion" +#pragma CPROVER check disable "undefined-shift" +#pragma CPROVER check disable "nan" +#pragma CPROVER check disable "pointer-primitive" + { + int N = 10; + char *p = malloc(N * sizeof(*p)); + char *q; + char *r; + float den; + float x; + float y; + ABC e; + bool same; + char i; + signed int j; + same = __CPROVER_same_object(p, q); + q = p + 2000000000000; + q = r; + if(nondet_bool()) + den = 0.0; + else + den = 1.0; + y = x / den; + e = 10; + i += 1; + j += 1; + } +#pragma CPROVER check push +#pragma CPROVER check enable "bounds" +#pragma CPROVER check enable "pointer" +#pragma CPROVER check enable "div-by-zero" +#pragma CPROVER check enable "enum-range" +#pragma CPROVER check enable "signed-overflow" +#pragma CPROVER check enable "unsigned-overflow" +#pragma CPROVER check enable "pointer-overflow" +#pragma CPROVER check enable "float-overflow" +#pragma CPROVER check enable "conversion" +#pragma CPROVER check enable "undefined-shift" +#pragma CPROVER check enable "nan" +#pragma CPROVER check enable "pointer-primitive" + { + int N = 10; + char *p = malloc(N * sizeof(*p)); + char *q; + char *r; + float den; + float x; + float y; + ABC e; + bool same; + char i; + signed int j; + same = __CPROVER_same_object(p, q); + q = p + 2000000000000; + q = r; + if(nondet_bool()) + den = 0.0; + else + den = 1.0; + y = x / den; + e = 10; + i += 1; + j += 1; + } +#pragma CPROVER check pop +#pragma CPROVER check pop + return 0; +} diff --git a/regression/cbmc/pragma_cprover_enable_all/test.desc b/regression/cbmc/pragma_cprover_enable_all/test.desc new file mode 100644 index 00000000000..ae18f942e09 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_all/test.desc @@ -0,0 +1,27 @@ +CORE broken-smt-backend +main.c +--object-bits 8 --bounds-check --pointer-check --pointer-primitive-check --div-by-zero-check --enum-range-check --unsigned-overflow-check --signed-overflow-check --pointer-overflow-check --float-overflow-check --conversion-check --undefined-shift-check --nan-check --pointer-primitive-check +^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE +^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE +^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000(l|ll): FAILURE +^\[main\.NaN\.\d+\] line 84 NaN on / in x / den: FAILURE +^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE +^\[main\.overflow\.\d+\] line 84 arithmetic overflow on floating-point division in x / den: FAILURE +^\[main\.enum-range-check\.\d+\] line 85 enum range check in \(ABC\)10: FAILURE +^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE +^\[main\.overflow\.\d+\] line 87 arithmetic overflow on signed \+ in j \+ 1: FAILURE +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in POINTER_OBJECT\(const void \*\)q\): FAILURE +^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in POINTER_OBJECT\(const void \*\)q\): FAILURE +^\[main\.pointer_arithmetic\.\d+\] line 41 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000(l|ll): FAILURE +^\[main\.NaN\.\d+\] line 47 NaN on / in x / den: FAILURE +^\[main\.division-by-zero\.\d+\] line 47 division by zero in x / den: FAILURE +^\[main\.overflow\.\d+\] line 47 arithmetic overflow on floating-point division in x / den: FAILURE +^\[main\.enum-range-check\.\d+\] line 48 enum range check in \(ABC\)10: FAILURE +^\[main\.overflow\.\d+\] line 49 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE +^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed \+ in j \+ 1: FAILURE +-- +This test uses all possible named-checks to maximize coverage. \ No newline at end of file diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_off/main.c b/regression/cbmc/pragma_cprover_enable_disable_global_off/main.c new file mode 100644 index 00000000000..31c7360121e --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_global_off/main.c @@ -0,0 +1,42 @@ +#include + +int main() +{ + char *p = malloc(sizeof(*p)); + char *q; + +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-primitive" + // must generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check push +#pragma CPROVER check disable "pointer-primitive" + // must not generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-primitive" + // must generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must not generate generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must generate generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must not generate generate checks + if(__CPROVER_same_object(p, q)) + { + } + return 0; +} diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc b/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc new file mode 100644 index 00000000000..d438774aaa4 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc @@ -0,0 +1,36 @@ +CORE +main.c + +^main.c function main$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^\[main.pointer_primitives.\d+\] line 17 +^\[main.pointer_primitives.\d+\] line 28 +^\[main.pointer_primitives.\d+\] line 38 +-- diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_on/main.c b/regression/cbmc/pragma_cprover_enable_disable_global_on/main.c new file mode 100644 index 00000000000..c4ad7887ccb --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_global_on/main.c @@ -0,0 +1,42 @@ +#include + +int main() +{ + char *p = malloc(sizeof(*p)); + char *q; + +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-primitive" + // must generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check push +#pragma CPROVER check disable "pointer-primitive" + // must not generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-primitive" + // must generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must not generate generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must generate generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must generate generate checks + if(__CPROVER_same_object(p, q)) + { + } + return 0; +} diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc b/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc new file mode 100644 index 00000000000..ccc772d828e --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc @@ -0,0 +1,43 @@ +CORE +main.c +--pointer-primitive-check +^main.c function main$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 38 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 38 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^\[main.pointer_primitives.\d+\] line 17 +^\[main.pointer_primitives.\d+\] line 28 +-- diff --git a/regression/cbmc/pragma_cprover_enable_disable_multiple/main.c b/regression/cbmc/pragma_cprover_enable_disable_multiple/main.c new file mode 100644 index 00000000000..e914c31bd45 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_multiple/main.c @@ -0,0 +1,19 @@ +#include + +int main() +{ + char *p = malloc(sizeof(*p)); + char *q; + +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-overflow" +// should not print an error message +#pragma CPROVER check enable "pointer-overflow" +#pragma CPROVER check push +#pragma CPROVER check disable "pointer-primitive" +// PARSE_ERROR +#pragma CPROVER check enable "pointer-primitive" +#pragma CPROVER check pop +#pragma CPROVER check pop + return 0; +} diff --git a/regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc b/regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc new file mode 100644 index 00000000000..9a39bcf1b94 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc @@ -0,0 +1,11 @@ +CORE +main.c + +^file main.c line \d+ function main: Found enable and disable pragmas for pointer-primitive-check +^file main.c line \d+ function main: syntax error before ' check enable "pointer-primitive"' +^PARSING ERROR$ +^EXIT=6$ +^SIGNAL=0$ +-- +^file main.c line \d+ function main: Found enable and disable pragmas for pointer-overflow-check +-- From cebf6d56c88339c29b13a9467c2f547d30a212c5 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 1 Dec 2021 01:33:58 +0000 Subject: [PATCH 7/9] Remove unused import --- src/analyses/goto_check.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 1356850e359..ade16e015cf 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_check.h" #include +#include #include #include From 68e8888130535df589401b7a97519466b3d2fccc Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 1 Dec 2021 01:34:24 +0000 Subject: [PATCH 8/9] Updated documentation for CPROVER check enable and disable pragmas. --- doc/cprover-manual/properties.md | 73 ++++++++++++++++++++++++++++---- 1 file changed, 64 insertions(+), 9 deletions(-) diff --git a/doc/cprover-manual/properties.md b/doc/cprover-manual/properties.md index 40f9c10eede..2e85ab4b171 100644 --- a/doc/cprover-manual/properties.md +++ b/doc/cprover-manual/properties.md @@ -131,22 +131,77 @@ The goto-instrument program supports these checks: | `--error-label label` | check that given label is unreachable | As all of these checks apply across the entire input program, we may wish to -disable them for selected statements in the program. For example, unsigned -overflows can be expected and acceptable in certain instructions even when -elsewhere we do not expect them. As of version 5.12, CBMC supports selectively -disabling automatically generated properties. To disable property generation, -use `#pragma CPROVER check disable ""`, which remains in effect -until a `#pragma CPROVER check pop` (to re-enable all properties -disabled before or since the last `#pragma CPROVER check push`) is provided. +disable or enable them for selected statements in the program. +For example, unsigned overflows can be expected and acceptable in certain +instructions even when elsewhere we do not expect them. +As of version 5.12, CBMC supports selectively disabling or enabling +automatically generated properties using pragmas. + + +CPROVER pragmas are handled using a stack: +- `#pragma CPROVER check push` pushes a new level on the pragma stack +- `#pragma CPROVER check disable ""` adds a disable pragma + at the top of the stack +- `#pragma CPROVER check enable ""` adds a enable pragma + at the top of the stack +- an `enable` or `disable` pragma for a given check present at the top level + of the stack shadows other pragmas for the same in lower levels of the stack +- adding both `enable` and `disable` pragmas for a same check in a same level + of the stack creates a PARSING_ERROR. +- `#pragma CPROVER check pop` pops a level in the stack and restores the state + of pragmas at the sub level + For example, for unsigned overflow checks, use + ``` unsigned foo(unsigned x) { #pragma CPROVER check push +#pragma CPROVER check enable "unsigned-overflow" + // unsigned overflow check apply here + x = x + 1; +#pragma CPROVER check pop + // unsigned overflow checks do not apply here + x = x + 2; +``` + +``` +unsigned foo(unsigned x) +{ +#pragma CPROVER check push +#pragma CPROVER check enable "unsigned-overflow" +#pragma CPROVER check enable "signed-overflow" + // unsigned and signed overflow check apply here + x = x + 1; +#pragma CPROVER check push #pragma CPROVER check disable "unsigned-overflow" - x = x + 1; // immediately follows the pragma, no unsigned overflow check here + // only signed overflow check apply here + x = x + 2; +#pragma CPROVER check pop + // unsigned and signed overflow check apply here + x = x + 3; +#pragma CPROVER check pop + // unsigned overflow checks do not apply here + x = x + 2; +``` + +``` +unsigned foo(unsigned x) +{ +#pragma CPROVER check push +#pragma CPROVER check enable "unsigned-overflow" +#pragma CPROVER check enable "signed-overflow" + // unsigned and signed overflow check apply here + x = x + 1; +#pragma CPROVER check push +#pragma CPROVER check disable "unsigned-overflow" +#pragma CPROVER check enable "unsigned-overflow" + // PARSING_ERROR Found enable and disable pragmas for unsigned-overflow-check + x = x + 2; +#pragma CPROVER check pop + x = x + 3; #pragma CPROVER check pop - x = x + 2; // unsigned overflow checks are generated here + x = x + 2; ``` #### Flag --nan-check limitations From f245b3ac72ca9d28ff267fc19ea23fdba128046f Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 1 Dec 2021 15:23:49 +0000 Subject: [PATCH 9/9] Removing unused import --- src/analyses/goto_check.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index ade16e015cf..1356850e359 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_check.h" #include -#include #include #include