From fa1fbb53e56c047d56ceec28b004b1072e235c74 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 9 Dec 2025 10:26:09 +0000 Subject: [PATCH] Add edge case regression tests for --generate-function-body const handling The existing tests provided basic const handling coverage, but several complex scenarios were not comprehensively tested. This PR addresses the following edge cases: 1. **Triple pointer const handling** - `int * const **` (const at middle level) 2. **Double const qualification** - `const int * const` (both pointer and data const) 3. **Array of pointers to const** - `const int **` / `const int *arr[]` 4. **Const function pointers** - `func_ptr_t * const` 5. **Nested struct const pointers** - Mixed const/non-const in nested structures 6. **Combined qualifiers** - `volatile const int *` (volatile + const interaction) 7. **Const array parameters** - `const int[]` (array parameter const protection) 8. **Pointer to const struct** - `const struct test_struct *` (struct-level const) 9. **Systematic const variations** - Comprehensive test of const at each pointer level Co-authored-by: Kiro autonomous agent Fixes: #1948 --- .../main.c | 33 ++++++ .../test.desc | 18 +++ .../main.c | 28 +++++ .../test.desc | 17 +++ .../main.c | 23 ++++ .../test.desc | 11 ++ .../main.c | 27 +++++ .../test.desc | 8 ++ .../main.c | 46 ++++++++ .../test.desc | 16 +++ .../main.c | 33 ++++++ .../test.desc | 15 +++ .../main.c | 103 ++++++++++++++++++ .../test.desc | 28 +++++ .../main.c | 35 ++++++ .../test.desc | 12 ++ .../main.c | 24 ++++ .../test.desc | 11 ++ 18 files changed, 488 insertions(+) create mode 100644 regression/goto-instrument/generate-function-body-array-of-pointers-to-const/main.c create mode 100644 regression/goto-instrument/generate-function-body-array-of-pointers-to-const/test.desc create mode 100644 regression/goto-instrument/generate-function-body-const-array-parameter/main.c create mode 100644 regression/goto-instrument/generate-function-body-const-array-parameter/test.desc create mode 100644 regression/goto-instrument/generate-function-body-const-pointer-to-const/main.c create mode 100644 regression/goto-instrument/generate-function-body-const-pointer-to-const/test.desc create mode 100644 regression/goto-instrument/generate-function-body-function-pointer-const/main.c create mode 100644 regression/goto-instrument/generate-function-body-function-pointer-const/test.desc create mode 100644 regression/goto-instrument/generate-function-body-nested-struct-const-pointers/main.c create mode 100644 regression/goto-instrument/generate-function-body-nested-struct-const-pointers/test.desc create mode 100644 regression/goto-instrument/generate-function-body-pointer-to-const-struct/main.c create mode 100644 regression/goto-instrument/generate-function-body-pointer-to-const-struct/test.desc create mode 100644 regression/goto-instrument/generate-function-body-pointer-variations-const/main.c create mode 100644 regression/goto-instrument/generate-function-body-pointer-variations-const/test.desc create mode 100644 regression/goto-instrument/generate-function-body-triple-pointer-const-middle/main.c create mode 100644 regression/goto-instrument/generate-function-body-triple-pointer-const-middle/test.desc create mode 100644 regression/goto-instrument/generate-function-body-volatile-const-pointers/main.c create mode 100644 regression/goto-instrument/generate-function-body-volatile-const-pointers/test.desc diff --git a/regression/goto-instrument/generate-function-body-array-of-pointers-to-const/main.c b/regression/goto-instrument/generate-function-body-array-of-pointers-to-const/main.c new file mode 100644 index 00000000000..32d3fadf761 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-array-of-pointers-to-const/main.c @@ -0,0 +1,33 @@ +#include + +// 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; +} diff --git a/regression/goto-instrument/generate-function-body-array-of-pointers-to-const/test.desc b/regression/goto-instrument/generate-function-body-array-of-pointers-to-const/test.desc new file mode 100644 index 00000000000..c3d6f47637e --- /dev/null +++ b/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$ +-- \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-const-array-parameter/main.c b/regression/goto-instrument/generate-function-body-const-array-parameter/main.c new file mode 100644 index 00000000000..0a30757e601 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-const-array-parameter/main.c @@ -0,0 +1,28 @@ +#include + +// 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; +} \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-const-array-parameter/test.desc b/regression/goto-instrument/generate-function-body-const-array-parameter/test.desc new file mode 100644 index 00000000000..0adef79a7f3 --- /dev/null +++ b/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$ +-- \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-const-pointer-to-const/main.c b/regression/goto-instrument/generate-function-body-const-pointer-to-const/main.c new file mode 100644 index 00000000000..5e4de30f558 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-const-pointer-to-const/main.c @@ -0,0 +1,23 @@ +#include + +// 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; +} diff --git a/regression/goto-instrument/generate-function-body-const-pointer-to-const/test.desc b/regression/goto-instrument/generate-function-body-const-pointer-to-const/test.desc new file mode 100644 index 00000000000..daffbb2ba5e --- /dev/null +++ b/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$ +-- \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-function-pointer-const/main.c b/regression/goto-instrument/generate-function-body-function-pointer-const/main.c new file mode 100644 index 00000000000..d8639b4a6db --- /dev/null +++ b/regression/goto-instrument/generate-function-body-function-pointer-const/main.c @@ -0,0 +1,27 @@ +#include + +// 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; +} diff --git a/regression/goto-instrument/generate-function-body-function-pointer-const/test.desc b/regression/goto-instrument/generate-function-body-function-pointer-const/test.desc new file mode 100644 index 00000000000..8f5a35fb741 --- /dev/null +++ b/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$ +-- \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-nested-struct-const-pointers/main.c b/regression/goto-instrument/generate-function-body-nested-struct-const-pointers/main.c new file mode 100644 index 00000000000..c78b8543962 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-nested-struct-const-pointers/main.c @@ -0,0 +1,46 @@ +#include + +// 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; +} \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-nested-struct-const-pointers/test.desc b/regression/goto-instrument/generate-function-body-nested-struct-const-pointers/test.desc new file mode 100644 index 00000000000..ca875b6297f --- /dev/null +++ b/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$ +-- \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-pointer-to-const-struct/main.c b/regression/goto-instrument/generate-function-body-pointer-to-const-struct/main.c new file mode 100644 index 00000000000..2cacc1562e8 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-pointer-to-const-struct/main.c @@ -0,0 +1,33 @@ +#include + +// 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; +} \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-pointer-to-const-struct/test.desc b/regression/goto-instrument/generate-function-body-pointer-to-const-struct/test.desc new file mode 100644 index 00000000000..4e881fd2aa3 --- /dev/null +++ b/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$ +-- \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-pointer-variations-const/main.c b/regression/goto-instrument/generate-function-body-pointer-variations-const/main.c new file mode 100644 index 00000000000..0e9eed01df6 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-pointer-variations-const/main.c @@ -0,0 +1,103 @@ +#include + +// Comprehensive test for various pointer-to-pointer-to-const variations +// These test different positions where const can appear in multi-level pointers + +// Test case 1: const int ** (pointer to pointer to const int) +void havoc_pp_const_int(const int **pp); + +// Test case 2: int * const * (pointer to const pointer to int) +void havoc_p_const_p_int(int *const *pp); + +// Test case 3: int ** const (const pointer to pointer to int) +void havoc_const_pp_int(int **const pp); + +// Test case 4: const int * const * (pointer to const pointer to const int) +void havoc_p_const_p_const_int(const int *const *pp); + +// Test case 5: const int ** const (const pointer to pointer to const int) +void havoc_const_pp_const_int(const int **const pp); + +int main(void) +{ + // Test data + int a = 1, b = 2, c = 3, d = 4, e = 5; + + // Test case 1: const int ** + { + int *pa = &a; + const int **pp1 = (const int **)&pa; + + assert(a == 1); + assert(**pp1 == 1); + + havoc_pp_const_int(pp1); + + // The int value should be preserved (const int) + assert(a == 1); + // But the pointer relationships may change + assert(**pp1 == 1); // May fail due to pointer modification + } + + // Test case 2: int * const * + { + int *pb = &b; + int *const *pp2 = &pb; + + assert(b == 2); + assert(**pp2 == 2); + + havoc_p_const_p_int(pp2); + + // The int value may be modified (not const), but const pointer should remain + assert(b == 2); // May fail - int is not const + assert(*pp2 == pb); // Should succeed - const pointer + } + + // Test case 3: int ** const + { + int *pc = &c; + int **const pp3 = &pc; + + assert(c == 3); + assert(**pp3 == 3); + + havoc_const_pp_int(pp3); + + // The outer pointer is const, but inner data can change + assert(c == 3); // May fail - int is not const + assert(*pp3 == pc); // May fail - inner pointer not const + } + + // Test case 4: const int * const * + { + int *pd = &d; + const int *const *pp4 = (const int *const *)&pd; + + assert(d == 4); + assert(**pp4 == 4); + + havoc_p_const_p_const_int(pp4); + + // Both int and middle pointer are const + assert(d == 4); // Should succeed - const int + assert(**pp4 == 4); // Should succeed - const int + } + + // Test case 5: const int ** const + { + int *pe = &e; + const int **const pp5 = (const int **)&pe; + + assert(e == 5); + assert(**pp5 == 5); + + havoc_const_pp_const_int(pp5); + + // Outer pointer is const, int is const, but middle pointer is not + assert(e == 5); // Should succeed - const int + assert(**pp5 == 5); // May fail - middle pointer can change + } + + return 0; +} \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-pointer-variations-const/test.desc b/regression/goto-instrument/generate-function-body-pointer-variations-const/test.desc new file mode 100644 index 00000000000..1f038a5333e --- /dev/null +++ b/regression/goto-instrument/generate-function-body-pointer-variations-const/test.desc @@ -0,0 +1,28 @@ +CORE +main.c +--generate-function-body "havoc_.*" --generate-function-body-options havoc,params:.* +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion a == 1: SUCCESS$ +^\[main.assertion.2\] .* assertion \*\*pp1 == 1: SUCCESS$ +^\[main.assertion.3\] .* assertion a == 1: SUCCESS$ +^\[main.assertion.4\] .* assertion \*\*pp1 == 1: FAILURE$ +^\[main.assertion.5\] .* assertion b == 2: SUCCESS$ +^\[main.assertion.6\] .* assertion \*\*pp2 == 2: SUCCESS$ +^\[main.assertion.7\] .* assertion b == 2: FAILURE$ +^\[main.assertion.8\] .* assertion \*pp2 == pb: SUCCESS$ +^\[main.assertion.9\] .* assertion c == 3: SUCCESS$ +^\[main.assertion.10\] .* assertion \*\*pp3 == 3: SUCCESS$ +^\[main.assertion.11\] .* assertion c == 3: FAILURE$ +^\[main.assertion.12\] .* assertion \*pp3 == pc: FAILURE$ +^\[main.assertion.13\] .* assertion d == 4: SUCCESS$ +^\[main.assertion.14\] .* assertion \*\*pp4 == 4: SUCCESS$ +^\[main.assertion.15\] .* assertion d == 4: SUCCESS$ +^\[main.assertion.16\] .* assertion \*\*pp4 == 4: SUCCESS$ +^\[main.assertion.17\] .* assertion e == 5: SUCCESS$ +^\[main.assertion.18\] .* assertion \*\*pp5 == 5: SUCCESS$ +^\[main.assertion.19\] .* assertion e == 5: SUCCESS$ +^\[main.assertion.20\] .* assertion \*\*pp5 == 5: FAILURE$ +-- +Test various combinations of const qualifiers in multi-level pointers +to ensure proper handling of const at different pointer levels \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-triple-pointer-const-middle/main.c b/regression/goto-instrument/generate-function-body-triple-pointer-const-middle/main.c new file mode 100644 index 00000000000..c5dd08521a5 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-triple-pointer-const-middle/main.c @@ -0,0 +1,35 @@ +#include + +// Edge case: const is on the middle pointer level +// int * const ** means the middle pointer is const, but the outer pointer +// and the int can be modified +void havoc_triple_pointer_const_middle(int *const **triple_ptr); + +int main(void) +{ + int x = 42; + int y = 100; + int *ptr_to_x = &x; + int *ptr_to_y = &y; + int *const *ptr_to_const_ptr = &ptr_to_x; // const middle pointer + int *const **triple_ptr = &ptr_to_const_ptr; + + // Initial assertions + assert(x == 42); + assert(y == 100); + assert(**triple_ptr == &x); + assert(***triple_ptr == 42); + + // This should havoc the outer pointer and potentially the pointed-to data + // but the middle const pointer level should remain unchanged + havoc_triple_pointer_const_middle(triple_ptr); + + // After havoc: + // - x and y values should be preserved (pointed-to const data) + // - The const middle pointer relationship should be preserved + // - But the outer pointer could be modified + assert(x == 42); // Should succeed - const protects this + assert(y == 100); // Should succeed - const protects this + + return 0; +} diff --git a/regression/goto-instrument/generate-function-body-triple-pointer-const-middle/test.desc b/regression/goto-instrument/generate-function-body-triple-pointer-const-middle/test.desc new file mode 100644 index 00000000000..b053b7dabb6 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-triple-pointer-const-middle/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--generate-function-body havoc_triple_pointer_const_middle --generate-function-body-options havoc,params:.* +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x == 42: SUCCESS$ +^\[main.assertion.2\] .* assertion y == 100: SUCCESS$ +^\[main.assertion.3\] .* assertion \*\*triple_ptr == &x: SUCCESS$ +^\[main.assertion.4\] .* assertion \*\*\*triple_ptr == 42: SUCCESS$ +^\[main.assertion.5\] .* assertion x == 42: FAILURE$ +^\[main.assertion.6\] .* assertion y == 100: FAILURE$ +-- \ No newline at end of file diff --git a/regression/goto-instrument/generate-function-body-volatile-const-pointers/main.c b/regression/goto-instrument/generate-function-body-volatile-const-pointers/main.c new file mode 100644 index 00000000000..59d1189ef8e --- /dev/null +++ b/regression/goto-instrument/generate-function-body-volatile-const-pointers/main.c @@ -0,0 +1,24 @@ +#include + +// Edge case: volatile and const qualifiers together +// volatile const int * means pointer to volatile const data +void havoc_volatile_const_pointer(volatile const int *ptr); + +int main(void) +{ + volatile int x = 77; + volatile const int *ptr = &x; + + assert(x == 77); + assert(*ptr == 77); + + // With const qualifier, the pointed-to value should not be modified + // even though it's volatile + havoc_volatile_const_pointer(ptr); + + // Should succeed due to const + assert(x == 77); + assert(*ptr == 77); + + return 0; +} diff --git a/regression/goto-instrument/generate-function-body-volatile-const-pointers/test.desc b/regression/goto-instrument/generate-function-body-volatile-const-pointers/test.desc new file mode 100644 index 00000000000..66be5f08d00 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-volatile-const-pointers/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--generate-function-body havoc_volatile_const_pointer --generate-function-body-options havoc,params:.* +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x == 77: SUCCESS$ +^\[main.assertion.2\] .* assertion \*ptr == 77: SUCCESS$ +^\[main.assertion.3\] .* assertion x == 77: SUCCESS$ +^\[main.assertion.4\] .* assertion \*ptr == 77: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- \ No newline at end of file