From d299ea29e0a51c4f78d62ea35f4f8cfd957894e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 21 Jun 2017 17:55:54 +0200 Subject: [PATCH 1/2] Allow "unknown" value assignments in JSON trace With the exception_value support, there is the possibility to have `nil` values assigned in the trace. These values are returned from `prop_conv.get(expr)`. --- src/goto-programs/json_goto_trace.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 316b83b41f7..3f4397f3c8e 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -208,7 +208,6 @@ void convert( type_string=from_type(ns, identifier, symbol->type); json_assignment["mode"]=json_stringt(id2string(symbol->mode)); - assert(step.full_lhs_value.is_not_nil()); exprt simplified=simplify_array_access(step.full_lhs_value); full_lhs_value=json(simplified, ns, symbol->mode); } From 82642b9599592b25d41c61f25a642fa9889a422b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 21 Jun 2017 19:11:45 +0200 Subject: [PATCH 2/2] Add regression test for nil assigns in JSON trace --- regression/cbmc-java/exceptions20/A.class | Bin 0 -> 234 bytes regression/cbmc-java/exceptions20/B.class | Bin 0 -> 216 bytes regression/cbmc-java/exceptions20/C.class | Bin 0 -> 216 bytes regression/cbmc-java/exceptions20/D.class | Bin 0 -> 216 bytes regression/cbmc-java/exceptions20/test.class | Bin 0 -> 1025 bytes regression/cbmc-java/exceptions20/test.desc | 11 +++++++ regression/cbmc-java/exceptions20/test.java | 30 +++++++++++++++++++ 7 files changed, 41 insertions(+) create mode 100644 regression/cbmc-java/exceptions20/A.class create mode 100644 regression/cbmc-java/exceptions20/B.class create mode 100644 regression/cbmc-java/exceptions20/C.class create mode 100644 regression/cbmc-java/exceptions20/D.class create mode 100644 regression/cbmc-java/exceptions20/test.class create mode 100644 regression/cbmc-java/exceptions20/test.desc create mode 100644 regression/cbmc-java/exceptions20/test.java diff --git a/regression/cbmc-java/exceptions20/A.class b/regression/cbmc-java/exceptions20/A.class new file mode 100644 index 0000000000000000000000000000000000000000..eb19ef6be2b4b0dc315cdfd2ae091ecc67882efd GIT binary patch literal 234 zcmXX=%MQU%5IsX5TBX7dSYn|YJ0fW$R*em@zv_l7)h5;QT~-ncAK;_J+%n0`dF0Gw z-k;|Szyuu^b+l}>ZTJLhrczbR3H8BnOE4DMUK0FBrE*oCcQW6IUBXT`%3_ghMXt2| zn?`X|7ha9RDZyQ5Wgg3=(s8GdmtuSpSK+~cNuZF>(>h2*dI&bhJiF;j=%dE}=pt^; iGFr?6M(voR2k6eE2Aii7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|N0ia<-WNlvOJ0;V`m%{smNkcs&?*7 zqdu#OPor>6a1TXOrgEp+xKqojUR=aYcraiRC}aefK;!Ri5ra3(7ON$5>zMNg=*~ie V&E4u^J=Weo00%Blg#It(eE}M}B0B&8 literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/exceptions20/test.class b/regression/cbmc-java/exceptions20/test.class new file mode 100644 index 0000000000000000000000000000000000000000..c76687b1bc7a0547086d763afd30f531210e3b7a GIT binary patch literal 1025 zcmZuvZBNr+6g|({ty|ZPF%&@&5kWUp<_m&uXoR7Oro#^y5+Q+fTZQ82Ok0eORw}P5==E;f zRp_%l-(B9@ZMwl*NmeM@-Imi?bplWPlb{}Ldm($+ksC%eR_{8VuP|6zw|AURPNn1c zTa}e4@cgZsbXOdz*-Ok+EkSibO+kx-96<|$I8bvxOO6w4asB`FQ^>7EPU}O%`513Q zai|L=p&AP5`BvwIn7Pv33tH|=PiSOh(`i}GLJ#!;P(Z)J(AoA2e|38i z1l@oXrGbH}g&O7+3TK&bnmcYQqIPGYdWW)8kG30nf!jXq#l@pN{z1*xaGkH#$5&Q` zA(>93fqG+r_XT(nJgW;RQ;<1aL6vgU$mkWZP0kH+T_@fk z*G;nB#Yn8gd-h3VjQ@;Kfdczo#VEHBX|FM^vAe-D&W$GN-5^SGN*)t&MJ-07tZl?- zjA%1P<3!YvRX1sG@eCrpZJ?B2G*FgnO0L^^&cAc|cr$So&|l1bLw+BIegIwj3iJF! RO3Ne?)^mC8yL1wm{teh!r=|b^ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/exceptions20/test.desc b/regression/cbmc-java/exceptions20/test.desc new file mode 100644 index 00000000000..72829197eb8 --- /dev/null +++ b/regression/cbmc-java/exceptions20/test.desc @@ -0,0 +1,11 @@ +CORE +test.class +--json-ui --trace +^EXIT=10$ +^SIGNAL=0$ +.*VERIFICATION FAILED.* +-- +^warning: ignoring +-- +this fails with assertion error if nil values are not allowed in assignments in +the JSON trace diff --git a/regression/cbmc-java/exceptions20/test.java b/regression/cbmc-java/exceptions20/test.java new file mode 100644 index 00000000000..bc925b32d65 --- /dev/null +++ b/regression/cbmc-java/exceptions20/test.java @@ -0,0 +1,30 @@ +class A extends Throwable {} +class B extends A {} +class C extends B {} +class D extends C {} + +public class test { + public static void main (String arg[]) { + try { + D d = new D(); + C c = new C(); + B b = new B(); + A a = new A(); + A e = a; + throw e; + } + catch(D exc) { + assert false; + } + catch(C exc) { + assert false; + } + catch(B exc) { + assert false; + } + catch(A exc) { + assert false; + } + } +} +