-
Notifications
You must be signed in to change notification settings - Fork 5
Issues: gradual-verification/gvc0
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.
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Question about the testcase in the c0 file for Daisy's first example in the paper
#65
opened Jun 17, 2024 by
fanweneddie
Verification error when verifying the fully-specified example program
#64
opened Jun 17, 2024 by
fanweneddie
Lemmas functions should become a specification construct + be removed from programs when completely statically verified
enhancement
New feature or request
question
Further information is requested
#63
opened Jun 9, 2024 by
jennalwise
Verification error when verifying fully specified correct program
#62
opened May 22, 2024 by
cliu369
Benchmarker producing wrong .verified files after generating correct source code permutations due to oddly constructed IRs
enhancement
New feature or request
#59
opened Nov 15, 2023 by
jennalwise
Need to catch logical conditionals with impure conditions in frontend and produce error message
bug
Something isn't working
enhancement
New feature or request
#57
opened Sep 28, 2023 by
jennalwise
Run-time checks with char comparison should use char val not int val
bug
Something isn't working
#56
opened Sep 26, 2023 by
jennalwise
Permutation generator does not support treating missing
requires and ensures specifications as true
#53
opened Aug 1, 2023 by
icmccorm
Verifier is unsound for bad specs involving method calls with equi-imprecise preconditions; discussion in Conrad's paper
enhancement
New feature or request
#52
opened Jul 28, 2023 by
jennalwise
Recursive predicates should fail due to separation rather than infinite recursion if separation failure applies
enhancement
New feature or request
#49
opened Apr 21, 2023 by
jennalwise
line numbers for static errors
enhancement
New feature or request
#48
opened Apr 18, 2023 by
JonathanAldrich
"Invalid specification" is an overly general & unhelpful error message
#46
opened Apr 11, 2023 by
JonathanAldrich
Unfolding avlh(node, h) might fail. Fraction write might be negative.
bug
Something isn't working
#44
opened Jan 19, 2023 by
icmccorm
Unexpected output from Z3 when verifying list.c0
bug
Something isn't working
#43
opened Jan 18, 2023 by
icmccorm
Significant slow-downs compared to fully dynamic approach at run time for static/more precise specs
enhancement
New feature or request
#37
opened Jun 30, 2022 by
jennalwise
explain which path leads to a postcondition that doesn't hold
enhancement
New feature or request
#36
opened May 26, 2022 by
JonathanAldrich
list_loop_exec.c0 under the bugs folder is failing an assert at run time
bug
Something isn't working
#34
opened May 24, 2022 by
jennalwise
gradual viper backend seems to conflate predicates that are very similar
enhancement
New feature or request
#33
opened May 21, 2022 by
JonathanAldrich
Code with returns inside conditionals, with code following, doesn't verify properly
enhancement
New feature or request
#32
opened May 21, 2022 by
JonathanAldrich
dynamic gradual guarantee broken at a conditional
enhancement
New feature or request
#31
opened May 21, 2022 by
JonathanAldrich
Conditionals in expressions (not formulas) should be translated to if statements in Gradual Viper
bug
Something isn't working
enhancement
New feature or request
good first issue
Good for newcomers
#29
opened May 20, 2022 by
jennalwise
Test file IO should use Source.getResource("...") rather than Source.getFile("...")
enhancement
New feature or request
#7
opened Oct 1, 2021 by
jennalwise
Previous Next
ProTip!
Type g p on any issue or pull request to go back to the pull request listing page.