Loop Invariant Encoding #78
Open
Conversation
This file contains hidden or 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
Owner
|
Could you add some tests? |
paaassscccaaalll
force-pushed
the
loop_invariant_encoding
branch
from
21d338b to
4c11fa0
Compare
JonasAlaif
force-pushed
the
loop_invariant_encoding
branch
from
1143378 to
adac2c0
Compare
print for which function is currently encoded deleted pcs deleted utils and put helper function into change is_ad_trusted() to is_type_trusted() which now take in a ty:TY formating fix PR 68 (over to desktop) trying to add support for T/# trying to fix partial ord while loop fix panic in make.rs changed closure as loop invariant detection over to desktop added encoding of lool invariant closure which is than added to the invariants (permission issue persists) added invariant acc for every loop invariant fixed bug where in forall annotations the make_concrete and s_Ref_immutable was applied twice some leftovers revert tried fix added axiom for closure bugfix for handeling of refrences in forall added axiom for immref continue in fn_wand region pairs style fix style fix axiom immref stuff now it correctly encodes the loop invariant directly removed debug output for loop invariant new axiom for immref new axiom for immref with r further refinement (before nested loop fix) works but what if some label is used twice in the mir over to laptop removed artifact added used local check for not adding access to unused variables added panic to detect reuse of identifiers made collection of loop invariants more efficient used visitor to detect used locals and added assert such that body_invariants are catched pcg diff removed removed diff removed diff 2 remove diff 3 updated pcg style fix make it work with new version skip invariant closures
renamed LoopSpecification enum for bodyinvariant! from Invariant to BodyInvariant
JonasAlaif
force-pushed
the
loop_invariant_encoding
branch
from
adac2c0 to
81af147
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
loop.rsloop_invariant!macro which follows the actual definition of an invariant (is also true at start and end of the loop).