alexanderjsummers

Slightly-too-long lifetime for Loan inferred

1

In the following code, it doesn't seem correct that the first Loan struct computed includes the line `START/6` - it seems that that value of `list` is dead by that...

New failure on small linked list example

4

The following example previously worked on a Prusti install I have here, but after running "Prusti: update dependencies" I get a failure for the postcondition on `push`: ``` #![feature(box_patterns, box_syntax)]...

Trying to clarify a few parts I found initially less clear (some of them became clear later in the document anyway).

Unsoundness of old expressions in magic wands in postconditions

5

It seems that an "old" expression in a magic wand (RHS) in the postcondition of the called method is wrongly interpreted as referring to the old state of the caller...

Using quantified permissions on the left of a wand seems OK, but on the RHS I get a stack trace. For example, for the program: ``` field val : Int...

Unsoundness of old expressions in magic wands in postconditions

2

It seems that an "old" expression in a magic wand (RHS) in the postcondition of the called method is wrongly interpreted as referring to the old state of the caller...

The same applies with e.g. quantified predicate instances (and e.g. with a reasonable conditional as opposed to literally quantifying over all Refs): ``` field f: Ref method foo() { package...

We need a design for the "snapshots" of such magic wands in Carbon. In the short-term, we should make sure a better error message is raised (unsupported feature).

Change error type used for division by zero in assert statements

1

It seems surprising that the following code generates a `assert.failed:division.by.zero` error rather than `not.wellformed:division.by.zero`: ``` method foo() { //:: ExpectedOutput(not.wellformed:division.by.zero) assert 42 / 0 == 1 } ```