From 3ccb482c323648da8f15c001e06895c2f02e247a Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Thu, 8 Sep 2016 10:29:02 +0100
Subject: [PATCH 1/2] Clean variable-length array size expressions. Fixes
 verification-engine-utils#192

This enables trace construction to reduce variable-length array
references down to constants, populating the full_lhs_value trace
member where previously it would have been a non-constant expression
such as `nil[0]` due to simplify_expr failing to evaluate the array
base expression.
---
 src/goto-symex/symex_builtin_functions.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index ed9c6262ee4..19cfe1f7e5c 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -478,7 +478,9 @@ void goto_symext::symex_cpp_new(
   {
     symbol.type=array_typet();
     symbol.type.subtype()=code.type().subtype();
-    symbol.type.set(ID_size, code.find(ID_size));
+    exprt size_arg=static_cast<const exprt&>(code.find(ID_size));
+    clean_expr(size_arg, state, false);
+    symbol.type.set(ID_size, size_arg);
   }
   else
     symbol.type=code.type().subtype();

From edb69089e090cb6fe1385ad4486691c2d4ac232b Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Wed, 4 Jan 2017 11:50:38 +0000
Subject: [PATCH 2/2] Add variable-length array trace test

Without the fix in 3ccb482c323648da8f15c001e06895c2f02e247a this
produces a trace containing nil expressions; with it, they are
successfully evaluated constant expresssions as expected.
---
 .../VarLengthArrayTrace1/Container.class      | Bin 0 -> 243 bytes
 .../VarLengthArrayTrace1.class                | Bin 0 -> 665 bytes
 .../VarLengthArrayTrace1.java                 |  21 ++++++++++++++++++
 .../cbmc-java/VarLengthArrayTrace1/test.desc  |  10 +++++++++
 4 files changed, 31 insertions(+)
 create mode 100644 regression/cbmc-java/VarLengthArrayTrace1/Container.class
 create mode 100644 regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.class
 create mode 100644 regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.java
 create mode 100644 regression/cbmc-java/VarLengthArrayTrace1/test.desc

diff --git a/regression/cbmc-java/VarLengthArrayTrace1/Container.class b/regression/cbmc-java/VarLengthArrayTrace1/Container.class
new file mode 100644
index 0000000000000000000000000000000000000000..fd0aca0d2472dd509cbe8148d7f48e1d610e6fb6
GIT binary patch
literal 243
zcmW+wyNbe45IqxPVzP04bYde`YM}_0iy(p^h!#rvNxWzz-oPaaewM|uu!SGsM~Pz?
z=FFTk56<)T{{S#S(}#_!hZ4SB)LhgFr7NcdS`wU}L?`)_VE2~&P|7^pD?)9RXtlna
zBV~3RrK0%T>|$cINIs+$vRNs8$d5B)__i|~tMTx}R}SE!5ugl*;LS6gvph0{`e!&w
zSszB5=%nIYO!WF8I%3Nfn<ObmMMv_ZB8n%h3rhm<2Y;YJ`xn-|*zpCO;;Je5CCozb
E2B@1Wh5!Hn

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.class b/regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.class
new file mode 100644
index 0000000000000000000000000000000000000000..3ec80acb986c9b93cc334f2de0b15d579bfeb2c8
GIT binary patch
literal 665
zcmZuv%T5$Q6g}0inkgD)7#_}mpx^)l5r_#<7sN<LO(x;7fRKQznw|<YG~J}Shs1?H
z!bW$lQR5_HbniE*@m5Eejhni+?&I8ZZq?5}U%vxb!;*kNjblQ<!eo(-yG0Z*#W5}5
znan+b`<UUFWf-Z;G*vnalQ?}5rm`KW4g))6@YcgP%$_mWjm3Qir<rsVLuoUN)pqx+
zt@NHLro@>HV+Oa;YMHvh-Ao3jTk<?l6AO+942AU|`UfX=ldcZbtI#yp_NCrb@lkfX
zp|yOor)8iXt(?dU>0=N>48>*=XEZ=*6R7)`!@Q3H_zYE3wi?O!Xm#U8!%M9b%`o~u
zSdIlB4J<O0`<*-O6BT3(*6S8YY2*^@3mMT4C{XGbHX~XT!+1xfp;n#Si6l4cQi8U0
zh#A_mphsZks^LhU4O$6?=q%A~iYz1RF7?2!Od-m2dU=q<Vi*<jP3c=|b;&-xhIKH}
zgT3|eGaUCFoGase6Whzq<j%6Q^4R$Z_Y##cr!3xM;2PdR5B!Hgw{rApaPnP3_XwS%
zW<CSmW{K((A~{0Y60BdSaE$&&onwq14CA+~*K&HmaHa4C#Y=GK104Gk-2RLk1qRE7
N<v%w%@8lG!e*t-mczgf=

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.java b/regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.java
new file mode 100644
index 00000000000..b014a545c7a
--- /dev/null
+++ b/regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.java
@@ -0,0 +1,21 @@
+public class VarLengthArrayTrace1 {
+
+  public static void main(int unknown, int arg2) {
+
+    Container c = new Container(unknown);
+    if(c.val != 2) return;
+    int[] arr = new int[c.val];
+    arr[1] = arg2;
+    int test = arr[1];
+    assert(test != 10);
+
+  }
+
+}
+
+class Container {
+
+  public Container(int v) { val = v; }
+  int val;
+
+}
diff --git a/regression/cbmc-java/VarLengthArrayTrace1/test.desc b/regression/cbmc-java/VarLengthArrayTrace1/test.desc
new file mode 100644
index 00000000000..74403444d22
--- /dev/null
+++ b/regression/cbmc-java/VarLengthArrayTrace1/test.desc
@@ -0,0 +1,10 @@
+CORE
+VarLengthArrayTrace1.class
+--trace
+^EXIT=10$
+^SIGNAL=0$
+dynamic_3_array\[1l\]=10
+--
+^warning: ignoring
+assignment removed
+irep("(\\"nil\\")")