search

viperproject / chalice2silver

Other
0 stars 0 forks source link

Crash with mustRelease(this, 1); in precondition. #81

Open viper-admin opened 8 years ago

viper-admin commented 8 years ago

Created by @vakaras on 2016-04-13 14:56

The following example:

#!chalice

class A {

  method test() {
    acquire this;
    call do_release();
  }

  method do_release()
    requires mustRelease(this, 1);
  {
    release this;
  }

}

crashes with the following error:

[info]     [chalice2silver.error] java.lang.AssertionError: assertion failed: Cannot deal with: ExplicitThisExpr() in argumentscala.Predef$.assert(Predef.scala:165)
[info]   viper.chalice2sil.translation.LifetimeFunctionHandler$$anonfun$getLifetimeAssumptions$1$$anonfun$apply$2.apply(LifetimeFunctions.scala:546)
[info]   viper.chalice2sil.translation.LifetimeFunctionHandler$$anonfun$getLifetimeAssumptions$1$$anonfun$apply$2.apply(LifetimeFunctions.scala:531)
[info]   chalice.AST$$anonfun$visit$1.apply(Ast.scala:1093)
[info]   chalice.AST$$anonfun$visit$1.apply(Ast.scala:1093)
[info]   chalice.AST$.visitOpt2(Ast.scala:1100)
[info]   chalice.AST$.visitOpt(Ast.scala:1097)
[info]   chalice.AST$.visit(Ast.scala:1093)
[info]   chalice.Expression.visit(Ast.scala:561)
[info]   viper.chalice2sil.translation.LifetimeFunctionHandler$$anonfun$getLifetimeAssumptions$1.apply(LifetimeFunctions.scala:531)
[info]   viper.chalice2sil.translation.LifetimeFunctionHandler$$anonfun$getLifetimeAssumptions$1.apply(LifetimeFunctions.scala:528)
[info]   scala.collection.immutable.List.foreach(List.scala:381)
[info]   viper.chalice2sil.translation.LifetimeFunctionHandler.getLifetimeAssumptions(LifetimeFunctions.scala:528)
[info]   viper.chalice2sil.translation.ProgramTranslator.translateStm(ProgramTranslator.scala:1866)
[info]   viper.chalice2sil.translation.ProgramTranslator$$anonfun$23.apply(ProgramTranslator.scala:1421)
[info]   viper.chalice2sil.translation.ProgramTranslator$$anonfun$23.apply(ProgramTranslator.scala:1421)
[info]   scala.collection.immutable.List.map(List.scala:277)
[info]   viper.chalice2sil.translation.ProgramTranslator.translateBody(ProgramTranslator.scala:1421)
[info]   viper.chalice2sil.translation.ProgramTranslator$$anonfun$translate$3.apply(ProgramTranslator.scala:418)
[info]   viper.chalice2sil.translation.ProgramTranslator$$anonfun$translate$3.apply(ProgramTranslator.scala:417)