New Ensuring/Require/Assert trees
- Ensurings/Require are now proper purescala trees - Introduce Assert as a tree - Simplify tactics to support arbitrary asserts/errors/inner ensurings - New phase to inject assertions for unsafe calls (array/map access) - Refactor Default and Induction tactic
Showing
- src/main/scala/leon/codegen/CodeGeneration.scala 6 additions, 0 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/evaluators/RecursiveEvaluator.scala 6 additions, 0 deletionssrc/main/scala/leon/evaluators/RecursiveEvaluator.scala
- src/main/scala/leon/frontends/scalac/ASTExtractors.scala 16 additions, 6 deletionssrc/main/scala/leon/frontends/scalac/ASTExtractors.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 63 additions, 44 deletionssrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/purescala/Definitions.scala 24 additions, 9 deletionssrc/main/scala/leon/purescala/Definitions.scala
- src/main/scala/leon/purescala/Extractors.scala 3 additions, 0 deletionssrc/main/scala/leon/purescala/Extractors.scala
- src/main/scala/leon/purescala/TreeOps.scala 48 additions, 0 deletionssrc/main/scala/leon/purescala/TreeOps.scala
- src/main/scala/leon/purescala/Trees.scala 16 additions, 0 deletionssrc/main/scala/leon/purescala/Trees.scala
- src/main/scala/leon/solvers/combinators/FunctionTemplate.scala 7 additions, 0 deletions...ain/scala/leon/solvers/combinators/FunctionTemplate.scala
- src/main/scala/leon/solvers/z3/FunctionTemplate.scala 18 additions, 37 deletionssrc/main/scala/leon/solvers/z3/FunctionTemplate.scala
- src/main/scala/leon/synthesis/Rules.scala 1 addition, 1 deletionsrc/main/scala/leon/synthesis/Rules.scala
- src/main/scala/leon/termination/SimpleTerminationChecker.scala 1 addition, 1 deletion...ain/scala/leon/termination/SimpleTerminationChecker.scala
- src/main/scala/leon/utils/PreprocessingPhase.scala 2 additions, 1 deletionsrc/main/scala/leon/utils/PreprocessingPhase.scala
- src/main/scala/leon/verification/AnalysisPhase.scala 3 additions, 9 deletionssrc/main/scala/leon/verification/AnalysisPhase.scala
- src/main/scala/leon/verification/DefaultTactic.scala 42 additions, 210 deletionssrc/main/scala/leon/verification/DefaultTactic.scala
- src/main/scala/leon/verification/InductionTactic.scala 53 additions, 102 deletionssrc/main/scala/leon/verification/InductionTactic.scala
- src/main/scala/leon/verification/InjectAsserts.scala 39 additions, 0 deletionssrc/main/scala/leon/verification/InjectAsserts.scala
- src/main/scala/leon/verification/Tactic.scala 27 additions, 7 deletionssrc/main/scala/leon/verification/Tactic.scala
- src/main/scala/leon/verification/VerificationCondition.scala 1 addition, 0 deletionssrc/main/scala/leon/verification/VerificationCondition.scala
- src/test/resources/regression/verification/purescala/invalid/Asserts1.scala 32 additions, 0 deletions.../regression/verification/purescala/invalid/Asserts1.scala
Loading
Please register or sign in to comment