search

gradual-verification / gvc0

Gradually Verified C0
6 stars 5 forks source link

Crash on any conditional in postcondition #12

Closed conradz closed 2 years ago

conradz commented 2 years ago

Silicon seems to crash every time a conditional is added in a postcondition.

Minimal example:

int main()
//@ ensures true ? true : true;
{
  return 0;
}

This prints the following error:

[info] Verification aborted exceptionally: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: scala.MatchError: (true ? true : true) (of class viper.silver.ast.CondExp)
[info]   Cause: java.util.concurrent.ExecutionException: scala.MatchError: (true ? true : true) (of class viper.silver.ast.CondExp)

@hemantgouni @jennalwise this seems caused by a bug in the verifier. It is making implementation of conditional checks quite difficult.

jennalwise commented 2 years ago

Sorry, I have known about this issue for a while. It was supposed to be a fixed a long time ago, but I think it got overlooked. It should be fixed in this recent commit: https://github.com/gradual-verification/silicon-gv/commit/c5f07a83e62cc345e3089b02328255d5eacbd588. Pretty much we didn't have a case to deal with pure if conditionals in a consume. I added it back in.

conradz commented 2 years ago

Yes, this is fixed by that commit; I just hadn't pulled it. Thank you!