(a) Adding support for inferring invariants in Leon.
(b) Adding support for inferring time, depth, stack and rec bounds (c) Adding support for compositional reasoning in inferrence of time bounds (d) Adding support for estimating stack usage at runtime (e) Adding support for fractional literals
Showing
- build.sbt 1 addition, 1 deletionbuild.sbt
- leon-change-notes 155 additions, 0 deletionsleon-change-notes
- library/annotation/package.scala 5 additions, 2 deletionslibrary/annotation/package.scala
- library/instrumentation/package.scala 24 additions, 0 deletionslibrary/instrumentation/package.scala
- library/invariant/package.scala 26 additions, 0 deletionslibrary/invariant/package.scala
- library/lang/synthesis/package.scala 1 addition, 1 deletionlibrary/lang/synthesis/package.scala
- library/par/package.scala 3 additions, 2 deletionslibrary/par/package.scala
- src/main/java/leon/codegen/runtime/Rational.java 127 additions, 0 deletionssrc/main/java/leon/codegen/runtime/Rational.java
- src/main/scala/leon/Main.scala 16 additions, 7 deletionssrc/main/scala/leon/Main.scala
- src/main/scala/leon/codegen/CodeGeneration.scala 101 additions, 99 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/codegen/CompilationUnit.scala 20 additions, 18 deletionssrc/main/scala/leon/codegen/CompilationUnit.scala
- src/main/scala/leon/codegen/CompiledExpression.scala 1 addition, 1 deletionsrc/main/scala/leon/codegen/CompiledExpression.scala
- src/main/scala/leon/evaluators/CodeGenEvaluator.scala 3 additions, 3 deletionssrc/main/scala/leon/evaluators/CodeGenEvaluator.scala
- src/main/scala/leon/evaluators/RecursiveEvaluator.scala 41 additions, 31 deletionssrc/main/scala/leon/evaluators/RecursiveEvaluator.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 16 additions, 16 deletionssrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala 235 additions, 0 deletions...a/leon/invariant/engine/CompositionalTemplateSolver.scala
- src/main/scala/leon/invariant/engine/ConstraintTracker.scala 45 additions, 0 deletionssrc/main/scala/leon/invariant/engine/ConstraintTracker.scala
- src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala 165 additions, 0 deletions...in/scala/leon/invariant/engine/InferInvariantsPhase.scala
- src/main/scala/leon/invariant/engine/InferenceContext.scala 31 additions, 0 deletionssrc/main/scala/leon/invariant/engine/InferenceContext.scala
- src/main/scala/leon/invariant/engine/InferenceEngine.scala 179 additions, 0 deletionssrc/main/scala/leon/invariant/engine/InferenceEngine.scala
Loading
Please register or sign in to comment