Partially restore array handling in parameter context

smowton · smowton · commit c08416ef26d0 · 2016-08-02T09:53:11.000+01:00
diff --git a/regression/test_gen/array_parameter/TestGenTest.class b/regression/test_gen/array_parameter/TestGenTest.class
diff --git a/regression/test_gen/array_parameter/TestGenTest.java b/regression/test_gen/array_parameter/TestGenTest.java
@@ -3,7 +3,7 @@ public class TestGenTest {
 
   public static void test(int[] got, A[] got2, long[] got3) {
 
-    assert(!(got != null && got[0] == 1 && got[1] == 2 && got2 != null && got2[0] != null && got2[1] != null && got2[0].x == 3 && got2[1].x == 4 && got3 != null && got3[0] == 100));
+    assert(!(got != null && got.length == 2 && got[0] == 1 && got[1] == 2 && got2 != null && got2.length == 2 && got2[0] != null && got2[1] != null && got2[0].x == 3 && got2[1].x == 4 && got3 != null && got3.length == 1 && got3[0] == 100));
 
   }
 
diff --git a/src/test_gen/java_test_source_factory.cpp b/src/test_gen/java_test_source_factory.cpp
@@ -433,7 +433,8 @@ void reference_factoryt::gather_referenced_symbols(const exprt& rhs, inputst& in
 {
   forall_operands(op_iter,rhs)
   {
-    if(op_iter->type().id()==ID_pointer)
+    if(op_iter->type().id()==ID_pointer ||
+       (op_iter->type().id()==ID_struct && rhs.id()==ID_address_of))
     {
       symbol_exprt underlying=try_find_underlying_symbol_expr(*op_iter);
       if(underlying!=symbol_exprt())

Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,7 @@ public class TestGenTest {`
`3`	`3`
`4`	`4`	`public static void test(int[] got, A[] got2, long[] got3) {`
`5`	`5`
`6`		`- assert(!(got != null && got[0] == 1 && got[1] == 2 && got2 != null && got2[0] != null && got2[1] != null && got2[0].x == 3 && got2[1].x == 4 && got3 != null && got3[0] == 100));`
	`6`	`+ assert(!(got != null && got.length == 2 && got[0] == 1 && got[1] == 2 && got2 != null && got2.length == 2 && got2[0] != null && got2[1] != null && got2[0].x == 3 && got2[1].x == 4 && got3 != null && got3.length == 1 && got3[0] == 100));`
`7`	`7`
`8`	`8`	`}`
`9`	`9`
Original file line number	Diff line number	Diff line change
`@@ -433,7 +433,8 @@ void reference_factoryt::gather_referenced_symbols(const exprt& rhs, inputst& in`
`433`	`433`	`{`
`434`	`434`	`forall_operands(op_iter,rhs)`
`435`	`435`	`{`
`436`		`- if(op_iter->type().id()==ID_pointer)`
	`436`	`+ if(op_iter->type().id()==ID_pointer \|\|`
	`437`	`+ (op_iter->type().id()==ID_struct && rhs.id()==ID_address_of))`
`437`	`438`	`{`
`438`	`439`	`symbol_exprt underlying=try_find_underlying_symbol_expr(*op_iter);`
`439`	`440`	`if(underlying!=symbol_exprt())`