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

Jump to bottom

Runtime Verification #1202

Draft
wants to merge 115 commits into
base: dev
Choose a base branch
from
Draft

Runtime Verification #1202

wants to merge 115 commits into from

Conversation

pieter-bos
Copy link
Member

Checklist:

  • The wiki is updated in accordance with the changes in this PR. For example: syntax changes, semantics changes, VerCors flags changes, etc.

PR description

Support for run-time checking of verification conditions, code from http://essay.utwente.nl/98745/ which is being adapted in this branch.

@ddjanssen
Initial setup runtime verification
acede73
@ddjanssen
Initial start on reconstructing constructors and removing unnecessary…
86dff78 
… generated code
@ddjanssen
Trying to use Java AST
0154bb7
@ddjanssen
Revert "Trying to use Java AST"
326b797 
This reverts commit 0154bb7.
@ddjanssen
Creating constructor works
7d3717f
@ddjanssen
Start on automated testing
f6b8954
@ddjanssen
Created CodeString declaration to insert code directly, without havin…
09d7dbc 
…g to create a very complicated ast for it
@ddjanssen
Created block structure to perform permission checks
82e8abb
@ddjanssen
clean up of CreateBlocksMethods.scala
4bea70b
@ddjanssen
clean up
ef0a747
@ddjanssen
clean up
1b18062
@ddjanssen
Created permission checks on blocks in methods
a6e008c
@ddjanssen
Updated desciption of block permissions
1bb38de
@ddjanssen
Add: Pre post condition permission checking
ce2378b
@ddjanssen
Start: creating array permission fields
7dc578e
@ddjanssen
Creating ideas on how to do the passes for the Transformation
e9eddd5
@ddjanssen
Fix bug: duplication error while origin is different
5b4f8e6 
Add: start on fork join template
@ddjanssen
Fix: found bug with method reference and refactored permissions block…
656526c 
…s method
@ddjanssen
Fix bug: objects dereferenced fields can now also be checked in blocks
60a2cc6
@ddjanssen
Fix bug: post conditions before return statements
d0ccabd
@ddjanssen
Fix permission checking blocks for if statements and loops
217e9fc
@ddjanssen
Fix bug post condition checking at all return statements
56299a1
@ddjanssen
Fix bug inner object references
6e9e821
@ddjanssen
Remove todo
1feb682
@ddjanssen
pc change
0f8befe
@ddjanssen
add test cases
a1caaab
@ddjanssen
Changed field permission to do both normal fields and arrays. Changed…
ce8c9bf 
… it so that it can create ledgers dynamically
@ddjanssen
PC change
671fb31
@ddjanssen
Pc change
3df2f7b
@ddjanssen
Add: finding bounds of a quantifier is now possible
fa2bb84 
Add: creating a quantifier method is now possible
Add: calling the quantifier method is now possible

TODO: implementation should be tested
ddjanssen and others added 25 commits February 7, 2024 09:12
@ddjanssen
Merge remote-tracking branch 'origin/1-create-template-for-runtime-ve…
33e3641 
…rification' into 1-create-template-for-runtime-verification

# Conflicts:
#	src/rewrite/vct/rewrite/runtime/CheckPermissionsBlocksMethod.scala
#	src/rewrite/vct/rewrite/runtime/util/ExprFinder.scala
@ddjanssen
FIX: small bugs that are occurring while executing the tests
5365dc3
@ddjanssen
FIX: new array dimensions
058932e
@ddjanssen
ADD: optional static to instanceMethod
5e63190
@ddjanssen
ADD: optional static to instanceMethod
aae5600
@ddjanssen
ADD: optional static to instanceMethod
c79a902
@ddjanssen
FIX: bug for library fraction
12616e4
@ddjanssen
FIX: bug naming for classes, procedure is now not taking the name any…
0ac2e35 
…more and is removed completely in the final step
@ddjanssen
FIX: offset in quantifiers condition
d7e53af
@ddjanssen
FIX: bug permission on other fields of object
fbd0f6a 
ADD: support for join tokens
ADD: Assert with expected
@ddjanssen
Change: predicates are now also in the ledger
3400ceb
@ddjanssen
Fix bug loop invariant
c752ea8
@ddjanssen
Fix final bugs
b64b25f
@ddjanssen
Fix final bugs
d7d9406
@ddjanssen
Fix final bugs
207b857
@ddjanssen
Fixed bugs and moved the GenerateJava to the codegeneration step to t…
4fb25be 
…ransform the program to an as close as possible executable file
@ddjanssen
Fix injectivitymap check for duplicates
717eba9
@ddjanssen
Update message with line numbers
24a1755
@ddjanssen
Fixed bugs (un)fold
a7bac02
@ddjanssen
Add comments to the code
a819229
@ddjanssen
Fixed tiny bug in code
822e74d
@ddjanssen
Loopinvariant only check on continue keyword and not return or break …
56fe703 
…keywords
@ddjanssen
Loopinvariant only check on continue or break keywords and not return…
5f3811f 
… keyword
@ddjanssen
Should only be continue, checked again, also at other languages
17bce44
@pieter-bos
Merge branch 'dev' into 1-create-template-for-runtime-verification
d138138
@pieter-bos pieter-bos mentioned this pull request May 21, 2024
Closed
1 task
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@51494306 51494306 51494306 approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@pieter-bos @51494306 @ddjanssen