Skip to content

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

Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:fix-1948-more-tests
Open

Add edge case regression tests for --generate-function-body const handling#8797
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:fix-1948-more-tests

Conversation

@tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Dec 9, 2025

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

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig changed the title Add edge case regression tests for --generate-function-body const han… Add edge case regression tests for --generate-function-body const handling Dec 9, 2025
@tautschnig tautschnig self-assigned this Feb 24, 2026
@tautschnig tautschnig force-pushed the fix-1948-more-tests branch from fa1fbb5 to 227164e Compare March 10, 2026 17:14
@tautschnig tautschnig marked this pull request as ready for review March 10, 2026 19:15
Copilot AI review requested due to automatic review settings March 10, 2026 19:15
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

Adds regression coverage for --generate-function-body around tricky const/volatile qualifier placement, especially across multi-level pointers, arrays, structs, and function-pointer indirections.

Changes:

  • Introduces new regression test directories covering volatile+const, const at different pointer levels, and const in structs/arrays.
  • Adds systematic “pointer variations” test that mixes const placement across **/* const */** const forms.
  • Adds negative tests (expected assertion failures) where pointer relationships are allowed to change.

Reviewed changes

Copilot reviewed 18 out of 18 changed files in this pull request and generated 11 comments.

Show a summary per file
File Description
regression/goto-instrument/generate-function-body-volatile-const-pointers/test.desc New harness expectations for volatile+const pointer test
regression/goto-instrument/generate-function-body-volatile-const-pointers/main.c Adds volatile+const pointer regression scenario
regression/goto-instrument/generate-function-body-triple-pointer-const-middle/test.desc New harness expectations for middle-level const triple pointer test
regression/goto-instrument/generate-function-body-triple-pointer-const-middle/main.c Adds triple-pointer “const in middle” regression scenario
regression/goto-instrument/generate-function-body-pointer-variations-const/test.desc Adds multi-variant const pointer-level expectations
regression/goto-instrument/generate-function-body-pointer-variations-const/main.c Implements const-placement matrix for pointer-to-pointer cases
regression/goto-instrument/generate-function-body-pointer-to-const-struct/test.desc New harness expectations for pointer-to-const-struct test
regression/goto-instrument/generate-function-body-pointer-to-const-struct/main.c Adds regression scenario for const-qualified struct pointer
regression/goto-instrument/generate-function-body-nested-struct-const-pointers/test.desc New harness expectations for nested struct const-pointer test
regression/goto-instrument/generate-function-body-nested-struct-const-pointers/main.c Adds nested struct scenario mixing const and non-const pointers
regression/goto-instrument/generate-function-body-function-pointer-const/test.desc Adds expected-failure harness for const function-pointer indirection
regression/goto-instrument/generate-function-body-function-pointer-const/main.c Adds function-pointer constness regression scenario
regression/goto-instrument/generate-function-body-const-pointer-to-const/test.desc New harness expectations for const int * const
regression/goto-instrument/generate-function-body-const-pointer-to-const/main.c Adds double-const pointer regression scenario
regression/goto-instrument/generate-function-body-const-array-parameter/test.desc New harness expectations for const array parameter
regression/goto-instrument/generate-function-body-const-array-parameter/main.c Adds const array parameter regression scenario
regression/goto-instrument/generate-function-body-array-of-pointers-to-const/test.desc Adds expected-failure harness for array-of-pointers-to-const
regression/goto-instrument/generate-function-body-array-of-pointers-to-const/main.c Adds array-of-pointers-to-const regression scenario

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@@ -0,0 +1,28 @@
CORE
main.c
--generate-function-body "havoc_.*" --generate-function-body-options havoc,params:.*
Copy link

Copilot AI Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

test.desc arguments are typically tokenized and passed directly (not via a shell), so the quotes are likely to be treated as literal characters. That can prevent the regex from matching any function names. Drop the quotes so the tool receives havoc_.* as the pattern.

Suggested change
--generate-function-body "havoc_.*" --generate-function-body-options havoc,params:.*
--generate-function-body havoc_.* --generate-function-body-options havoc,params:.*

