Add edge case regression tests for --generate-function-body const handling

regression/goto-instrument/generate-function-body-array-of-pointers-to-const/main.c

@@ -0,0 +1,33 @@
+#include <assert.h>
+
+// Edge case: array of pointers where each pointer points to const data
+// const int *arr[] - array elements are pointers to const int
+void havoc_array_of_pointers_to_const(const int **arr, int size);
+
+int main(void)
+{
+  int a = 10, b = 20, c = 30;
+  const int *arr[] = {&a, &b, &c};
+
+  assert(a == 10);
+  assert(b == 20);
+  assert(c == 30);
+  assert(*arr[0] == 10);
+  assert(*arr[1] == 20);
+  assert(*arr[2] == 30);
+
+  // Havoc the array - pointers can change but const data should be preserved
+  havoc_array_of_pointers_to_const(arr, 3);
+
+  // The underlying int values should remain unchanged due to const
+  assert(a == 10);
+  assert(b == 20);
+  assert(c == 30);
+
+  // But the array pointers could point elsewhere, so these may fail
+  assert(*arr[0] == 10);
+  assert(*arr[1] == 20);
+  assert(*arr[2] == 30);
+
+  return 0;
+}

regression/goto-instrument/generate-function-body-array-of-pointers-to-const/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--generate-function-body havoc_array_of_pointers_to_const --generate-function-body-options havoc,params:.*
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion a == 10: SUCCESS$
+^\[main.assertion.2\] .* assertion b == 20: SUCCESS$
+^\[main.assertion.3\] .* assertion c == 30: SUCCESS$
+^\[main.assertion.4\] .* assertion \*arr\[0\] == 10: SUCCESS$
+^\[main.assertion.5\] .* assertion \*arr\[1\] == 20: SUCCESS$
+^\[main.assertion.6\] .* assertion \*arr\[2\] == 30: SUCCESS$
+^\[main.assertion.7\] .* assertion a == 10: SUCCESS$
+^\[main.assertion.8\] .* assertion b == 20: SUCCESS$
+^\[main.assertion.9\] .* assertion c == 30: SUCCESS$
+^\[main.assertion.10\] .* assertion \*arr\[0\] == 10 FAILURE$
+^\[main.assertion.11\] .* assertion \*arr\[1\] == 20: FAILURE$
+^\[main.assertion.12\] .* assertion \*arr\[2\] == 30: FAILURE$
+--

regression/goto-instrument/generate-function-body-const-array-parameter/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+// Edge case: const array parameter
+// const int arr[] is equivalent to const int *arr
+void havoc_const_array(const int arr[], int size);
+
+int main(void)
+{
+  int data[] = {1, 2, 3, 4, 5};
+
+  assert(data[0] == 1);
+  assert(data[1] == 2);
+  assert(data[2] == 3);
+  assert(data[3] == 4);
+  assert(data[4] == 5);
+
+  // Array parameter with const should not allow modification of elements
+  havoc_const_array(data, 5);
+
+  // All should succeed due to const
+  assert(data[0] == 1);
+  assert(data[1] == 2);
+  assert(data[2] == 3);
+  assert(data[3] == 4);
+  assert(data[4] == 5);
+
+  return 0;
+}

regression/goto-instrument/generate-function-body-const-array-parameter/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--generate-function-body havoc_const_array --generate-function-body-options havoc,params:.*
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion data\[0\] == 1: SUCCESS$
+^\[main.assertion.2\] .* assertion data\[1\] == 2: SUCCESS$
+^\[main.assertion.3\] .* assertion data\[2\] == 3: SUCCESS$
+^\[main.assertion.4\] .* assertion data\[3\] == 4: SUCCESS$
+^\[main.assertion.5\] .* assertion data\[4\] == 5: SUCCESS$
+^\[main.assertion.6\] .* assertion data\[0\] == 1: SUCCESS$
+^\[main.assertion.7\] .* assertion data\[1\] == 2: SUCCESS$
+^\[main.assertion.8\] .* assertion data\[2\] == 3: SUCCESS$
+^\[main.assertion.9\] .* assertion data\[3\] == 4: SUCCESS$
+^\[main.assertion.10\] .* assertion data\[4\] == 5: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--

regression/goto-instrument/generate-function-body-const-pointer-to-const/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+
+// Edge case: both pointer and pointed-to data are const
+// const int * const means neither the pointer nor the data can be modified
+void havoc_const_pointer_to_const(const int *const param);
+
+int main(void)
+{
+  int x = 55;
+  const int *const ptr = &x;
+
+  assert(x == 55);
+  assert(*ptr == 55);
+
+  // With both const qualifiers, havoc should not modify anything
+  havoc_const_pointer_to_const(ptr);
+
+  // Both should succeed since everything is const
+  assert(x == 55);
+  assert(*ptr == 55);
+
+  return 0;
+}

regression/goto-instrument/generate-function-body-const-pointer-to-const/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--generate-function-body havoc_const_pointer_to_const --generate-function-body-options havoc,params:.*
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion x == 55: SUCCESS$
+^\[main.assertion.2\] .* assertion \*ptr == 55: SUCCESS$
+^\[main.assertion.3\] .* assertion x == 55: SUCCESS$
+^\[main.assertion.4\] .* assertion \*ptr == 55: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--

