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.

Sign up for GitHub

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

Update README with version numbers #5

Merged
merged 1 commit into from
May 14, 2024
Merged

Update README with version numbers #5

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 8 additions & 6 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,11 @@
This program is licensed under the GPL2 license, see license headers in source code files
and the full license in the LICENSE file.

ACSL Contract inference for helper functions.
Developed for Frama-C v23.1 but also seems to work for Frama-C versions <= 28.1.
Please note that the plugin is experimental and still under development so that no results are guaranteed.
This is a plugin for Frama-C. Given ab entry-point function with an ACSL contract, it infers
ACSL contracts for helper functions, i.e. functions further down the call tree. It was
originally developed for Frama-C v23.1 but has been tested with Frama-C versions <= 28.1.
Please note that the plugin is experimental and still under development so that no results
are guaranteed.


## Install TriCera
Expand Down Expand Up @@ -52,9 +54,9 @@ The plugin is currently limited to programs/specifications following these rules
Aside from the limitations listed above, many more limitations/bugs expected to exist.

## *Summary*
The execution of the plugin can be summarized as:
The execution of the plugin can be summarized as:
Step 1: convert the top-level contract to a TriCera harness function
Step 2: Merge the harness function with the source code
Step 2: Merge the harness function with the source code (this result is stored in `tmp_harness_source_merged.c`)
Step 3: Run tricera on the result from step 2
Step 4: Merge the inferred contracts from step 3 with the source code
Step 4: Merge the inferred contracts from step 3 with the source code (this result is stored in `tmp_inferred_source_merged.c`)
Step 5: (optional) Run the wp plugin on the result from step 4