Open viper-admin opened 3 years ago
Here is a client that shows the transformation:
import viper.silver.{ast => vpr}
import viper.silicon.Silicon
import viper.silver.reporter.NoopReporter
import viper.silver.verifier.{Failure, Success}
import viper.silver.verifier.{AbstractVerificationError, errors => vprerr, reasons => vprrea}
val v = vpr.LocalVarDecl("x", vpr.Int)()
val b = vpr.EqCmp(vpr.Div(v.localVar, vpr.IntLit(0)())(), vpr.IntLit(42)())()
val p = vpr.Program(
Seq.empty,
Seq.empty,
Seq.empty,
Seq.empty,
Seq(vpr.Method(
"foo",
Seq(v),
Seq.empty,
Seq.empty,
Seq.empty,
Some(vpr.Seqn(Seq(vpr.If(b, vpr.Seqn(Seq.empty, Seq.empty)(), vpr.Seqn(Seq.empty, Seq.empty)())()), Seq.empty)())
)()),
Seq.empty,
)()
val silicon = Silicon.fromPartialCommandLineArguments(Seq.empty, NoopReporter)
silicon.start()
val res = silicon.verify(p)
silicon.stop()
res match {
case Failure(Seq(vprerr.IfFailed(offendingNode, _, _))) =>
print("1: "); println(offendingNode == b) // false
print("2: "); println(offendingNode == vpr.Not(vpr.EqCmp(vpr.Div(v.localVar, vpr.IntLit(0)())(), vpr.IntLit(42)())())()) // true
println(offendingNode)
}
The underlying issue in Viper should be fixed (https://github.com/viperproject/silver/pull/649).
The error back-translation implementation contains a workaround for what I think might be a problem in Silver and/or Silicon. See (not sure how to better link to files/lines in particular commits in Bitbucket):
https://bitbucket.org/Felale/gobra-one/src/e7e58d00b4e831073ac3e495577e8074649d9ac4/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala#lines-121
The reason for this workaround is a bit technical. It appears that Viper internally sometimes negates conditions of if-statements, or generates extra if-statements for user-written if-statements but with the original conditions negated. However, these negations don't seem to preserve any source information, which could lead to stack traces in Gobra. Those particular scenarios are prevented by this workaround, but we eventually want a nicer solution.