search

viperproject / chalice2silver

Other
0 stars 0 forks source link

Crash when receive expression creates new variable #85

Open viper-admin opened 7 years ago

viper-admin commented 7 years ago

Created by @vakaras on 2016-12-20 17:48

The following program:

#!chalice
class A
{

    method cr(other:A, ch:C1)
    {
        receive b := ch
    }
}

channel C1(m: A) where true;

crashes with the stack trace:

[info] - obligations/christian/syntax.chalice [carbon-Chalice2Silver-Silver] *** FAILED *** (600 milliseconds)
[info]   1 errors
[info]
[info]   The following output occurred during testing, but should not have according to the test annotations:
[info]     [verifier.exception] scala.sys.package$.error(package.scala:27)
[info]   viper.carbon.verifier.Environment.get(Environment.scala:54)
[info]   viper.carbon.modules.impls.DefaultExpModule.translateLocalVar(DefaultExpModule.scala:249)
[info]   viper.carbon.modules.impls.DefaultExpModule.translateExp(DefaultExpModule.scala:52)
[info]   viper.carbon.modules.impls.DefaultStmtModule.simpleHandleStmt(DefaultStmtModule.scala:65)
[info]   viper.carbon.modules.impls.DefaultStmtModule.handleStmt(DefaultStmtModule.scala:57)
[info]   viper.carbon.modules.impls.DefaultStmtModule$$anonfun$translateStmt$2.apply(DefaultStmtModule.scala:229)
[info]   viper.carbon.modules.impls.DefaultStmtModule$$anonfun$translateStmt$2.apply(DefaultStmtModule.scala:228)
[info]   scala.collection.immutable.List.foreach(List.scala:381)
[info]   viper.carbon.modules.impls.DefaultStmtModule.translateStmt(DefaultStmtModule.scala:228)
[info]   viper.carbon.modules.impls.DefaultStmtModule$$anonfun$translateStmt$1.apply(DefaultStmtModule.scala:206)
[info]   viper.carbon.modules.impls.DefaultStmtModule$$anonfun$translateStmt$1.apply(DefaultStmtModule.scala:206)
[info]   scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
[info]   scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
[info]   scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
[info]   scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
[info]   scala.collection.TraversableLike$class.map(TraversableLike.scala:245)
[info]   scala.collection.AbstractTraversable.map(Traversable.scala:104)
[info]   viper.carbon.modules.impls.DefaultStmtModule.translateStmt(DefaultStmtModule.scala:206)
[info]   viper.carbon.modules.impls.DefaultStmtModule$$anonfun$translateStmt$1.apply(DefaultStmtModule.scala:206)
[info]   viper.carbon.modules.impls.DefaultStmtModule$$anonfun$translateStmt$1.apply(DefaultStmtModule.scala:206)
[info]   scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
[info]   scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
[info]   scala.collection.immutable.List.foreach(List.scala:381)
[info]   scala.collection.TraversableLike$class.map(TraversableLike.scala:245)
[info]   scala.collection.immutable.List.map(List.scala:285)
[info]   viper.carbon.modules.impls.DefaultStmtModule.translateStmt(DefaultStmtModule.scala:206)
[info]   viper.carbon.modules.impls.DefaultMainModule.translateMethodDecl(DefaultMainModule.scala:111)
[info]   viper.carbon.modules.impls.DefaultMainModule$$anonfun$7.apply(DefaultMainModule.scala:66)
[info]   viper.carbon.modules.impls.DefaultMainModule$$anonfun$7.apply(DefaultMainModule.scala:66)
[info]   scala.collection.immutable.Stream.flatMap(Stream.scala:489)
[info]   viper.carbon.modules.impls.DefaultMainModule.translate(DefaultMainModule.scala:66)
[info]   viper.carbon.CarbonVerifier.verify(CarbonVerifier.scala:128)
[info]   viper.chalice2sil.Chalice2SILFrontEnd.verify(Chalice2SILFrontend.scala:123)
[info]   viper.silver.frontend.DefaultPhases$$anonfun$5.apply$mcV$sp(Frontend.scala:72)
[info]   viper.silver.frontend.DefaultPhases$$anonfun$5.apply(Frontend.scala:72)
[info]   viper.silver.frontend.DefaultPhases$$anonfun$5.apply(Frontend.scala:72)
[info]   viper.silver.testing.TimingUtils$class.time(SilSuite.scala:144)
[info]   viper.silver.testing.SilSuite$VerifierUnderTest.time(SilSuite.scala:89)
[info]   viper.silver.testing.SilSuite$VerifierUnderTest$$anonfun$1.apply(SilSuite.scala:97)
[info]   viper.silver.testing.SilSuite$VerifierUnderTest$$anonfun$1.apply(SilSuite.scala:96)
[info]   scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
[info]   scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
[info]   scala.collection.immutable.List.foreach(List.scala:381)
[info]   scala.collection.TraversableLike$class.map(TraversableLike.scala:245)
[info]   scala.collection.immutable.List.map(List.scala:285)
[info]   viper.silver.testing.SilSuite$VerifierUnderTest.run(SilSuite.scala:96)
[info]   viper.silver.testing.AnnotationBasedTestSuite$$anonfun$registerTest$1.apply$mcV$sp(AnnotationBasedTestSuite.scala:45)
[info]   viper.silver.testing.AnnotationBasedTestSuite$$anonfun$registerTest$1.apply(AnnotationBasedTestSuite.scala:40)
[info]   viper.silver.testing.AnnotationBasedTestSuite$$anonfun$registerTest$1.apply(AnnotationBasedTestSuite.scala:40)
[info]   org.scalatest.Transformer$$anonfun$apply$1.apply$mcV$sp(Transformer.scala:22)
[info]   org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85)
[info]   org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
[info]   org.scalatest.Transformer.apply(Transformer.scala:22)
[info]   org.scalatest.Transformer.apply(Transformer.scala:20)
[info]   org.scalatest.FunSuiteLike$$anon$1.apply(FunSuiteLike.scala:166)
[info]   org.scalatest.Suite$class.withFixture(Suite.scala:1122)
[info]   org.scalatest.FunSuite.withFixture(FunSuite.scala:1555)
[info]   org.scalatest.FunSuiteLike$class.invokeWithFixture$1(FunSuiteLike.scala:163)
[info]   org.scalatest.FunSuiteLike$$anonfun$runTest$1.apply(FunSuiteLike.scala:175)
[info]   org.scalatest.FunSuiteLike$$anonfun$runTest$1.apply(FunSuiteLike.scala:175)
[info]   org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
[info]   org.scalatest.FunSuiteLike$class.runTest(FunSuiteLike.scala:175)
[info]   viper.silver.testing.ResourceBasedTestSuite.runTest(ResourceBasedTestSuite.scala:271)
[info]   org.scalatest.FunSuiteLike$$anonfun$runTests$1.apply(FunSuiteLike.scala:208)
[info]   org.scalatest.FunSuiteLike$$anonfun$runTests$1.apply(FunSuiteLike.scala:208)
[info]   org.scalatest.SuperEngine$$anonfun$traverseSubNodes$1$1.apply(Engine.scala:413)
[info]   org.scalatest.SuperEngine$$anonfun$traverseSubNodes$1$1.apply(Engine.scala:401)
[info]   scala.collection.immutable.List.foreach(List.scala:381)
[info]   org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
[info]   org.scalatest.SuperEngine.org$scalatest$SuperEngine$$runTestsInBranch(Engine.scala:396)
[info]   org.scalatest.SuperEngine.runTestsImpl(Engine.scala:483)
[info]   org.scalatest.FunSuiteLike$class.runTests(FunSuiteLike.scala:208)
[info]   viper.silver.testing.ResourceBasedTestSuite.runTests(ResourceBasedTestSuite.scala:283)
[info]   org.scalatest.Suite$class.run(Suite.scala:1424)
[info]   org.scalatest.FunSuite.org$scalatest$FunSuiteLike$$super$run(FunSuite.scala:1555)
[info]   org.scalatest.FunSuiteLike$$anonfun$run$1.apply(FunSuiteLike.scala:212)
[info]   org.scalatest.FunSuiteLike$$anonfun$run$1.apply(FunSuiteLike.scala:212)
[info]   org.scalatest.SuperEngine.runImpl(Engine.scala:545)
[info]   org.scalatest.FunSuiteLike$class.run(FunSuiteLike.scala:212)
[info]   viper.silver.testing.ResourceBasedTestSuite.run(ResourceBasedTestSuite.scala:295)
[info]   viper.silver.testing.SilSuite.org$scalatest$BeforeAndAfterAll$$super$run(SilSuite.scala:17)
[info]   org.scalatest.BeforeAndAfterAll$class.liftedTree1$1(BeforeAndAfterAll.scala:257)
[info]   org.scalatest.BeforeAndAfterAll$class.run(BeforeAndAfterAll.scala:256)
[info]   viper.silver.testing.SilSuite.run(SilSuite.scala:17)
[info]   org.scalatest.tools.Framework.org$scalatest$tools$Framework$$runSuite(Framework.scala:462)
[info]   org.scalatest.tools.Framework$ScalaTestTask.execute(Framework.scala:671)
[info]   sbt.ForkMain$Run$2.call(ForkMain.java:296)
[info]   sbt.ForkMain$Run$2.call(ForkMain.java:286)
[info]   java.util.concurrent.FutureTask.run(FutureTask.java:266)
[info]   java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1142)
[info]   java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:617)
[info]   java.lang.Thread.run(Thread.java:745) (syntax.chalice@2.1) (AnnotationBasedTestSuite.scala:63)
[info]   + Verifier used: carbon 1.0.
[info]   + Time required: 82 msec (parse), 0 msec (typecheck), 43 msec (translate), 471 msec (verify).