-
- Downloads
Check preconditions/correctness conditions within specs
TransformerWithPaths now traverses Ensuring DefaultTactic.generatePreconditions and generateCorrectnessConditions now looks in fullBody Fix CodeGeneration to handle Require Don't collect Require, Ensuring in collectCorrectnessConditions
Showing
- src/main/scala/leon/codegen/CodeGeneration.scala 7 additions, 12 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/purescala/ExprOps.scala 3 additions, 3 deletionssrc/main/scala/leon/purescala/ExprOps.scala
- src/main/scala/leon/purescala/TransformerWithPC.scala 23 additions, 3 deletionssrc/main/scala/leon/purescala/TransformerWithPC.scala
- src/main/scala/leon/utils/TypingPhase.scala 1 addition, 1 deletionsrc/main/scala/leon/utils/TypingPhase.scala
- src/main/scala/leon/verification/DefaultTactic.scala 18 additions, 24 deletionssrc/main/scala/leon/verification/DefaultTactic.scala
- src/test/resources/regression/verification/purescala/invalid/PreInSpecs.scala 25 additions, 0 deletions...egression/verification/purescala/invalid/PreInSpecs.scala
- src/test/resources/regression/verification/purescala/valid/PreInSpecs.scala 25 additions, 0 deletions.../regression/verification/purescala/valid/PreInSpecs.scala
Loading
Please register or sign in to comment