gradual-verification gvc0 issues

gradual-verification / gvc0

Gradually Verified C0

6 stars 5 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Properly scope dynamic loop permissions

#66 conradz closed 1 month ago
0
Question about the testcase in the c0 file for Daisy's first example in the paper

#65 fanweneddie opened 3 months ago
0
Verification error when verifying the fully-specified example program

#64 fanweneddie opened 3 months ago
1
Lemmas functions should become a specification construct + be removed from programs when completely statically verified

#63 jennalwise opened 3 months ago
0
Verification error when verifying fully specified correct program

#62 cliu369 opened 4 months ago
3
Allow multiple files in `DefaultMode`

#61 samestep opened 10 months ago
0
Allow multiple `--recreate` permutations at once

#60 samestep closed 10 months ago
0
Benchmarker producing wrong .verified files after generating correct source code permutations due to oddly constructed IRs

#59 jennalwise opened 10 months ago
3
Baseline verifiers producing the wrong count for numFields during benchmarking

#58 jennalwise closed 10 months ago
1
Need to catch logical conditionals with impure conditions in frontend and produce error message

#57 jennalwise opened 1 year ago
1
Run-time checks with char comparison should use char val not int val

#56 jennalwise opened 1 year ago
0
gvc0 should default missing specs to ? not 'true'

#55 jennalwise closed 1 year ago
1
Weaver fails when multiple accessibility predicates for a return value must be run-time checked

#54 jennalwise closed 1 year ago
2
Permutation generator does not support treating missing `requires` and `ensures` specifications as `true`

#53 icmccorm opened 1 year ago
0
Verifier is unsound for bad specs involving method calls with equi-imprecise preconditions; discussion in Conrad's paper

#52 jennalwise opened 1 year ago
2
Finish part of import and comment in the pyteal parser

#51 JudySun233 closed 1 year ago
0
add verified gvc0 codes for minimum priority queue and stack

#50 JudySun233 closed 1 year ago
0
Recursive predicates should fail due to separation rather than infinite recursion if separation failure applies

#49 jennalwise opened 1 year ago
1
line numbers for static errors

#48 JonathanAldrich opened 1 year ago
0
Invalid acc() argument exception

#47 JonathanAldrich opened 1 year ago
0
"Invalid specification" is an overly general & unhelpful error message

#46 JonathanAldrich opened 1 year ago
0
stack verification performed

#45 kunalsingh3110 opened 1 year ago
0
Unfolding avlh(node, h) might fail. Fraction write might be negative.

#44 icmccorm opened 1 year ago
0
Unexpected output from Z3 when verifying list.c0

#43 icmccorm opened 1 year ago
2
Update branch

#42 janpaulpl closed 1 year ago
0
Method not marked as containing imprecision when it has an imprecise pre or postcondition

#41 jennalwise closed 2 years ago
1
simple fix for issue 38

#40 jennalwise closed 2 years ago
0
Run-time check with a condition injected prior to the corresponding condition variable being defined in AVL

#39 jennalwise closed 2 years ago
2
Run-time checks from backend for before loops are being put after the loop

#38 jennalwise closed 2 years ago
1
Significant slow-downs compared to fully dynamic approach at run time for static/more precise specs

#37 jennalwise opened 2 years ago
5
explain which path leads to a postcondition that doesn't hold

#36 JonathanAldrich opened 2 years ago
0
gvc0 generates permission-manipulating code based on expressions over mutable data rather than stored variables

#35 JonathanAldrich opened 2 years ago
1
list_loop_exec.c0 under the bugs folder is failing an assert at run time

#34 jennalwise opened 2 years ago
3
gradual viper backend seems to conflate predicates that are very similar

#33 JonathanAldrich opened 2 years ago
2
Code with returns inside conditionals, with code following, doesn't verify properly

#32 JonathanAldrich opened 2 years ago
1
dynamic gradual guarantee broken at a conditional

#31 JonathanAldrich opened 2 years ago
1
dynamic gradual guarantee broken for permissions

#30 JonathanAldrich opened 2 years ago
0
Conditionals in expressions (not formulas) should be translated to if statements in Gradual Viper

#29 jennalwise opened 2 years ago
0
Variables in specifications aren't correctly renamed when building the AST.

#28 icmccorm closed 2 years ago
1
Owned fields passing at method calls treats pre and postconditions as precise when they have hidden imprecision

#27 jennalwise closed 2 years ago
0
Partial specs #145-151 of BST failing at runtime with missing permission.

#26 icmccorm closed 2 years ago
0
Permissions not being reinitialized before call to imprecise method in precise context (BST)

#25 icmccorm closed 2 years ago
0
BST - Failing series of partial specs when removing imprecision

#24 icmccorm closed 2 years ago
0
Runtime-check fails when removing imprecision and adding fold to the specification.

#23 icmccorm closed 2 years ago
0
Translate2.c0 failing to compile in cc0 for run-time execution

#22 jennalwise closed 2 years ago
6
Creating ViperBranch for CheckPosition at loop with no invariant

#21 icmccorm closed 2 years ago
0
Simplifying runtime check conditions results in an infinite loop

#20 icmccorm closed 2 years ago
1
ViperBranch in Collector missing cases for folds/unfolds

#19 jennalwise closed 2 years ago
0
Match Error ? && true

#18 jennalwise closed 2 years ago
0
Condition Versioning: Condition Versioned out of Place

#17 jennalwise closed 2 years ago
1