Properly type initial value of __CPROVER_max_malloc_size

tautschnig · tautschnig · commit 28e423890708 · 2023-08-23T12:27:14.000Z
Use a suffix to ensure the constant isn't treated as an int, but instead
matches the left-hand side's type.
diff --git a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 1, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 10, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 1, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 10, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 3, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 3, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --vsd-arrays every-element --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 2, assigns: 7, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: [12], function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 2, assigns: [89], function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_08/test.desc b/regression/goto-analyzer/constant_propagation_08/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 4, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 4, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 4, assigns: 14, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --vsd-arrays every-element --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 6, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: [12], function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: [78], function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 6, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: [12], function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: [78], function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 7, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 1, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 8, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 7, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 1, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 8, function calls: 2$
 --
 ^warning: ignoring
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -183,8 +183,15 @@ void ansi_c_internal_additions(std::string &code)
 
     CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
     integer2string(max_malloc_size(config.ansi_c.pointer_width, config
-    .bv_encoding.object_bits))+";\n"
+    .bv_encoding.object_bits));
+  if(config.ansi_c.pointer_width==config.ansi_c.long_int_width)
+    code += "UL;\n";
+  else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
+    code += "ULL;\n";
+  else
+    code += "U;\n";
 
+  code+=
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["
       CPROVER_PREFIX "constant_infinity_uint];\n"
