Skip to content

Ensure variables are available in the scope when used

Viktor Kuncak requested to merge ensure_well_formed into master

Created by: mantognini

This catches error such as this one, but hopefully many more:

  case class B(var x: Int) {
    def foo(y: Int): Boolean = {
      x == y // just a dummy example
    } ensuring { res =>
      old(x) == x // instead of old(this).x == x
    }
  }

Of course, we need to give the user a proper error message, but that's the job of stainless. This patch ensures all transformations don't mess (too much) with variables.

BUT there's a catch...

The TIP parser doesn't extract commands such as (declare-const |error: Match is non-exhaustive!58| (_ BitVec 32)) into Let statement and the "variable" (Parser.Locals.vars) are not present in the Symbols, hence the tests are currently failing.

The question is, how do we workaround that? Should the TIP part be updated to use Let? (I've no idea how it works nor how much effort it would mean.) Should this kind of checks be disabled for some part of Inox? Should they be moved to stainless?

Merge request reports