Remy Willems

### Description - Make all by block proofs penetrate the entire LHS ### How has this been tested? - Updated tests for call statements and the three types of assignment...

### Description - Remove usage of opaque from standard library ### How has this been tested? - Standard library is verified by CI By submitting this pull request, I confirm...

Prototype for adding a front-end for an extension of Java that supports verification. ### Description - The file `JavaGrammar.cs` contains the currently partial definition of the extended Java. - The...

Wrap requires and ensures clauses in Boogie functions, to prevent duplication of expressions when desugaring Boogie call statements. Duplicating Boogie expression causes extra SMT to be generated which is bad...

I'm pausing this until we further clean up the Boogie encoding, so performance issues with this PR will be easier to debug. One issue I ran into with `BinaryTree.dfy` is...

Suppose we have the following program ```dafny method test(element:int, a:array) requires a.Length > 2 modifies a; { a[0] := element; } method Main() { var a : array; var element...

Prototype for adding a front-end for an extension of Java that supports verification. The file `JavaGrammar.cs` contains the currently partial definition of the extended Java. The new project `CompilerBuilder` contains...

Add regression tests for all signatures created by code generators

2

We should add regression tests that compare the output of `dafny translate` to a fixed expectation output. However, to allow implementation details, such as method bodies, to change, we should...

Resolver crash Program: ``` trait Computation { function run(): T } class Stop extends Computation { var value: T; constructor(value: T) { this.value := value; } function run(): T {...

Enable compiling Dafny programs with deeply nested code

1

Programs with deeply nested Dafny code will crash the Dafny compiler. Here's an example: ``` method Main() { var c := 1; print(c + c + c + c +...