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

Updated limitations. #8

Merged
merged 1 commit into from
Jun 26, 2024
Merged

Updated limitations. #8

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
7 changes: 6 additions & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,12 @@ The plugin is currently limited to programs/specifications following these rules
* Any non-main function should _not_ contain a contract.
I.e., only 1 contract allowed in the file.
* The non-main functions has to be called somewhere from within the file
* Currently does not work for arrays or floats.
* Currently does not support arrays, floating points, or stack pointers.
* Heap pointers are generally supported (but bugs exist in some cases in the translation to ACSL).
* Does not support inference of contracts for functions with local static variables.
* In the ACSL contract, only ensures and requires clauses over C expressions are support, with the exception of certain uses of quantification: universal quantification is supported in the post-conditions, and existential quantification in the pre-condition.
Other types of ACSL built-in or user defined constructs, such as logical functions and predicates, are not supported.


Aside from the limitations listed above, many more limitations/bugs expected to exist.

Expand Down
Loading