issues
search
viperproject
/
silver
Definition of the Viper intermediate verification language.
Mozilla Public License 2.0
78
stars
40
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Support for chained comparisons
#713
marcoeilers
closed
1 year ago
4
Disable simplification of equalities
#712
marcoeilers
closed
1 year ago
0
Forbidding function self-references in postconditions for functions without decreases clauses
#711
marcoeilers
closed
1 year ago
0
Auto-including well-foundedness functions and axioms when they are used
#710
marcoeilers
closed
1 year ago
1
Adding join point computation
#709
marcoeilers
closed
1 year ago
0
Fixing let parsing
#708
marcoeilers
closed
1 year ago
0
Adding two new types of messages
#707
marcoeilers
closed
1 year ago
0
Missing hashCode definitions
#706
fpoli
opened
1 year ago
0
Resources can be used on left of implication in assumes
#705
totoyoyo
opened
1 year ago
0
Fixe scope (Seqn) handling in parser and pretty-printer
#704
marcoeilers
closed
1 year ago
0
Termination Plugin: Generates ill-formed Viper code for input with let expressions
#703
Felalolf
closed
1 year ago
2
Slightly better parse errors
#702
marcoeilers
closed
1 year ago
0
Fixing issue #474
#701
marcoeilers
closed
1 year ago
0
Adding consistency check to forbid wildcards in compound expressions
#700
marcoeilers
closed
1 year ago
0
Wildcard permission can be interpreted as greater than one
#699
rayman2000
closed
1 year ago
2
Allow calls of non-domain functions without preconditions from domain axioms
#698
marcoeilers
closed
1 year ago
0
Parser and pretty-printer do not preserve scopes
#697
marcoeilers
closed
1 year ago
1
Consistency check to forbid empty ADTs.
#696
marcoeilers
closed
1 year ago
0
Labelled old in triggers
#695
marcoeilers
closed
1 year ago
0
Add witness for silver issue 688
#694
jcp19
closed
1 year ago
0
Empty ADT causes "unsoundness"
#693
JonasAlaif
closed
1 year ago
1
Pretty-printing annotations
#692
marcoeilers
closed
1 year ago
0
Fix incorrect positions in imported files
#691
JonasAlaif
closed
1 year ago
0
Fix test triggers
#690
alexanderjsummers
closed
1 year ago
0
Decreases in method giving error: Verification aborted exceptionally
#689
BenjaminFrei
closed
1 year ago
4
Silicon not using variables assigned through let statements
#688
BenjaminFrei
closed
1 year ago
0
Trigger inference infers invalid triggers
#687
vakaras
opened
1 year ago
4
Autoformatting type checking code
#686
marcoeilers
closed
1 year ago
0
Improve language flexibility
#685
JonasAlaif
closed
1 year ago
15
Better type error reporting
#684
marcoeilers
closed
1 year ago
2
Update tests for Carbon exhale with well-definedness change
#683
gauravpartha
closed
1 year ago
0
The semantics of permission introspection in the body of unfolding expressions is unclear
#682
gauravpartha
opened
1 year ago
0
Two fixes for VerifyThis issues
#681
marcoeilers
closed
1 year ago
0
Re-disabling unstable test for Silicon
#680
marcoeilers
closed
1 year ago
0
Reenabling tests for some examples
#679
marcoeilers
closed
1 year ago
0
Updating tests
#678
marcoeilers
closed
1 year ago
0
Adapted test annotations to slightly improved trigger generation
#677
marcoeilers
closed
1 year ago
0
Adding a check to ensure that field assignment fields are actually fields
#676
marcoeilers
closed
1 year ago
0
Incorrect field assignments crash Viper
#675
marcoeilers
closed
1 year ago
0
More general string parsing, test for Silicon issue #707
#674
marcoeilers
closed
1 year ago
0
Bachelor Thesis: Advanced Logical Proofs in a Verifier
#673
dinanoe
closed
6 months ago
2
New message type for reporting failure per branch
#672
marcoeilers
closed
1 year ago
0
Delete test that has a matching loop
#671
marcoeilers
closed
1 year ago
1
Fixing some parser warnings
#670
marcoeilers
closed
1 year ago
0
Rejecting self-references in function postconditions
#669
marcoeilers
closed
1 year ago
2
Can ensure false as the post-condition of a function
#668
BenjaminFrei
closed
1 year ago
2
Support for special Z3 relations
#667
fpoli
opened
1 year ago
1
Annotations
#666
marcoeilers
closed
1 year ago
0
Small fixes
#665
JonasAlaif
closed
1 year ago
0
Added tests for recently fixed Silicon soundness issues
#664
marcoeilers
closed
1 year ago
0
Previous
Next