regression/goto-instrument/generate-function-body-function-pointer-const/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+
+// Edge case: const function pointer
+// int (* const fp)(void) means the function pointer itself is const
+typedef int (*func_ptr_t)(void);
+
+int test_function(void)
+{
+  return 42;
+}
+
+void havoc_const_function_pointer(func_ptr_t *const func_ptr);
+
+int main(void)
+{
+  func_ptr_t fp = test_function;
+  func_ptr_t *const const_fp_ptr = &fp;
+
+  // The function pointer itself should not be modifiable
+  havoc_const_function_pointer(const_fp_ptr);
+
+  // Since the pointer to the function pointer is const,
+  // the function pointer itself should remain unchanged
+  assert(fp == test_function);
+
+  return 0;
+}

regression/goto-instrument/generate-function-body-function-pointer-const/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body havoc_const_function_pointer --generate-function-body-options havoc,params:.*
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion fp == test_function: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--

regression/goto-instrument/generate-function-body-nested-struct-const-pointers/main.c

@@ -0,0 +1,46 @@
+#include <assert.h>
+
+// Edge case: nested struct with mixed const pointer qualifiers
+struct inner
+{
+  const int *const_ptr; // pointer to const
+  int *normal_ptr;      // normal pointer
+};
+
+struct outer
+{
+  struct inner *const const_inner_ptr;  // const pointer to struct
+  struct inner *normal_inner_ptr;       // normal pointer to struct
+  const struct inner *const_struct_ptr; // pointer to const struct
+};
+
+void havoc_nested_struct_const_pointers(struct outer *s);
+
+int main(void)
+{
+  int x = 100, y = 200, z = 300, w = 400;
+
+  struct inner inner1 = {&x, &y};
+  struct inner inner2 = {&z, &w};
+  struct outer outer_struct = {&inner1, &inner2, &inner1};
+
+  // Initial state
+  assert(x == 100);
+  assert(y == 200);
+  assert(z == 300);
+  assert(w == 400);
+  assert(*outer_struct.const_inner_ptr->const_ptr == 100);
+  assert(*outer_struct.const_inner_ptr->normal_ptr == 200);
+
+  havoc_nested_struct_const_pointers(&outer_struct);
+
+  // Values pointed to by const pointers should be preserved
+  assert(x == 100); // pointed to by const_ptr
+  assert(z == 300); // pointed to by const_ptr in inner2
+
+  // Values pointed to by normal pointers may be modified
+  assert(y == 200); // may fail - pointed to by normal_ptr
+  assert(w == 400); // may fail - pointed to by normal_ptr
+
+  return 0;
+}

regression/goto-instrument/generate-function-body-nested-struct-const-pointers/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--generate-function-body havoc_nested_struct_const_pointers --generate-function-body-options havoc,params:.*
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion x == 100: SUCCESS$
+^\[main.assertion.2\] .* assertion y == 200: SUCCESS$
+^\[main.assertion.3\] .* assertion z == 300: SUCCESS$
+^\[main.assertion.4\] .* assertion w == 400: SUCCESS$
+^\[main.assertion.5\] .* assertion \*outer_struct.const_inner_ptr->const_ptr == 100: SUCCESS$
+^\[main.assertion.6\] .* assertion \*outer_struct.const_inner_ptr->normal_ptr == 200: SUCCESS$
+^\[main.assertion.7\] .* assertion x == 100: SUCCESS$
+^\[main.assertion.8\] .* assertion z == 300: SUCCESS$
+^\[main.assertion.9\] .* assertion y == 200: FAILURE$
+^\[main.assertion.10\] .* assertion w == 400: FAILURE$
+--

regression/goto-instrument/generate-function-body-pointer-to-const-struct/main.c

@@ -0,0 +1,33 @@
+#include <assert.h>
+
+// Edge case: pointer to const struct (entire struct is const)
+struct test_struct
+{
+  int a;
+  int b;
+  int *ptr;
+};
+
+void havoc_pointer_to_const_struct(const struct test_struct *s);
+
+int main(void)
+{
+  int x = 500;
+  struct test_struct s = {10, 20, &x};
+
+  assert(s.a == 10);
+  assert(s.b == 20);
+  assert(x == 500);
+  assert(*s.ptr == 500);
+
+  // Const struct means all members are const
+  havoc_pointer_to_const_struct(&s);
+
+  // All struct members should be preserved due to const
+  assert(s.a == 10);
+  assert(s.b == 20);
+  assert(x == 500);      // x itself might still be modifiable
+  assert(*s.ptr == 500); // but accessed through const struct should be stable
+
+  return 0;
+}

regression/goto-instrument/generate-function-body-pointer-to-const-struct/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--generate-function-body havoc_pointer_to_const_struct --generate-function-body-options havoc,params:.*
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion s.a == 10: SUCCESS$
+^\[main.assertion.2\] .* assertion s.b == 20: SUCCESS$
+^\[main.assertion.3\] .* assertion x == 500: SUCCESS$
+^\[main.assertion.4\] .* assertion \*s.ptr == 500: SUCCESS$
+^\[main.assertion.5\] .* assertion s.a == 10: SUCCESS$
+^\[main.assertion.6\] .* assertion s.b == 20: SUCCESS$
+^\[main.assertion.7\] .* assertion x == 500: SUCCESS$
+^\[main.assertion.8\] .* assertion \*s.ptr == 500: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--