You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
}
On Silicon this gives: Precondition of function __unfolding_test__ might not hold. There might be insufficient permission to access r.x (test.vpr@7.19--8.1)
On Carbon this gives: Assert might fail. There might be insufficient permission to access test(r) (test.vpr@7.9--7.10) Assert might fail. There might be insufficient permission to access r.x (test.vpr@7.9--7.10)
Switching back to Silicon gives: Assert might fail. There might be insufficient permission to access test(r) (test.vpr@7.9--7.10)
The text was updated successfully, but these errors were encountered:
@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.
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:
which my plugin expands to
On Silicon this gives:
Precondition of function __unfolding_test__ might not hold. There might be insufficient permission to access r.x (test.vpr@7.19--8.1)
On Carbon this gives:
Assert might fail. There might be insufficient permission to access test(r) (test.vpr@7.9--7.10)
Assert might fail. There might be insufficient permission to access r.x (test.vpr@7.9--7.10)
Switching back to Silicon gives:
Assert might fail. There might be insufficient permission to access test(r) (test.vpr@7.9--7.10)
The text was updated successfully, but these errors were encountered: