From 249fb3f4b785d47b7871e60c7f7d28e4f2fb7b98 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Jan 2019 10:48:55 +0000 Subject: [PATCH 01/11] Method stubs: add missing type This had used a typeless symbol expression for ages without us noticing. --- jbmc/src/java_bytecode/simple_method_stubbing.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp index a17e8ab6033..96bda1db533 100644 --- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp +++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp @@ -170,7 +170,8 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol) symbol_table); const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr(); code_assignt get_argument( - init_symbol_expression, symbol_exprt(this_argument.get_identifier())); + init_symbol_expression, + symbol_exprt(this_argument.get_identifier(), this_type)); get_argument.add_source_location() = synthesized_source_location; new_instructions.add(get_argument); create_method_stub_at( From eda5f14234a32a3de66fb09c72dae5913ecb705a Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Jan 2019 10:49:50 +0000 Subject: [PATCH 02/11] JBMC: support validation This invokes validation using the same arguments as CBMC. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 21 +++++++++++++++++++++ jbmc/src/jbmc/jbmc_parse_options.h | 2 ++ 2 files changed, 23 insertions(+) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 8ea70017c47..f946da31a50 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -369,6 +369,16 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) "symex-coverage-report", cmdline.get_value("symex-coverage-report")); + if(cmdline.isset("validate-ssa-equation")) + { + options.set_option("validate-ssa-equation", true); + } + + if(cmdline.isset("validate-goto-model")) + { + options.set_option("validate-goto-model", true); + } + PARSE_OPTIONS_GOTO_TRACE(cmdline, options); if(cmdline.isset("no-lazy-methods")) @@ -553,6 +563,11 @@ int jbmc_parse_optionst::doit() if(set_properties(goto_model)) return 7; // should contemplate EX_USAGE from sysexits.h + if(cmdline.isset("validate-goto-model")) + { + goto_model.validate(validation_modet::INVARIANT); + } + // The `configure_bmc` callback passed will enable enum-unwind-static if // applicable. return bmct::do_language_agnostic_bmc( @@ -585,6 +600,11 @@ int jbmc_parse_optionst::doit() // particular function: add_failed_symbols(lazy_goto_model.symbol_table); + if(cmdline.isset("validate-goto-model")) + { + lazy_goto_model.validate(validation_modet::INVARIANT); + } + // Provide show-goto-functions and similar dump functions after symex // executes. If --paths is active, these dump routines run after every // paths iteration. Its return value indicates that if we ran any dump @@ -1141,6 +1161,7 @@ void jbmc_parse_optionst::help() " --version show version and exit\n" " --xml-ui use XML-formatted output\n" " --json-ui use JSON-formatted output\n" + HELP_VALIDATE HELP_GOTO_TRACE HELP_FLUSH " --verbosity # verbosity level\n" diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index d5989a7a5fc..8e4ca02d7e1 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -80,6 +81,7 @@ class optionst; "(localize-faults)(localize-faults-method):" \ "(java-threading)" \ OPT_GOTO_TRACE \ + OPT_VALIDATE \ "(symex-driven-lazy-loading)" // clang-format on From c203ef2e2e2878690b6ea09aece555d4f14e5d8a Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Jan 2019 10:50:48 +0000 Subject: [PATCH 03/11] Lazy goto model: support validation This mirrors existing support in goto_modelt. --- src/goto-programs/abstract_goto_model.h | 6 ++++++ src/goto-programs/goto_model.h | 14 +++++++++++++- src/goto-programs/lazy_goto_model.h | 9 +++++++++ 3 files changed, 28 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/abstract_goto_model.h b/src/goto-programs/abstract_goto_model.h index 6a244d837fe..25243c8f5eb 100644 --- a/src/goto-programs/abstract_goto_model.h +++ b/src/goto-programs/abstract_goto_model.h @@ -49,6 +49,12 @@ class abstract_goto_modelt /// underneath them, so this should only be used to lend a reference to code /// that cannot also call get_goto_function. virtual const symbol_tablet &get_symbol_table() const = 0; + + /// Check that the goto model is well-formed + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + virtual void validate(const validation_modet vm) const = 0; }; #endif diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index a71dbf82402..3dd6e434679 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -94,7 +94,7 @@ class goto_modelt : public abstract_goto_modelt /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate(const validation_modet vm) const + void validate(const validation_modet vm) const override { symbol_table.validate(vm); @@ -138,6 +138,18 @@ class wrapper_goto_modelt : public abstract_goto_modelt goto_functions.function_map.end(); } + /// Check that the goto model is well-formed + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + void validate(const validation_modet vm) const override + { + symbol_table.validate(vm); + + const namespacet ns(symbol_table); + goto_functions.validate(ns, vm); + } + private: const symbol_tablet &symbol_table; const goto_functionst &goto_functions; diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index 61b623c63ad..d62b477c838 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -243,6 +243,15 @@ class lazy_goto_modelt : public abstract_goto_modelt return goto_functions.at(id); } + /// Check that the goto model is well-formed + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + void validate(const validation_modet vm) const override + { + goto_model->validate(vm); + } + private: std::unique_ptr goto_model; From 738fbde8fe801cda6869d85d557188cb1ebf11a6 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Jan 2019 10:52:03 +0000 Subject: [PATCH 04/11] Don't validate Java symbols' base names for now They use a different pattern to that expected for C programs, and changing that will have some impact. For now let's make validation practically usable without making a change with potentially widespread impact. --- src/util/symbol.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 58edd886cd3..73225b1e502 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -137,10 +137,11 @@ bool symbolt::is_well_formed() const // Well-formedness criterion number 2 is for a symbol // to have it's base name as a suffix to it's more // general name. - if(!has_suffix(id2string(name), id2string(base_name))) - { + // Exception: Java symbols' base names do not have type signatures + // (for example, they can have name "someclass.method:(II)V" and base name + // "method") + if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java) return false; - } return true; } From 555ff9aa08ca54b26550201dec85f7cf963fc508 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 14 Jan 2019 15:50:33 +0000 Subject: [PATCH 05/11] Revert "strengthen assignment type consistency" This reverts commit caae4ceee630400519fd47528dadedc62149c00b. Reverting because we can't currently meet either the weak (base_type_eq) or the strong (==) consistency requirement. Let's target the weak one first. --- src/util/std_code.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/std_code.h b/src/util/std_code.h index 6ec29664634..015d8d8c0fd 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -303,7 +303,7 @@ class code_assignt:public codet DATA_CHECK( vm, - code.op0().type() == code.op1().type(), + base_type_eq(code.op0().type(), code.op1().type(), ns), "lhs and rhs of assignment must have same type"); } From 03277d6cbc8f2bc525aaf366dcc861b321208882 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 14 Jan 2019 16:29:03 +0000 Subject: [PATCH 06/11] Add name to namespace parameter --- src/util/std_code.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/std_code.h b/src/util/std_code.h index 015d8d8c0fd..d4e7058114c 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -296,7 +296,7 @@ class code_assignt:public codet static void validate( const codet &code, - const namespacet &, + const namespacet &ns, const validation_modet vm = validation_modet::INVARIANT) { check(code, vm); From 586778568e5ae2e06e8cf24e616f848eb6eaa4ea Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Jan 2019 11:16:42 +0000 Subject: [PATCH 07/11] Enable model validation in all JBMC regression tests --- jbmc/regression/jbmc-concurrency/CMakeLists.txt | 2 +- jbmc/regression/jbmc-concurrency/Makefile | 4 ++-- jbmc/regression/jbmc-generics/CMakeLists.txt | 4 ++-- jbmc/regression/jbmc-generics/Makefile | 8 ++++---- jbmc/regression/jbmc-inheritance/CMakeLists.txt | 2 +- jbmc/regression/jbmc-inheritance/Makefile | 4 ++-- jbmc/regression/jbmc-strings/CMakeLists.txt | 4 ++-- jbmc/regression/jbmc-strings/Makefile | 16 ++++++++-------- jbmc/regression/jbmc/CMakeLists.txt | 4 ++-- jbmc/regression/jbmc/Makefile | 8 ++++---- .../strings-smoke-tests/CMakeLists.txt | 4 ++-- jbmc/regression/strings-smoke-tests/Makefile | 16 ++++++++-------- 12 files changed, 38 insertions(+), 38 deletions(-) diff --git a/jbmc/regression/jbmc-concurrency/CMakeLists.txt b/jbmc/regression/jbmc-concurrency/CMakeLists.txt index afe0ea5761a..41bcd14736c 100644 --- a/jbmc/regression/jbmc-concurrency/CMakeLists.txt +++ b/jbmc/regression/jbmc-concurrency/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + "$ --validate-goto-model" ) diff --git a/jbmc/regression/jbmc-concurrency/Makefile b/jbmc/regression/jbmc-concurrency/Makefile index ad6e5381fff..c4f57b99d3b 100644 --- a/jbmc/regression/jbmc-concurrency/Makefile +++ b/jbmc/regression/jbmc-concurrency/Makefile @@ -3,10 +3,10 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc-generics/CMakeLists.txt b/jbmc/regression/jbmc-generics/CMakeLists.txt index 1c5fc08cf6b..a45412e6b33 100644 --- a/jbmc/regression/jbmc-generics/CMakeLists.txt +++ b/jbmc/regression/jbmc-generics/CMakeLists.txt @@ -1,10 +1,10 @@ add_test_pl_tests( - "$" + "$ --validate-goto-model" ) add_test_pl_profile( "jbmc-generics-symex-driven-lazy-loading" - "$ --symex-driven-lazy-loading" + "$ --validate-goto-model --symex-driven-lazy-loading" "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading" "CORE" ) diff --git a/jbmc/regression/jbmc-generics/Makefile b/jbmc/regression/jbmc-generics/Makefile index 1639d08dea4..3e131188519 100644 --- a/jbmc/regression/jbmc-generics/Makefile +++ b/jbmc/regression/jbmc-generics/Makefile @@ -3,12 +3,12 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc-inheritance/CMakeLists.txt b/jbmc/regression/jbmc-inheritance/CMakeLists.txt index afe0ea5761a..41bcd14736c 100644 --- a/jbmc/regression/jbmc-inheritance/CMakeLists.txt +++ b/jbmc/regression/jbmc-inheritance/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + "$ --validate-goto-model" ) diff --git a/jbmc/regression/jbmc-inheritance/Makefile b/jbmc/regression/jbmc-inheritance/Makefile index ad6e5381fff..c4f57b99d3b 100644 --- a/jbmc/regression/jbmc-inheritance/Makefile +++ b/jbmc/regression/jbmc-inheritance/Makefile @@ -3,10 +3,10 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc-strings/CMakeLists.txt b/jbmc/regression/jbmc-strings/CMakeLists.txt index 1b698f38161..17905543c1e 100644 --- a/jbmc/regression/jbmc-strings/CMakeLists.txt +++ b/jbmc/regression/jbmc-strings/CMakeLists.txt @@ -1,10 +1,10 @@ add_test_pl_tests( - "$" + "$ --validate-goto-model" ) add_test_pl_profile( "jbmc-strings-symex-driven-lazy-loading" - "$ --symex-driven-lazy-loading" + "$ --validate-goto-model --symex-driven-lazy-loading" "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading" "CORE" ) diff --git a/jbmc/regression/jbmc-strings/Makefile b/jbmc/regression/jbmc-strings/Makefile index 6a87a176e59..70b6cd5e570 100644 --- a/jbmc/regression/jbmc-strings/Makefile +++ b/jbmc/regression/jbmc-strings/Makefile @@ -3,20 +3,20 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading testfuture: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CF + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading testall: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CFTK + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc/CMakeLists.txt b/jbmc/regression/jbmc/CMakeLists.txt index fa345944621..85c24586b49 100644 --- a/jbmc/regression/jbmc/CMakeLists.txt +++ b/jbmc/regression/jbmc/CMakeLists.txt @@ -1,10 +1,10 @@ add_test_pl_tests( - "$" + "$ --validate-goto-model" ) add_test_pl_profile( "jbmc-symex-driven-lazy-loading" - "$ --symex-driven-lazy-loading" + "$ --validate-goto-model --symex-driven-lazy-loading" "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading" "CORE" ) diff --git a/jbmc/regression/jbmc/Makefile b/jbmc/regression/jbmc/Makefile index 1639d08dea4..3e131188519 100644 --- a/jbmc/regression/jbmc/Makefile +++ b/jbmc/regression/jbmc/Makefile @@ -3,12 +3,12 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading show: @for dir in *; do \ diff --git a/jbmc/regression/strings-smoke-tests/CMakeLists.txt b/jbmc/regression/strings-smoke-tests/CMakeLists.txt index 0b63a67939c..93b92d81026 100644 --- a/jbmc/regression/strings-smoke-tests/CMakeLists.txt +++ b/jbmc/regression/strings-smoke-tests/CMakeLists.txt @@ -1,10 +1,10 @@ add_test_pl_tests( - "$" + "$ --validate-goto-model" ) add_test_pl_profile( "strings-smoke-tests-symex-driven-lazy-loading" - "$ --symex-driven-lazy-loading" + "$ --validate-goto-model --symex-driven-lazy-loading" "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading" "CORE" ) diff --git a/jbmc/regression/strings-smoke-tests/Makefile b/jbmc/regression/strings-smoke-tests/Makefile index 6a87a176e59..70b6cd5e570 100644 --- a/jbmc/regression/strings-smoke-tests/Makefile +++ b/jbmc/regression/strings-smoke-tests/Makefile @@ -3,20 +3,20 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading testfuture: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CF + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading testall: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CFTK + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading show: @for dir in *; do \ From 0f1abe1deddc09afc26ed8c82db361c5d9a8097e Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Jan 2019 11:43:53 +0000 Subject: [PATCH 08/11] DECL VCCs: don't check non-existent SSA-rhs DECL clauses do not give an RHS, so comparing its type against the LHS is meaningless (and always fails). --- src/goto-symex/symex_target_equation.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 637715ffa04..d0a07c044a4 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -961,8 +961,12 @@ void symex_target_equationt::SSA_stept::validate( case goto_trace_stept::typet::CONSTRAINT: validate_full_expr(cond_expr, ns, vm); break; - case goto_trace_stept::typet::ASSIGNMENT: case goto_trace_stept::typet::DECL: + validate_full_expr(ssa_lhs, ns, vm); + validate_full_expr(ssa_full_lhs, ns, vm); + validate_full_expr(original_full_lhs, ns, vm); + break; + case goto_trace_stept::typet::ASSIGNMENT: validate_full_expr(ssa_lhs, ns, vm); validate_full_expr(ssa_full_lhs, ns, vm); validate_full_expr(original_full_lhs, ns, vm); From d53bf4b30e6a4e8617013eb978010c06026b6417 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Jan 2019 11:45:01 +0000 Subject: [PATCH 09/11] Equation validation: use base_type_eq on types, not exprs The expr version expects two like-structured expressions and validates subexpressions pairwise, which is not the expected situation for VCCs. --- src/goto-symex/symex_target_equation.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index d0a07c044a4..2a947691a85 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -973,7 +973,7 @@ void symex_target_equationt::SSA_stept::validate( validate_full_expr(ssa_rhs, ns, vm); DATA_CHECK( vm, - base_type_eq(ssa_lhs.get_original_expr(), ssa_rhs, ns), + base_type_eq(ssa_lhs.get_original_expr().type(), ssa_rhs.type(), ns), "Type inequality in SSA assignment\nlhs-type: " + ssa_lhs.get_original_expr().type().id_string() + "\nrhs-type: " + ssa_rhs.type().id_string()); From b2fe0352412e67902bf2333e89ca83fd7312cc05 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Jan 2019 11:48:09 +0000 Subject: [PATCH 10/11] JBMC: enable SSA equation validation in all regression tests --- jbmc/regression/jbmc-concurrency/CMakeLists.txt | 2 +- jbmc/regression/jbmc-concurrency/Makefile | 4 ++-- jbmc/regression/jbmc-generics/CMakeLists.txt | 4 ++-- jbmc/regression/jbmc-generics/Makefile | 8 ++++---- jbmc/regression/jbmc-inheritance/CMakeLists.txt | 2 +- jbmc/regression/jbmc-inheritance/Makefile | 4 ++-- jbmc/regression/jbmc-strings/CMakeLists.txt | 4 ++-- jbmc/regression/jbmc-strings/Makefile | 16 ++++++++-------- jbmc/regression/jbmc/CMakeLists.txt | 4 ++-- jbmc/regression/jbmc/Makefile | 8 ++++---- .../strings-smoke-tests/CMakeLists.txt | 4 ++-- jbmc/regression/strings-smoke-tests/Makefile | 16 ++++++++-------- 12 files changed, 38 insertions(+), 38 deletions(-) diff --git a/jbmc/regression/jbmc-concurrency/CMakeLists.txt b/jbmc/regression/jbmc-concurrency/CMakeLists.txt index 41bcd14736c..25982e8508f 100644 --- a/jbmc/regression/jbmc-concurrency/CMakeLists.txt +++ b/jbmc/regression/jbmc-concurrency/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$ --validate-goto-model" + "$ --validate-goto-model --validate-ssa-equation" ) diff --git a/jbmc/regression/jbmc-concurrency/Makefile b/jbmc/regression/jbmc-concurrency/Makefile index c4f57b99d3b..e330a0eea3e 100644 --- a/jbmc/regression/jbmc-concurrency/Makefile +++ b/jbmc/regression/jbmc-concurrency/Makefile @@ -3,10 +3,10 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc-generics/CMakeLists.txt b/jbmc/regression/jbmc-generics/CMakeLists.txt index a45412e6b33..507772ba3e0 100644 --- a/jbmc/regression/jbmc-generics/CMakeLists.txt +++ b/jbmc/regression/jbmc-generics/CMakeLists.txt @@ -1,10 +1,10 @@ add_test_pl_tests( - "$ --validate-goto-model" + "$ --validate-goto-model --validate-ssa-equation" ) add_test_pl_profile( "jbmc-generics-symex-driven-lazy-loading" - "$ --validate-goto-model --symex-driven-lazy-loading" + "$ --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading" "CORE" ) diff --git a/jbmc/regression/jbmc-generics/Makefile b/jbmc/regression/jbmc-generics/Makefile index 3e131188519..592bd2d0d96 100644 --- a/jbmc/regression/jbmc-generics/Makefile +++ b/jbmc/regression/jbmc-generics/Makefile @@ -3,12 +3,12 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc-inheritance/CMakeLists.txt b/jbmc/regression/jbmc-inheritance/CMakeLists.txt index 41bcd14736c..25982e8508f 100644 --- a/jbmc/regression/jbmc-inheritance/CMakeLists.txt +++ b/jbmc/regression/jbmc-inheritance/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$ --validate-goto-model" + "$ --validate-goto-model --validate-ssa-equation" ) diff --git a/jbmc/regression/jbmc-inheritance/Makefile b/jbmc/regression/jbmc-inheritance/Makefile index c4f57b99d3b..e330a0eea3e 100644 --- a/jbmc/regression/jbmc-inheritance/Makefile +++ b/jbmc/regression/jbmc-inheritance/Makefile @@ -3,10 +3,10 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc-strings/CMakeLists.txt b/jbmc/regression/jbmc-strings/CMakeLists.txt index 17905543c1e..c7b8343e59c 100644 --- a/jbmc/regression/jbmc-strings/CMakeLists.txt +++ b/jbmc/regression/jbmc-strings/CMakeLists.txt @@ -1,10 +1,10 @@ add_test_pl_tests( - "$ --validate-goto-model" + "$ --validate-goto-model --validate-ssa-equation" ) add_test_pl_profile( "jbmc-strings-symex-driven-lazy-loading" - "$ --validate-goto-model --symex-driven-lazy-loading" + "$ --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading" "CORE" ) diff --git a/jbmc/regression/jbmc-strings/Makefile b/jbmc/regression/jbmc-strings/Makefile index 70b6cd5e570..1cb0d87fafb 100644 --- a/jbmc/regression/jbmc-strings/Makefile +++ b/jbmc/regression/jbmc-strings/Makefile @@ -3,20 +3,20 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading testfuture: - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CF - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading testall: - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CFTK - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc/CMakeLists.txt b/jbmc/regression/jbmc/CMakeLists.txt index 85c24586b49..561fe5ab0c7 100644 --- a/jbmc/regression/jbmc/CMakeLists.txt +++ b/jbmc/regression/jbmc/CMakeLists.txt @@ -1,10 +1,10 @@ add_test_pl_tests( - "$ --validate-goto-model" + "$ --validate-goto-model --validate-ssa-equation" ) add_test_pl_profile( "jbmc-symex-driven-lazy-loading" - "$ --validate-goto-model --symex-driven-lazy-loading" + "$ --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading" "CORE" ) diff --git a/jbmc/regression/jbmc/Makefile b/jbmc/regression/jbmc/Makefile index 3e131188519..592bd2d0d96 100644 --- a/jbmc/regression/jbmc/Makefile +++ b/jbmc/regression/jbmc/Makefile @@ -3,12 +3,12 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading show: @for dir in *; do \ diff --git a/jbmc/regression/strings-smoke-tests/CMakeLists.txt b/jbmc/regression/strings-smoke-tests/CMakeLists.txt index 93b92d81026..e3584329528 100644 --- a/jbmc/regression/strings-smoke-tests/CMakeLists.txt +++ b/jbmc/regression/strings-smoke-tests/CMakeLists.txt @@ -1,10 +1,10 @@ add_test_pl_tests( - "$ --validate-goto-model" + "$ --validate-goto-model --validate-ssa-equation" ) add_test_pl_profile( "strings-smoke-tests-symex-driven-lazy-loading" - "$ --validate-goto-model --symex-driven-lazy-loading" + "$ --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading" "CORE" ) diff --git a/jbmc/regression/strings-smoke-tests/Makefile b/jbmc/regression/strings-smoke-tests/Makefile index 70b6cd5e570..1cb0d87fafb 100644 --- a/jbmc/regression/strings-smoke-tests/Makefile +++ b/jbmc/regression/strings-smoke-tests/Makefile @@ -3,20 +3,20 @@ default: tests.log include ../../src/config.inc test: - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading testfuture: - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CF - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading testall: - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CFTK - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" - @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading show: @for dir in *; do \ From 4232b15cc545bca9b426217d60093c6767cf6489 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 14 Jan 2019 15:54:38 +0000 Subject: [PATCH 11/11] Pacify clang-format Adding an include in a prior commit --> I must sort the other ones, apparently :) --- jbmc/src/jbmc/jbmc_parse_options.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 8e4ca02d7e1..3b9d7dd30c0 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -12,9 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_JBMC_JBMC_PARSE_OPTIONS_H #define CPROVER_JBMC_JBMC_PARSE_OPTIONS_H -#include #include #include +#include #include #include