silver
silver copied to clipboard
viperproject
Definition of the Viper intermediate verification language.
closes #660 Same as #660, but the changes have been squashed into a single commit
By profiling for 165 seconds a Carbon run with VisualVM I found that: * The time spent in the JVM is 53s, which is 32% of the wall-clock time. *...
The AST of a program containing a top-level function with a quote (`'`) in its name passes the consistency checks. However, the dump of the program is rejected by the...
Both backends currently use techniques to record resources that are folded into predicates. Carbon uses a knownfolded permission approach (based on an extension of [1]) and Silicon uses a predicate...
Viper disallows putting resource assertions in the body of an `unfolding`: ``` field f: Int predicate p(x: Ref) { acc(x.f, 1/4) } method test(x: Ref) requires p(x) requires unfolding p(x)...
Currently, the simplifier converts an expression `s[1] == s[1]` to `true`; however, the original expression may not be well-defined (and Silicon / Carbon would raise an exception accordingly). This PR...
```silver import adt List[T] { Nil() Cons(value: T, tail: List[T]) } derives { contains } method client() { var x: List[Int] := Cons(42, Cons(33, Nil())) assert contains(42, x) // passes,...
The new ADT plugin did not handle `result` expressions in post-conditions yet properly. This PR is a patch to fix a couple of corner cases with additional regression tests.
Hello! I found my way here through doing some research for Prusti and I noticed the ADT plugin got merged very recently :) This looks like a really great feature,...
What is the best way for a plugin to override mapVerificationResult? I noticed that the termination and predicate instance plugins each apply the error-transformers to all errors of a specific...
Metadata
Owner
Metadata
Definition of the Viper intermediate verification language.