-
- Downloads
Introduces a phase to protect exact type of vars
This new phase is invoked after the extraction phase. It will rewrite precondition (and postcondition) of functions to add instanceOf when the parameter (and return type) is a case class concrete type (instead of abstract class). If not done, then during the mapping to Z3 we lose the precise subtype information, and Z3 will be able to find non valid counter-examples, of a different case class for example. Since tests are very important, we introduce two testcases that make sure the issue is fixed. We also needed to update the Testcase runners to make use of the new pipeline.
Showing
- src/main/scala/leon/Main.scala 3 additions, 2 deletionssrc/main/scala/leon/Main.scala
- src/main/scala/leon/SubtypingPhase.scala 47 additions, 0 deletionssrc/main/scala/leon/SubtypingPhase.scala
- src/test/resources/regression/verification/purescala/valid/Subtyping1.scala 31 additions, 0 deletions.../regression/verification/purescala/valid/Subtyping1.scala
- src/test/resources/regression/verification/purescala/valid/Subtyping2.scala 21 additions, 0 deletions.../regression/verification/purescala/valid/Subtyping2.scala
- src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala 1 addition, 1 deletion...n/test/verification/PureScalaVerificationRegression.scala
- src/test/scala/leon/test/verification/XLangVerificationRegression.scala 1 addition, 1 deletion.../leon/test/verification/XLangVerificationRegression.scala
Loading
Please register or sign in to comment