gradual-verification / gvc0

Gradually Verified C0
6 stars 5 forks source link

Issue tracking location with singular unfold in list example #15

Closed icmccorm closed 2 years ago

icmccorm commented 2 years ago

Adding in the singular unfold sorted(list) in list_insert, with all other specifications made imprecise, triggers the following error:

single_unfold_program.txt

Exception in thread "main" gvc.weaver.WeaverException: Could not find location for !(b == c)
        at gvc.weaver.Collector$.$anonfun$collect$15(Collector.scala:561)
        at scala.collection.MapLike.getOrElse(MapLike.scala:131)
        at scala.collection.MapLike.getOrElse$(MapLike.scala:129)
        at scala.collection.AbstractMap.getOrElse(Map.scala:65)
        at gvc.weaver.Collector$.$anonfun$collect$14(Collector.scala:560)
        at scala.collection.immutable.List.$anonfun$foldRight$1(List.scala:447)
        at scala.collection.immutable.List.foldRight(List.scala:91)
        at gvc.weaver.Collector$.branchCondition$1(Collector.scala:557)
        at gvc.weaver.Collector$.$anonfun$collect$6(Collector.scala:354)
        at scala.collection.immutable.List.foreach(List.scala:431)
        at gvc.weaver.Collector$.gvc$weaver$Collector$$check$1(Collector.scala:353)
        at gvc.weaver.Collector$$anonfun$checkAll$1$1.applyOrElse(Collector.scala:413)
        at gvc.weaver.Collector$$anonfun$checkAll$1$1.applyOrElse(Collector.scala:413)
        at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:38)
        at viper.silver.ast.utility.Visitor$.visit(Visitor.scala:16)
        at viper.silver.ast.utility.Visitor$.$anonfun$visit$1(Visitor.scala:19)
        at viper.silver.ast.utility.Visitor$.$anonfun$visit$1$adapted(Visitor.scala:18)
        at scala.collection.immutable.List.foreach(List.scala:431)
        at viper.silver.ast.utility.Visitor$.visit(Visitor.scala:18)
        at viper.silver.ast.Node.visit(Ast.scala:75)
        at viper.silver.ast.Node.visit$(Ast.scala:74)
        at viper.silver.ast.MethodCall.visit(Statement.scala:82)
        at gvc.weaver.Collector$.checkAll$1(Collector.scala:413)
        at gvc.weaver.Collector$.visit$1(Collector.scala:432)
        at gvc.weaver.Collector$.$anonfun$collect$11(Collector.scala:476)
        at gvc.weaver.Collector$.$anonfun$collect$11$adapted(Collector.scala:458)
        at scala.collection.Iterator.foreach(Iterator.scala:943)
        at scala.collection.Iterator.foreach$(Iterator.scala:943)
        at gvc.transformer.IRGraph$Block$$anon$1.foreach(IRGraph.scala:341)
        at scala.collection.IterableLike.foreach(IterableLike.scala:74)
        at scala.collection.IterableLike.foreach$(IterableLike.scala:73)
        at gvc.transformer.IRGraph$ChildBlock.foreach(IRGraph.scala:359)
        at gvc.weaver.Collector$.visitBlock$1(Collector.scala:458)
        at gvc.weaver.Collector$.$anonfun$collect$11(Collector.scala:463)
        at gvc.weaver.Collector$.$anonfun$collect$11$adapted(Collector.scala:458)
        at scala.collection.Iterator.foreach(Iterator.scala:943)
        at scala.collection.Iterator.foreach$(Iterator.scala:943)
        at gvc.transformer.IRGraph$Block$$anon$1.foreach(IRGraph.scala:341)
        at scala.collection.IterableLike.foreach(IterableLike.scala:74)
        at scala.collection.IterableLike.foreach$(IterableLike.scala:73)
        at gvc.transformer.IRGraph$ChildBlock.foreach(IRGraph.scala:359)
        at gvc.weaver.Collector$.visitBlock$1(Collector.scala:458)
        at gvc.weaver.Collector$.$anonfun$collect$11(Collector.scala:463)
        at gvc.weaver.Collector$.$anonfun$collect$11$adapted(Collector.scala:458)
        at scala.collection.Iterator.foreach(Iterator.scala:943)
        at scala.collection.Iterator.foreach$(Iterator.scala:943)
        at gvc.transformer.IRGraph$Block$$anon$1.foreach(IRGraph.scala:341)
        at scala.collection.IterableLike.foreach(IterableLike.scala:74)
        at scala.collection.IterableLike.foreach$(IterableLike.scala:73)
        at gvc.transformer.IRGraph$MethodBlock.foreach(IRGraph.scala:355)
        at gvc.weaver.Collector$.visitBlock$1(Collector.scala:458)
        at gvc.weaver.Collector$.collect(Collector.scala:596)
        at gvc.weaver.Collector$.$anonfun$collect$1(Collector.scala:75)
        at scala.collection.immutable.List.map(List.scala:293)
        at gvc.weaver.Collector$.collect(Collector.scala:67)
        at gvc.weaver.Weaver$.weave(Weaver.scala:9)
        at gvc.Main$.verify(main.scala:186)
conradz commented 2 years ago

Fixed, I think by eff77b61fe3611da99dd353abcdd599697b9db85