Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Modify loop unwinding and general cleanup in Makefile.common #110

Conversation

markrtuttle
Copy link
Contributor

This pull request removes conditional invocations of goto-instrument. The command goto-instrument is idempotent when called with no flags (it just copies the file), so checking whether a flag is set before calling goto-instrument is unnecessary and complicates the makefile.common.

This pull request also modifies when loop unwinding is done. It moves all loop unwinding of loops specified by UNWINDSET back to the invocations of cbmc (no more early invocation of goto-instrument to do it), but it does introduce a new EARLY_UNWINDSET to support selective loop unwinding for the purpose of function and loop contract checking.

This pull request also cleans up some comments in makefile.common and advances the release to 2.2.

These changes have been checked against all starter kit proofs in github. The differences found were

  • removal of most (but not all) of the 'unknown loop identifier' warnings that resulted from giving loop unwinding instructions to both goto-instrument and cbmc
  • removal of a 'conflicting initializers' warning in derive_data_key
  • off-by-one differences in coverage reports due to the fact that a do statement is no longer considered by cbmc to be contributing goto instructions
  • many instances of a line considered "both" hit and missed are now considered just "hit" (unrolling causes a single line of code to contribute to many basic blocks, some unreachable if the loop is unwound an extra iteration by goto-instrument)

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@markrtuttle markrtuttle changed the title Modernize makefile common+unwindset Modify loop unwinding and general cleanup in Makefile.common May 6, 2022
@nwetzler nwetzler self-requested a review May 9, 2022 13:45
@markrtuttle
Copy link
Contributor Author

This should close issue #88

@markrtuttle markrtuttle merged commit 43c1ddd into model-checking:master May 9, 2022
@markrtuttle markrtuttle deleted the modernize-makefile-common+unwindset branch May 9, 2022 17:36
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.

4 participants