Copilot uses AI. Check for mistakes.
^\[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$
Copy link

Copilot AI Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The expected output format is inconsistent with the other failure lines (missing : before FAILURE). This regex likely won’t match the actual assertion output, causing a harness mismatch. Make it consistent with the surrounding patterns (e.g., ... == 10: FAILURE).

Suggested change
^\[main.assertion.10\] .* assertion \*arr\[0\] == 10 FAILURE$
^\[main.assertion.10\] .* assertion \*arr\[0\] == 10: FAILURE$

Copilot uses AI. Check for mistakes.
// Test case 1: const int **
{
int *pa = &a;
const int **pp1 = (const int **)&pa;
Copy link

Copilot AI Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These casts form invalid/unsafe pointer type conversions in C (notably int **const int **), and can trigger compiler diagnostics (often fatal under -Werror) and/or undefined behavior. Instead, introduce correctly-typed intermediate variables (e.g., const int *) so you can take their addresses without casting.

Copilot uses AI. Check for mistakes.
// Test case 4: const int * const *
{
int *pd = &d;
const int *const *pp4 = (const int *const *)&pd;
Copy link

Copilot AI Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These casts form invalid/unsafe pointer type conversions in C (notably int **const int **), and can trigger compiler diagnostics (often fatal under -Werror) and/or undefined behavior. Instead, introduce correctly-typed intermediate variables (e.g., const int *) so you can take their addresses without casting.

Suggested change
const int *const *pp4 = (const int *const *)&pd;
const int *cpd = &d;
const int *const *pp4 = &cpd;

Copilot uses AI. Check for mistakes.
// Test case 5: const int ** const
{
int *pe = &e;
const int **const pp5 = (const int **)&pe;
Copy link

Copilot AI Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These casts form invalid/unsafe pointer type conversions in C (notably int **const int **), and can trigger compiler diagnostics (often fatal under -Werror) and/or undefined behavior. Instead, introduce correctly-typed intermediate variables (e.g., const int *) so you can take their addresses without casting.

Copilot uses AI. Check for mistakes.
Comment on lines +28 to +31
// - The const middle pointer level prevents havoc from reaching the data
// - x and y values are preserved
assert(x == 42); // preserved - const middle level blocks havoc
assert(y == 100); // preserved - const middle level blocks havoc
Copy link

Copilot AI Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

int * const makes the pointer itself non-assignable, but does not make the pointed-to int const. So “const middle pointer level prevents havoc from reaching the data” is not correct in C terms, and the post-havoc assertions are likely asserting an invalid guarantee. Either (a) adjust the type so the data is const (e.g., add const to the int level), or (b) update the expectations/comments to reflect that x/y may legally change.

Suggested change
// - The const middle pointer level prevents havoc from reaching the data
// - x and y values are preserved
assert(x == 42); // preserved - const middle level blocks havoc
assert(y == 100); // preserved - const middle level blocks havoc
// - The const middle pointer level prevents reassignment of the middle pointer
// - The int objects (x and y) may have been modified; their values are not guaranteed

Copilot uses AI. Check for mistakes.
{
int a;
int b;
int *ptr;
Copy link

Copilot AI Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

const struct test_struct * prevents modifying the struct’s members (including reassigning ptr), but it does not make the pointee of ptr const. Writing to *s->ptr is still legal C if the tool follows that pointer, so expecting x/*s.ptr to remain unchanged is not a valid consequence of “const struct”. To make the test’s intent sound, change the member to const int *ptr (or update the assertions to allow x to change).

Suggested change
int *ptr;
const int *ptr;

Copilot uses AI. Check for mistakes.
Comment on lines +23 to +30
// 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
Copy link

Copilot AI Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

const struct test_struct * prevents modifying the struct’s members (including reassigning ptr), but it does not make the pointee of ptr const. Writing to *s->ptr is still legal C if the tool follows that pointer, so expecting x/*s.ptr to remain unchanged is not a valid consequence of “const struct”. To make the test’s intent sound, change the member to const int *ptr (or update the assertions to allow x to change).

Copilot uses AI. Check for mistakes.
return 42;
}

void havoc_const_function_pointer(func_ptr_t *const func_ptr);
Copy link

Copilot AI Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The comment at line 19 contradicts the actual type: func_ptr_t *const makes the parameter pointer const, but allows modifying the func_ptr_t value it points to (i.e., fp). Updating the comment will prevent confusion about what is and isn’t protected by this qualifier placement.

Copilot uses AI. Check for mistakes.
Comment on lines +19 to +23
// The function pointer itself should not be modifiable
havoc_const_function_pointer(const_fp_ptr);

// Since the pointer to the function pointer is const (not the function
// pointer itself), the function pointer value may be modified by havoc
Copy link

Copilot AI Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The comment at line 19 contradicts the actual type: func_ptr_t *const makes the parameter pointer const, but allows modifying the func_ptr_t value it points to (i.e., fp). Updating the comment will prevent confusion about what is and isn’t protected by this qualifier placement.

Copilot uses AI. Check for mistakes.
…dling

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: diffblue#1948
@codecov
Copy link

codecov bot commented Mar 11, 2026

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.00%. Comparing base (b191cc1) to head (0d03748).

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #8797      +/-   ##
===========================================
- Coverage    80.01%   80.00%   -0.01%     
===========================================
  Files         1700     1700              
  Lines       188345   188345              
  Branches        73       73              
===========================================
- Hits        150696   150693       -3     
- Misses       37649    37652       +3     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Add additional regression tests for --replace-function-body

2 participants