Viper command line not giving termination error
BenjaminFrei opened this issue · 2 comments
BenjaminFrei commented
While trying to verify the Viper code with the command line, an error occurs in the newest version. In older version the code verifies, for example in the silicon commit 3b3b4be the code verifies. This does also not work with the new carbon version.
code:
import <decreases/all.vpr>
domain ListWellFoundedOrder[T] {
axiom {
forall y : List[T] :: {bounded(y)} bounded(y)
}
axiom {
forall xs : List[T] , y : T ::
decreasing(xs, Cons(y, xs))
}
axiom {
forall xs : List[T], ys : List[T], zs : List[T] :: {decreasing(xs, ys), decreasing(ys, zs)}
decreasing(xs, ys) && decreasing(ys, zs) ==> decreasing(xs, zs)
}
}
adt List[T] {
Nil()
Cons(value : T, tail : List[T])
}
Output:
with the newest version of silicon, it gives this error message:
$ java -jar /home/benjamin_frei/Desktop/ETH/Bachelor_Thesis/silicon/target/scala-2.13/silicon.jar --z3Exe /usr/bin/z3 /home/benjamin_frei/Desktop/ETH/Bachelor_Thesis/Viper_examples/BachelorThesis/Book_Part1/ch6/chapter6viperhelp.vpr
Silicon 1.1-SNAPSHOT (8e3190bc)
Verification aborted exceptionally: scala.MatchError: List[T] (of class viper.silver.plugin.standard.adt.PAdtType)
scala.MatchError: List[T] (of class viper.silver.plugin.standard.adt.PAdtType)
at viper.silver.plugin.standard.termination.TerminationPlugin.viper$silver$plugin$standard$termination$TerminationPlugin$$isNotExpectedConstrainedType$1(TerminationPlugin.scala:134)
at viper.silver.plugin.standard.termination.TerminationPlugin$$anonfun$constrainsWellfoundednessUnexpectedly$2.applyOrElse(TerminationPlugin.scala:150)
at viper.silver.plugin.standard.termination.TerminationPlugin$$anonfun$constrainsWellfoundednessUnexpectedly$2.applyOrElse(TerminationPlugin.scala:147)
at scala.PartialFunction$Lifted.apply(PartialFunction.scala:338)
at scala.PartialFunction$Lifted.apply(PartialFunction.scala:334)
at viper.silver.ast.utility.Visitor$.$anonfun$shallowCollect$1(Visitor.scala:175)
at scala.collection.immutable.List.flatMap(List.scala:293)
at scala.collection.immutable.List.flatMap(List.scala:79)
at viper.silver.ast.utility.Visitor$.shallowCollect$1(Visitor.scala:174)
at viper.silver.ast.utility.Visitor$.$anonfun$shallowCollect$2(Visitor.scala:175)
at scala.Option.fold(Option.scala:263)
at viper.silver.ast.utility.Visitor$.$anonfun$shallowCollect$1(Visitor.scala:175)
at scala.collection.immutable.List.flatMap(List.scala:293)
at scala.collection.immutable.List.flatMap(List.scala:79)
at viper.silver.ast.utility.Visitor$.shallowCollect$1(Visitor.scala:174)
at viper.silver.ast.utility.Visitor$.$anonfun$shallowCollect$2(Visitor.scala:175)
at scala.Option.fold(Option.scala:263)
at viper.silver.ast.utility.Visitor$.$anonfun$shallowCollect$1(Visitor.scala:175)
at scala.collection.immutable.List.flatMap(List.scala:293)
at scala.collection.immutable.List.flatMap(List.scala:79)
at viper.silver.ast.utility.Visitor$.shallowCollect$1(Visitor.scala:174)
at viper.silver.ast.utility.Visitor$.shallowCollect(Visitor.scala:178)
at viper.silver.parser.PNode.shallowCollect(ParseAst.scala:76)
at viper.silver.parser.PNode.shallowCollect$(ParseAst.scala:75)
at viper.silver.parser.PForall.shallowCollect(ParseAst.scala:914)
at viper.silver.plugin.standard.termination.TerminationPlugin.constrainsWellfoundednessUnexpectedly(TerminationPlugin.scala:147)
at viper.silver.plugin.standard.termination.TerminationPlugin.$anonfun$beforeTranslate$5(TerminationPlugin.scala:173)
at scala.collection.immutable.List.flatMap(List.scala:293)
at scala.collection.immutable.List.flatMap(List.scala:79)
at viper.silver.plugin.standard.termination.TerminationPlugin.$anonfun$beforeTranslate$4(TerminationPlugin.scala:173)
at viper.silver.plugin.standard.termination.TerminationPlugin.$anonfun$beforeTranslate$4$adapted(TerminationPlugin.scala:167)
at scala.collection.immutable.List.foreach(List.scala:333)
at viper.silver.plugin.standard.termination.TerminationPlugin.beforeTranslate(TerminationPlugin.scala:167)
at viper.silver.plugin.SilverPluginManager.$anonfun$beforeTranslate$1(SilverPluginManager.scala:49)
at viper.silver.plugin.SilverPluginManager.$anonfun$foldWithError$1(SilverPluginManager.scala:30)
at scala.collection.immutable.ArraySeq.foldLeft(ArraySeq.scala:222)
at viper.silver.plugin.SilverPluginManager.foldWithError(SilverPluginManager.scala:28)
at viper.silver.plugin.SilverPluginManager.beforeTranslate(SilverPluginManager.scala:49)
at viper.silver.frontend.SilFrontend.doTranslation(SilFrontend.scala:304)
at viper.silver.frontend.SilFrontend.doTranslation$(SilFrontend.scala:302)
at viper.silicon.SiliconFrontend.doTranslation(Silicon.scala:338)
at viper.silicon.SiliconFrontend.doTranslation(Silicon.scala:338)
at viper.silver.frontend.DefaultFrontend.translation(Frontend.scala:247)
at viper.silver.frontend.DefaultFrontend.translation$(Frontend.scala:245)
at viper.silicon.SiliconFrontend.translation(Silicon.scala:338)
at viper.silver.frontend.DefaultPhases.$anonfun$Translation$1(Frontend.scala:115)
at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1(Frontend.scala:62)
at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1$adapted(Frontend.scala:60)
at scala.collection.immutable.List.foreach(List.scala:333)
at viper.silver.frontend.Frontend.runAllPhases(Frontend.scala:60)
at viper.silver.frontend.Frontend.runAllPhases$(Frontend.scala:59)
at viper.silicon.SiliconFrontend.runAllPhases(Silicon.scala:338)
at viper.silver.frontend.SilFrontend.execute(SilFrontend.scala:173)
at viper.silver.frontend.SilFrontend.execute$(SilFrontend.scala:150)
at viper.silicon.SiliconFrontend.execute(Silicon.scala:338)
at viper.silicon.SiliconRunnerInstance.runMain(Silicon.scala:391)
at viper.silicon.SiliconRunner$.main(Silicon.scala:382)
at viper.silicon.SiliconRunner.main(Silicon.scala)
jcp19 commented
The fact that this fails in both Silicon and Carbon may indicate that this is a Silver issue
marcoeilers commented
Fixed in viperproject/silver#730