silver

silver copied to clipboard

While many sources of well-definedness can't happen in a domain axiom (no dependency on state, no calling functions with preconditions), potential division by zero can and should be checked for.

alexanderjsummers

Is it possible to apply a perm expression on a parameter of a macro? The following doesn't parse: ``` define check(expr) { assert perm(expr) < write } ``` Error message:...

fpoli

The following program, generated by a fuzzer starting from Silver's test suite, makes Silicon crash. There are some weird characters in it, like "\ufffd\ufffd\ufffd". Error: ``` Silicon 1.1-SNAPSHOT Verification aborted...

fpoli

The following program fails to verify in Silicon and Carbon, but by uncommenting the first assert statement everything goes through. The incompleteness is essentially by design, as explained by @mschwerhoff...

fpoli

SilFrontend generates AST nodes with incorrect positions. In particular, the start position of methods is wrong (seems to be the same as their end position for some reason). This is...

aterga

The following code is causing issues in the correct line: ``` define A() false define B() A() method test() { assert B() // Issue in this line, not in the...

fabiopakk

Feature request: real numbers

5

For VerCors, I am working on implementing verification of programs that use floating point numbers (for my master thesis). The way that I plan on implementing the support for floating...

martijnrenssen

Invariants on labels should be disallowed unless they form loop heads and while loops that are not loop heads should be rejected

7

> Created by **@alexanderjsummers** on 2019-10-30 08:47 Because of how loops are verified, the current meaning of an “invariant” on a label varies significantly depending on whether the label represents...

viper-admin

At the moment, Magic Wands are not entirely supported in function preconditions and in predicates. As discussed on several issues (viperproject/carbon#364, #456, viperproject/carbon#244), it was decided to disable support for...

fabiopakk

```plain import function foo1(n: Int): Int decreases n { 0 < n ? foo1(n) : 123 } // n does not decrease (but is bounded) function foo2(n: Int): Int decreases...

mschwerhoff