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

[etiennebirling]

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

• VerCors version 2.2.0
• At commit a6105f9 from branch HEAD (changes=false)

Arguments

forperm.c

File Inputs

forperm.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]

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