Skip to content

Conversation

@carolynzech
Copy link
Contributor

The important changes are:

  • 37db951, which will allow autoharness to eventually work with modifies clauses. Since we don't generate autoharnesses for functions that take pointers as arguments anyway, this doesn't affect current functionality.
  • a325fd8, which ensures that the --function passed to CBMC is the mangled name of the automatic harness intrinsic, not the target function

Towards #3832

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@carolynzech carolynzech requested a review from tautschnig April 14, 2025 19:50
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Apr 14, 2025
@carolynzech carolynzech changed the title Autoharness Bug Fixes Autoharness: Harness Generation Improvements Apr 14, 2025
@carolynzech carolynzech marked this pull request as ready for review April 14, 2025 19:58
@carolynzech carolynzech requested a review from a team as a code owner April 14, 2025 19:58
@carolynzech carolynzech enabled auto-merge April 14, 2025 22:11
@carolynzech carolynzech added this pull request to the merge queue Apr 14, 2025
Merged via the queue into model-checking:main with commit 2a528a5 Apr 15, 2025
25 of 26 checks passed
@carolynzech carolynzech deleted the autoharness-contract-harnesses branch April 15, 2025 00:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants