From d2ca288722e74e6e89ebbdd6880d5c4998933e09 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 12 Mar 2019 14:20:16 +0000 Subject: [PATCH 1/2] Move invariant out of if The full_lhs_value should have a non-nil value regardless of whether the identifier exists in the namespace. This makes visible that the SMT solver returns for an unbounded array as value ((|__CPROVER_threads_exited#1| |__CPROVER_threads_exited#1|)) which is self-referential and thus not usable. --- regression/cbmc/enum-trace1/test_json.desc | 2 +- regression/cbmc/json1/test.desc | 2 +- regression/cbmc/trace_options_json_extended/extended.desc | 2 +- .../cbmc/trace_options_json_extended/non-extended.desc | 2 +- src/goto-programs/json_goto_trace.cpp | 7 ++++--- 5 files changed, 8 insertions(+), 7 deletions(-) diff --git a/regression/cbmc/enum-trace1/test_json.desc b/regression/cbmc/enum-trace1/test_json.desc index 6619fc73eea..255c95b8c1c 100644 --- a/regression/cbmc/enum-trace1/test_json.desc +++ b/regression/cbmc/enum-trace1/test_json.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-smt-backend main.c --json-ui --function test --trace activate-multi-line-match diff --git a/regression/cbmc/json1/test.desc b/regression/cbmc/json1/test.desc index b9eb6a30118..bf66d83d928 100644 --- a/regression/cbmc/json1/test.desc +++ b/regression/cbmc/json1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-smt-backend main.c --json-ui --stop-on-fail activate-multi-line-match diff --git a/regression/cbmc/trace_options_json_extended/extended.desc b/regression/cbmc/trace_options_json_extended/extended.desc index beafa0649de..51bef1274d1 100644 --- a/regression/cbmc/trace_options_json_extended/extended.desc +++ b/regression/cbmc/trace_options_json_extended/extended.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-smt-backend test.c --trace --json-ui --trace-json-extended ^EXIT=10$ diff --git a/regression/cbmc/trace_options_json_extended/non-extended.desc b/regression/cbmc/trace_options_json_extended/non-extended.desc index 5d03ca97bc1..c70b6540a9d 100644 --- a/regression/cbmc/trace_options_json_extended/non-extended.desc +++ b/regression/cbmc/trace_options_json_extended/non-extended.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-smt-backend test.c --trace --json-ui ^EXIT=10$ diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 2e27f766b5d..02a6f0f128d 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -118,6 +118,10 @@ void convert_decl( const symbolt *symbol; irep_idt base_name, display_name; + DATA_INVARIANT( + step.full_lhs_value.is_not_nil(), + "full_lhs_value in assignment must not be nil"); + if(!ns.lookup(identifier, symbol)) { base_name = symbol->base_name; @@ -132,9 +136,6 @@ void convert_decl( } else { - DATA_INVARIANT( - step.full_lhs_value.is_not_nil(), - "full_lhs_value in assignment must not be nil"); full_lhs_value = json(step.full_lhs_value, ns, ID_unknown); } From 08c7c9dfe4eaff8b40dbf386cc92059f5295cf82 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 12 Mar 2019 14:27:18 +0000 Subject: [PATCH 2/2] Adding test demonstrating fix to trace generation --- .../jbmc/nondet-array-size/TestClass.class | Bin 0 -> 762 bytes .../jbmc/nondet-array-size/TestClass.java | 11 +++++++++++ .../regression/jbmc/nondet-array-size/test.desc | 16 ++++++++++++++++ 3 files changed, 27 insertions(+) create mode 100644 jbmc/regression/jbmc/nondet-array-size/TestClass.class create mode 100644 jbmc/regression/jbmc/nondet-array-size/TestClass.java create mode 100644 jbmc/regression/jbmc/nondet-array-size/test.desc diff --git a/jbmc/regression/jbmc/nondet-array-size/TestClass.class b/jbmc/regression/jbmc/nondet-array-size/TestClass.class new file mode 100644 index 0000000000000000000000000000000000000000..75f92d76b8e68cac3069d4e07a1d552e62c25d37 GIT binary patch literal 762 zcmZvZO>fgc5Qg8ioj7rvkEW2elmev%5*Oi1Z>>;Kpa*0=s#cXqPa9{Iy7;47JH7Hh zdPd?5NE87IHxB$JgqU?ha)8Uu&U$9vXI}sO{bdYb6Zb8Yuwvl`ZkAEREfcF246K;A zZD9@TChjoIuk$n&G7FM8eH^5`ABq73>oF9!gE+_@GU)BjA%oFP27;mP1+jQOiuytx zsA7hum-sw9;{UmHU)X0 zL~T@Ho49M^9@;j_uoxC+G>`sz@41?K|nJzX@^=q%=sI_h*+rBr|h<|vlY#5}#I<~KA82V>u z&iGr=+tBU3575t1`3mFJ1q$Dlf}Sh1Xrj_-f~+URWt!X}K&9BaoQf;BO4$PGwdf?1 wDXT!Q?XX{1GOSO5S3 literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/nondet-array-size/TestClass.java b/jbmc/regression/jbmc/nondet-array-size/TestClass.java new file mode 100644 index 00000000000..2fd314083a5 --- /dev/null +++ b/jbmc/regression/jbmc/nondet-array-size/TestClass.java @@ -0,0 +1,11 @@ +import org.cprover.CProver; + +public class TestClass { + + public static void minimalJbmc(Object[] a) { + CProver.assume(a != null && a.length > 1); + float[] assigned = new float[a.length]; + assigned[0] = 1.0f; + assert(false); + } +} diff --git a/jbmc/regression/jbmc/nondet-array-size/test.desc b/jbmc/regression/jbmc/nondet-array-size/test.desc new file mode 100644 index 00000000000..c4069a8a128 --- /dev/null +++ b/jbmc/regression/jbmc/nondet-array-size/test.desc @@ -0,0 +1,16 @@ +CORE +TestClass.class +--function "TestClass.minimalJbmc" --unwind 5 --max-nondet-string-length 10 --java-unwind-enum-static --trace --json-ui +^EXIT=10$ +^SIGNAL=0$ +VERIFICATION FAILED +-- +-- +Verify that when an array's size is determined by an array input, the resulting +trace is valid. +To compile this source file, use: + +```bash +$ javac -g TestClass.java -cp ../../../lib/java-models-library/target/classes/:. +``` +to have the cprover library on the class path.