Merge pull request #1050 from mgudemann/fix/revert_assert_non_nil_decl_assign_json_trace

Fix/revert assert non nil decl assign json trace

Author: Daniel Kroening

regression/cbmc-java/exceptions20/A.class

@@ -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

regression/cbmc-java/exceptions20/B.class

@@ -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;
+   }  
+ }
+}
+

regression/cbmc-java/exceptions20/C.class

@@ -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);
         }