Error transformer not working with Silicon

[dewert99]

I was working on a plugin for a school project (which I've now submitted). I tried using an error transformer with VSCode, but when I tested it the errors appeared transformed when using Carbon but not when using Silicon. If I switched from Carbon to Silicon then Silicon would work (maybe to do with caching). The code for the plugin is part of a fork of Silver https://github.com/dewert99/silver/tree/pred-inline An example viper program that shows this issue when using the plugin is:

field x: Int

inline predicate test(r: Ref) {acc(r.x) && r.x > 0}

method foo(r: Ref)
{
  assert unfolding test(r) in r.x > 0
}

which my plugin expands to

domain __SECOND__[T] {
  
  function __second__(b: Bool, t: T): T
  
  axiom {
    (forall b: Bool, t: T :: { (__second__(b, t): T) } (__second__(b, t): T) == t)
  }
}

field x: Int

function __unfolding_test__(r: Ref, __perm__: Perm): Bool
  requires __perm__ >= none && (__perm__ > none ==> acc(r.x, write * __perm__) && r.x > 0)
{
  true
}

method foo(r: Ref)
{
  assert (__second__(__unfolding_test__(r, write), r.x > 0): Bool)
}

On Silicon this gives: Precondition of function __unfolding_test__ might not hold. There might be insufficient permission to access r.x ([email protected])

On Carbon this gives: Assert might fail. There might be insufficient permission to access test(r) ([email protected]) Assert might fail. There might be insufficient permission to access r.x ([email protected])

Switching back to Silicon gives: Assert might fail. There might be insufficient permission to access test(r) ([email protected])

[mschwerhoff]

@ArquintL Could this be an IDE issue? It seems that the temporary switch to Carbon produces a cache entry that is then picked up by Silicon, resulting in the changed error message between first and second run of Silicon.