vsp = nondet ? malloc(a) : malloc(b) works correctly

Author: jezhiggins

regression/goto-analyzer/heap-allocation-nondet-1/main.c

@@ -1,9 +1,10 @@
 
-int main() {
-  int* q = malloc(10);
-  int* r = malloc(10);
+int main()
+{
+  int *q = malloc(10);
+  int *r = malloc(10);
 
   int *p = r;
-  if (nondet())
+  if(nondet())
     p = q;
 }

regression/goto-analyzer/heap-allocation-nondet-2/main.c

@@ -1,6 +1,7 @@
 
-int main() {
+int main()
+{
   int *p = malloc(10);
-  if (nondet())
+  if(nondet())
     ++p;
 }

regression/goto-analyzer/heap-allocation-nondet-3/main.c

@@ -1,9 +1,10 @@
 
-int main() {
+int main()
+{
   int *q = malloc(10);
   int r[10];
 
   int *p = r;
-  if (nondet())
+  if(nondet())
     p = q;
 }

regression/goto-analyzer/heap-allocation-nondet-4/main.c

@@ -1,9 +1,10 @@
 
-int main() {
+int main()
+{
   int *q = malloc(10);
   int r[10];
 
   int *p = q;
-  if (nondet())
+  if(nondet())
     p = r;
 }

regression/goto-analyzer/heap-allocation-nondet-5/main.c

@@ -0,0 +1,8 @@
+
+int main()
+{
+  int *p = malloc(10);
+
+  if(non_det())
+    p = malloc(20);
+}

regression/goto-analyzer/heap-allocation-nondet-5/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-1\[0\]\) :value-set-end
+--

regression/goto-analyzer/heap-allocation-nondet-6/main.c

@@ -0,0 +1,5 @@
+
+int main()
+{
+  int *p = nondet() ? malloc(10) : malloc(20);
+}

regression/goto-analyzer/heap-allocation-nondet-6/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-1\[0\]\) :value-set-end
+--

regression/goto-analyzer/heap-allocation-write-2/main.c

@@ -1,9 +1,10 @@
 
-int main() {
+int main()
+{
   int *p = malloc(sizeof(int) * 5);
-  int* q = malloc(sizeof(int) * 10);
+  int *q = malloc(sizeof(int) * 10);
 
-  int* pp = p;
+  int *pp = p;
 
   *p = 10;
   ++p;

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -115,6 +115,9 @@ abstract_object_pointert value_set_pointer_abstract_objectt::typecast(
   abstract_object_sett new_values;
   for(auto value : values)
   {
+    if(value->is_top()) // multiple mallocs in the same scope can cause spurious
+      continue; // TOP values, which we can safely strip out during the cast
+
     auto pointer =
       std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
     new_values.insert(pointer->typecast(new_type, environment, ns));