search

utwente-fmt / vercors

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

VerCors crash should be more informative if crash is caused by unsound axiom being added #1255

Open bobismijnnaam opened 1 month ago

bobismijnnaam commented 1 month ago

Crash Message

An error condition was reached, which should be statically unreachable. `requires true` is always satisfiable.. Inner failure:
 > ======================================
 > At test.pvl
 > --------------------------------------
 >    14  }
 >    15  
 >       [-----------
 >    16  class C {
 >    17    
 >    18  }
 >        -]
 >    19  
 >    20  void m() {
 > --------------------------------------
 > The precondition of this contract may be unsatisfiable. If this is intentional, replace it with `requires false`. (https://utwente.nl/vercors#unsatisfiable)
 > ======================================
  at vct.col.origin.PanicBlame.blame(Blame.scala:1415)
  at vct.col.rewrite.CheckContractSatisfiability$AssertPassedNontrivialUnsatisfiable.blame(CheckContractSatisfiability.scala:48)
  at vct.col.rewrite.CheckContractSatisfiability$AssertPassedNontrivialUnsatisfiable.blame(CheckContractSatisfiability.scala:40)
  at vct.col.origin.ExpectedError.signalDone(ExpectedError.scala:32)
  at vct.main.stages.ExpectedErrors.$anonfun$run$1(ExpectedErrors.scala:16)
  at vct.main.stages.ExpectedErrors.$anonfun$run$1$adapted(ExpectedErrors.scala:16)
  at scala.collection.immutable.List.foreach(List.scala:333)
  at vct.main.stages.ExpectedErrors.run(ExpectedErrors.scala:16)
  at vct.main.stages.ExpectedErrors.run(ExpectedErrors.scala:12)
  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 vct.main.Main$.main(Main.scala:50)
  at vct.main.Main.main(Main.scala)

Version Information

Arguments

test.pvl --backend-file-base temp

File Inputs

test.pvl ```pvl // enum MyEnum { // } adt MyAdt { pure int my_enum1(MyAdt myEnum1); pure int one(); pure int two(); axiom one() == 1 && two() == 2; axiom one() == two(); } class C { } void m() { assert false; } ```

Full Log

``` 13:20:53.445 [INFO] Start: VerCors (at 13:20:53) 13:20:59.395 [INFO] Done: VerCors (at 13:20:59, duration: 00:00:05) 13:20:59.401 [ERROR] vct.col.origin.BlameUnreachable: An error condition was reached, which should be statically unreachable. `requires true` is always satisfiable.. Inner failure: > ====================================== > At test.pvl > -------------------------------------- > 14 } > 15 > [----------- > 16 class C { > 17 > 18 } > -] > 19 > 20 void m() { > -------------------------------------- > The precondition of this contract may be unsatisfiable. If this is intentional, replace it with `requires false`. (https://utwente.nl/vercors#unsatisfiable) > ====================================== at vct.col.origin.PanicBlame.blame(Blame.scala:1415) at vct.col.rewrite.CheckContractSatisfiability$AssertPassedNontrivialUnsatisfiable.blame(CheckContractSatisfiability.scala:48) at vct.col.rewrite.CheckContractSatisfiability$AssertPassedNontrivialUnsatisfiable.blame(CheckContractSatisfiability.scala:40) at vct.col.origin.ExpectedError.signalDone(ExpectedError.scala:32) at vct.main.stages.ExpectedErrors.$anonfun$run$1(ExpectedErrors.scala:16) at vct.main.stages.ExpectedErrors.$anonfun$run$1$adapted(ExpectedErrors.scala:16) at scala.collection.immutable.List.foreach(List.scala:333) at vct.main.stages.ExpectedErrors.run(ExpectedErrors.scala:16) at vct.main.stages.ExpectedErrors.run(ExpectedErrors.scala:12) 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) 13:20:59.402 [ERROR] !*!*!*!*!*!*!*!*!*!*!*! 13:20:59.402 [ERROR] ! VerCors has crashed ! 13:20:59.402 [ERROR] !*!*!*!*!*!*!*!*!*!*!*! 13:20:59.402 [ERROR] Please report this as a bug here: ```