From b28e701228d960a1e3c26ce8422eac02f11de96c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Sep 2017 17:04:15 +0000 Subject: [PATCH 01/13] fixup! variants of service functions for goto_modelt --- src/goto-programs/replace_java_nondet.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/goto-programs/replace_java_nondet.cpp b/src/goto-programs/replace_java_nondet.cpp index 8261bb087ea..b030cbaa312 100644 --- a/src/goto-programs/replace_java_nondet.cpp +++ b/src/goto-programs/replace_java_nondet.cpp @@ -251,4 +251,3 @@ void replace_java_nondet(goto_modelt &goto_model) { replace_java_nondet(goto_model.goto_functions); } - From fd5692102c7bac0e654b58a709c59d0e6716c295 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Sep 2017 17:37:17 +0000 Subject: [PATCH 02/13] fixup! Fix and run cbmc-cover tests --- regression/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/Makefile b/regression/Makefile index ff713b428e4..d47df3994cc 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -1,9 +1,9 @@ DIRS = ansi-c \ cbmc \ - cpp \ + cbmc-cover \ cbmc-java \ cbmc-java-inheritance \ - cbmc-cover \ + cpp \ goto-analyzer \ goto-diff \ goto-gcc \ From 8054162c43705cdfbfb277be68bb766e366dca02 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Sep 2017 17:52:34 +0000 Subject: [PATCH 03/13] fixup! Instrument string-refinement code such that null-pointer checks are detected --- src/java_bytecode/java_utils.h | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index 59405c9f9c6..ed26fe1caf6 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -6,15 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include -#include -#include - -#include "java_bytecode_parse_tree.h" #ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H #define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H -#include +#include +#include +#include bool java_is_array_type(const typet &type); From 7d261396dc2a1fc1a476ab2fa817571f681be0ee Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Sep 2017 18:00:24 +0000 Subject: [PATCH 04/13] fixup! Replace BV_ADDR_BITS by config setting --- src/solvers/flattening/pointer_logic.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h index 2ce6dee37aa..d094dbd8523 100644 --- a/src/solvers/flattening/pointer_logic.h +++ b/src/solvers/flattening/pointer_logic.h @@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com class namespacet; -class namespacet; - class pointer_logict { public: From d5db0bc0875b4247395bd29661f6f263aaf3b36f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Sep 2017 09:41:26 +0000 Subject: [PATCH 05/13] fixup! added a test case for combination use of forall/exists/not. --- regression/cbmc/Quantifiers-assertion/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc index 555f7b0e61f..df26ad98dbe 100644 --- a/regression/cbmc/Quantifiers-assertion/test.desc +++ b/regression/cbmc/Quantifiers-assertion/test.desc @@ -9,4 +9,4 @@ main.c ^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$ ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$ ^\*\* 2 of 6 failed \(2 iterations\)$ -^\VERIFICATION FAILED$ +^VERIFICATION FAILED$ From 191f37198025013c4fd5388ff5b3764674e53fd4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Sep 2017 09:41:58 +0000 Subject: [PATCH 06/13] fixup! a right place to implement the quantifier handling. --- regression/cbmc/Quantifiers-assignment/test.desc | 2 +- regression/cbmc/Quantifiers-if/test.desc | 2 +- regression/cbmc/Quantifiers-not/test.desc | 2 +- regression/cbmc/Quantifiers-type/test.desc | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc index 289e8a47efc..ca5f55d51a2 100644 --- a/regression/cbmc/Quantifiers-assignment/test.desc +++ b/regression/cbmc/Quantifiers-assignment/test.desc @@ -7,4 +7,4 @@ main.c ^\[main.assertion.3\] assertion z1: SUCCESS$ ^\[main.assertion.4\] assertion z2: SUCCESS$ ^\*\* 1 of 4 failed \(2 iterations\)$ -^\VERIFICATION FAILED$ +^VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc index be4945b25ef..7685cf4284a 100644 --- a/regression/cbmc/Quantifiers-if/test.desc +++ b/regression/cbmc/Quantifiers-if/test.desc @@ -8,4 +8,4 @@ main.c ^\[main.assertion.4\] failure 3: FAILURE$ ^\[main.assertion.5\] success 2: SUCCESS$ ^\*\* 3 of 5 failed \(2 iterations\)$ -^\VERIFICATION FAILED$ +^VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc index 2e862045758..b22b6666f14 100644 --- a/regression/cbmc/Quantifiers-not/test.desc +++ b/regression/cbmc/Quantifiers-not/test.desc @@ -8,4 +8,4 @@ main.c ^\[main.assertion.4\] success 3: SUCCESS$ ^\[main.assertion.5\] failure 2: FAILURE$ ^\*\* 2 of 5 failed \(2 iterations\)$ -^\VERIFICATION FAILED$ +^VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc index b0b25cc9903..a3939c6a78a 100644 --- a/regression/cbmc/Quantifiers-type/test.desc +++ b/regression/cbmc/Quantifiers-type/test.desc @@ -5,4 +5,4 @@ main.c ^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$ ^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$ ^\*\* 1 of 2 failed \(2 iterations\)$ -^\VERIFICATION FAILED$ +^VERIFICATION FAILED$ From 24be89c7bb315a81800f3059f64889912a30e019 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Sep 2017 09:43:09 +0000 Subject: [PATCH 07/13] fixup! simplify \'not exists\' to the form of \'forall not\' --- regression/cbmc/Quantifiers-not-exists/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc index 630e54eb224..63ff98c10ad 100644 --- a/regression/cbmc/Quantifiers-not-exists/test.desc +++ b/regression/cbmc/Quantifiers-not-exists/test.desc @@ -9,4 +9,4 @@ main.c ^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$ ^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$ ^\*\* 0 of 6 failed \(1 iteration\)$ -^\VERIFICATION SUCCESSFUL$ +^VERIFICATION SUCCESSFUL$ From dfd00d3160c0af5e98b37f3d0ee999ccafef19b3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Sep 2017 11:21:22 +0000 Subject: [PATCH 08/13] fixup! Translate exprt to/from miniBDD --- src/solvers/prop/bdd_expr.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp index 2a5b4ffa786..01dacc19048 100644 --- a/src/solvers/prop/bdd_expr.cpp +++ b/src/solvers/prop/bdd_expr.cpp @@ -122,7 +122,7 @@ exprt bdd_exprt::as_expr(const mini_bddt &r) const } else if(r.high().is_false()) { - if(r.high().is_true()) + if(r.low().is_true()) return not_exprt(n_expr); else return and_exprt(not_exprt(n_expr), as_expr(r.low())); From 66719a9f8d7971b66c5dfe7832898aa66313a641 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Sep 2017 13:10:42 +0000 Subject: [PATCH 09/13] fixup! goto-instrument --print-path-lengths: statistics about control-flow graph paths --- src/goto-instrument/goto_instrument_parse_options.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index f7aab087027..7d47a5a4771 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1489,6 +1489,8 @@ void goto_instrument_parse_optionst::help() " --show-natural-loops show natural loop heads\n" // NOLINTNEXTLINE(whitespace/line_length) " --list-calls-args list all function calls with their arguments\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --print-path-lengths print statistics about control-flow graph paths\n" "\n" "Safety checks:\n" " --no-assertions ignore user assertions\n" From f12c7909ee64cd637ff36a47c71309a25090a807 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Sep 2017 13:39:30 +0000 Subject: [PATCH 10/13] fixup! fixup! Add --drop-unused-functions option --- src/goto-instrument/goto_instrument_parse_options.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 7d47a5a4771..be77888ad47 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1482,6 +1482,7 @@ void goto_instrument_parse_optionst::help() " --show-symbol-table show symbol table\n" " --list-symbols list symbols with type information\n" HELP_SHOW_GOTO_FUNCTIONS + " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) " --print-internal-representation\n" // NOLINTNEXTLINE(*) " show verbose internal representation of the program\n" " --list-undefined-functions list functions without body\n" From 82ab237b09b940d08cdc2674618d0c86c1fa5622 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Sep 2017 13:54:10 +0000 Subject: [PATCH 11/13] fixup! Split java nondet pass in two --- src/goto-programs/convert_nondet.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp index d55afbe91a1..b329a41ddbc 100644 --- a/src/goto-programs/convert_nondet.cpp +++ b/src/goto-programs/convert_nondet.cpp @@ -67,7 +67,8 @@ static goto_programt::targett insert_nondet_init_code( } // Although, if the type is a ptr-to-void then we also want to bail - if(lhs.type().subtype().id()==ID_empty) + if(lhs.type().subtype().id()==ID_empty || + lhs.type().subtype().id()==ID_code) { return next_instr; } From 2060b34de7481cc9f058b374286d9f957b1070bf Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Sep 2017 14:44:46 +0000 Subject: [PATCH 12/13] fixup! Added __CPROVER_array_replace to complement __CPROVER_array_set --- src/goto-programs/goto_convert_class.h | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 508fb4fda6d..fe227986a71 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -530,11 +530,6 @@ class goto_convertt:public messaget const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest); - void do_array_set( - const exprt &lhs, - const exprt &rhs, - const exprt::operandst &arguments, - goto_programt &dest); void do_array_equal( const exprt &lhs, const exprt &rhs, @@ -543,7 +538,7 @@ class goto_convertt:public messaget void do_array_op( const irep_idt &id, const exprt &lhs, - const exprt &rhs, + const exprt &function, const exprt::operandst &arguments, goto_programt &dest); void do_printf( From 9d5d907ede97fb9d121cf39cea9819da4bd1c281 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Sep 2017 17:04:40 +0100 Subject: [PATCH 13/13] fixup! Allow extra entry-points to be specified for CI lazy loading --- src/java_bytecode/java_utils.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index 36b98dc0ccd..bf41076d84c 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + bool java_is_array_type(const typet &type) { if(type.id()!=ID_struct)