Issues
- 1
- 0
The semantics of permission introspection in the body of unfolding expressions is unclear
#682 opened by gauravpartha - 0
Perm under inhale-exhale expression handled differently by Silicon vs. Carbon
#808 opened by mschwerhoff - 1
Issue with variable renaming in macro expansion
#803 opened by marcoeilers - 4
Precondition reason
#798 opened by pieter-bos - 0
- 1
Syntax crash when defining a statement macro inside another statement macro
#786 opened by Bibin112358 - 2
Wrong optimization of signed integer divisions
#782 opened by fpoli - 1
goto name is replaced while label is not
#787 opened by Bibin112358 - 0
Variable scope with nested scopes
#789 opened by Aurel300 - 0
- 2
- 1
- 0
ADT Plugin should auto-generate well-foundedness axioms for the generated types
#739 opened by marcoeilers - 0
Silver sometimes auto-generates triggers that cannot be used by Silicon because of missing old-wrappers
#740 opened by marcoeilers - 0
Type of some division expressions is ambiguous and the default interpretation is bad
#745 opened by marcoeilers - 0
Feature request: Add more default types (and use them in examples and tutorials)
#741 opened by marcoeilers - 0
- 1
Is it intentional that adt exclusivity is not enforced?
#725 opened by glor - 0
Generic domain function application needs trivial type variable map with uninsightful error message
#733 opened by nilscrm - 0
No non-pure check for predicate access arguments
#720 opened by vfukala - 1
- 2
Termination Plugin: Generates ill-formed Viper code for input with let expressions
#703 opened by Felalolf - 1
Parser and pretty-printer do not preserve scopes
#697 opened by marcoeilers - 0
Missing hashCode definitions
#706 opened by fpoli - 0
- 2
- 1
Empty ADT causes "unsoundness"
#693 opened by JonasAlaif - 0
- 4
- 2
- 4
Trigger inference infers invalid triggers
#687 opened by vakaras - 0
Better type errors
#642 opened by fpoli - 0
Incorrect field assignments crash Viper
#675 opened by marcoeilers - 1
Support for special Z3 relations
#667 opened by fpoli - 2
- 0
Slow pretty-printer and consistency checks
#661 opened by fpoli - 3
Avoid linear scans in Program.find* methods
#657 opened by fpoli - 0
Missing consistency check for function identifiers
#651 opened by fpoli - 1
- 1
let inlining bug
#639 opened by pieter-bos - 1
undeclLocalVars does not consider Let expressions
#610 opened by Felalolf - 1
[Plugins] Streaming of Verification Results
#634 opened by ArquintL - 2
- 2
- 0
Discrepancy between Carbon knownfolded permissions and Silicon predicate snapshots
#624 opened by gauravpartha - 3
`let` in quantified permission
#620 opened by pieter-bos - 2
- 2
`unfolding` body does not admit resources
#606 opened by pieter-bos - 0
ADT plugin `contains` cannot prove lack of value
#596 opened by Aurel300