Fractional permissions #247
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
added 11 commits
April 24, 2023 14:22
Note: This adds the new load and store memory actions to the symbolic memory model
Signed-off-by: Sacha Ayoun <[email protected]>
…atform/Gillian into fractional_permissions
Now all examples in debugger-vscode-extension/sampleWorkspace verify as they should
giltho
reviewed
May 15, 2023
Comment on lines
+1
to
+3
| ; (executables | ||
| ; (names cwisl wislverify) | ||
| ; (libraries camelot wisl)) |
There was a problem hiding this comment.
Hahahahahahaha, how is this still in here?
I'll remove it from master directly
There was a problem hiding this comment.
(this is obviously not you, this is some bit of 4+-year-old code that should go away)
* Add parallel composition construct skeleton and parsing attempts
* Add function call rule to Gil grammar
* Cmd (...) -> Cmd function_call, and function_call = { ... }
Signed-off-by: Sacha Ayoun <[email protected]>
* added printer at the end of action
* Add parallel composition implementation and a small example program
* Fix unconditional execution bug
* Implement the parallel composition run spec correctly
* Add unification flags
* allocation allocates abstract location
* Add configurable conditions to the AST nodes
* Implemented floating point arithmetics and permission parsing
This also fixes bugs related to passing the in instead of the out permission from get to remcell and the merging of heaps
* Fix parser bugs for floats
* Add support for lab_spec_target to WISL
* Add test programs for more complicated concurrency
* reductions and correct code
* there we go
* Add more complicated concurrent binary tree tests
* Add lambda term substitution tests and fix <=#. bug
* Remove incorrect optimisations in reduction engine
* Update tests
* Fix overwrite_cell bug when storing
* Edit a comment
---------
Signed-off-by: Sacha Ayoun <[email protected]>
Co-authored-by: Tiberiu Bucur <[email protected]>
Co-authored-by: Sacha Ayoun <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
|
Converting to a draft as some work is needed to catch up with upstream changes |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Everything working nicely! :D