search

utwente-fmt / vercors

The VerCors verification toolset for verifying parallel and concurrent software
https://utwente.nl/vercors
Mozilla Public License 2.0
58 stars 26 forks source link

Crash report: The silver AST delivered to viper is not valid: - Consistency error: Perm and forperm in this conte #1274

Open etiennebirling opened 1 month ago

etiennebirling commented 1 month ago

Crash Message

The silver AST delivered to viper is not valid:
 - Consistency error: Perm and forperm in this context are only allowed if nested under inhale-exhale assertions. (forperm.c-7--7;unique_id=481)
  at viper.api.backend.SilverBackend.$anonfun$transform$1(SilverBackend.scala:107)
  at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16)
  at hre.progress.Progress$.stages(Progress.scala:47)
  at viper.api.backend.SilverBackend.transform(SilverBackend.scala:90)
  at viper.api.backend.SilverBackend.transform$(SilverBackend.scala:81)
  at viper.api.backend.silicon.Silicon.transform(Silicon.scala:34)
  at vct.main.stages.SilverBackend.transform(Backend.scala:196)
  at vct.main.stages.Backend.$anonfun$run$3(Backend.scala:152)
  at hre.progress.Progress$.$anonfun$map$2(Progress.scala:35)
  at hre.progress.task.AbstractTask.frame(AbstractTask.scala:166)
  at hre.progress.Progress$.$anonfun$map$1(Progress.scala:35)
  at scala.collection.parallel.IterableSplitter$Mapped.next(RemainsIterator.scala:463)
  ...
  at vct.main.Main$.main(Main.scala:50)
  at vct.main.Main.main(Main.scala)

Version Information

Arguments

forperm.c

File Inputs

forperm.c ```c struct t {int val;}; struct f {int cac;}; /*@ requires \pointer(this, 10, write); requires Perm(this->val, 1); ensures \pointer(this, 10, write); ensures (\forperm struct f * this \in this->cac; false); ensures Perm(this->val, 1); @*/ void incr(struct t* this, int n) { this->val = this->val + n; } ```

Full Log

``` 18:37:13.619 [INFO] Start: VerCors (at 18:37:13) 18:37:17.463 [INFO] Done: VerCors (at 18:37:17, duration: 00:00:03) 18:37:17.465 [ERROR] viper.api.backend.SilverBackend$ConsistencyErrors: The silver AST delivered to viper is not valid: - Consistency error: Perm and forperm in this context are only allowed if nested under inhale-exhale assertions. (forperm.c-7--7;unique_id=481) at viper.api.backend.SilverBackend.$anonfun$transform$1(SilverBackend.scala:107) at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16) at hre.progress.Progress$.stages(Progress.scala:47) at viper.api.backend.SilverBackend.transform(SilverBackend.scala:90) at viper.api.backend.SilverBackend.transform$(SilverBackend.scala:81) at viper.api.backend.silicon.Silicon.transform(Silicon.scala:34) at vct.main.stages.SilverBackend.transform(Backend.scala:196) at vct.main.stages.Backend.$anonfun$run$3(Backend.scala:152) at hre.progress.Progress$.$anonfun$map$2(Progress.scala:35) at hre.progress.task.AbstractTask.frame(AbstractTask.scala:166) at hre.progress.Progress$.$anonfun$map$1(Progress.scala:35) at scala.collection.parallel.IterableSplitter$Mapped.next(RemainsIterator.scala:463) at scala.collection.immutable.List.prependedAll(List.scala:153) at scala.collection.immutable.List$.from(List.scala:684) at scala.collection.immutable.List$.from(List.scala:681) at scala.collection.SeqFactory$Delegate.from(Factory.scala:306) at scala.collection.immutable.Seq$.from(Seq.scala:42) at scala.collection.immutable.Seq$.from(Seq.scala:39) at scala.collection.IterableFactory$ToFactory.fromSpecific(Factory.scala:274) at scala.collection.IterableOnceOps.to(IterableOnce.scala:1310) at scala.collection.IterableOnceOps.to$(IterableOnce.scala:1310) at scala.collection.parallel.IterableSplitter$Mapped.to(RemainsIterator.scala:460) at vct.main.stages.Backend.$anonfun$run$1(Backend.scala:153) at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16) at hre.progress.Progress$.stages(Progress.scala:47) at vct.main.stages.Backend.run(Backend.scala:145) at vct.main.stages.Backend.run$(Backend.scala:137) at vct.main.stages.SilverBackend.run(Backend.scala:184) at vct.main.stages.SilverBackend.run(Backend.scala:184) at hre.stages.Stages.$anonfun$run$3(Stages.scala:104) at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:101) at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576) at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574) at scala.collection.AbstractIterable.foreach(Iterable.scala:933) at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903) at hre.stages.Stages.$anonfun$run$1(Stages.scala:101) at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16) at hre.progress.Progress$.stages(Progress.scala:47) at hre.stages.Stages.run(Stages.scala:98) at hre.stages.Stages.run$(Stages.scala:95) at hre.stages.StagesPair.run(Stages.scala:145) at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:64) at vct.main.modes.Verify$.$anonfun$runOptions$3(Verify.scala:99) at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17) at hre.util.Time$.logTime(Time.scala:23) at vct.main.modes.Verify$.runOptions(Verify.scala:99) at vct.main.Main$.runMode(Main.scala:107) at vct.main.Main$.$anonfun$runOptions$3(Main.scala:100) at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17) at hre.middleware.Middleware$.using(Middleware.scala:78) at vct.main.Main$.$anonfun$runOptions$2(Main.scala:100) at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17) at hre.io.Watch$.booleanWithWatch(Watch.scala:58) at vct.main.Main$.$anonfun$runOptions$1(Main.scala:100) at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17) at hre.middleware.Middleware$.using(Middleware.scala:78) at vct.main.Main$.runOptions(Main.scala:95) at vct.main.Main$.main(Main.scala:50) at vct.main.Main.main(Main.scala) 18:37:17.465 [ERROR] !*!*!*!*!*!*!*!*!*!*!*! 18:37:17.465 [ERROR] ! VerCors has crashed ! 18:37:17.465 [ERROR] !*!*!*!*!*!*!*!*!*!*!*! 18:37:17.465 [ERROR] Please report this as a bug here: ```
superaxander commented 1 month ago

Thanks for the report, the lack of a proper error here is definitely a bug. In VerCors we write Viper's inhale-exhale expression as \polarity_dependent(inhale_expr, exhale_expr) that should allow you to use \forperm here