search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

Parsing Dereference Operator #99

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

Currently, the parse fails to parse the following assertion:

assert:
    forall(&int x):
        if:
            (*x) == 0
        then:
            (*x) == 0

Observe, however, that the corresponding AST node Expr.Dereference already exists.