team-worthwhile/worthwhile — Issue #92: Debugger should only show "worst" validity on statement
Author: jspam
Created: 2012-02-22 15:29:36+00:00
State: open
Labels: debugger

Take the following program:

```
function Integer noop(Integer a)
/* troll */ _ensures _return = a
_ensures _return = a // troll comment
_ensures _return = a
// _troll comment
{
if (a ≥ 0) {
return a
} else {
return 0
}
}

Integer test := noop(42)
Integer test2 := noop(-42)
```

Like the prover, the debugger should mark a statement as green only if it was `VALID` all times, else red.