-
- Downloads
Introduce support for methods and multiple objects/fields
Methods: -------- Methods are now supported in ADT roots only (e.g. single case classes or abstract classes). The phase `MethodLifting` converts them to normal global functions which makes them transparent to the rest of Leon. Introducing Leon Library: ------------------------- Common structures and functionalities can be shipped as part of the Library.scala file, which is a set of ADTs with methods. Imported via `import leon.Library._` New Annotations: ---------------- - @verified means library function will not be considered for verification unless specifically given through --functions - @proxy allows non-pure bodies, which will be silently ignored. pre/post need to be in purescala. Functions without bodies (e.g. proxy methods) are now materialized with a choose construct automatically, replicating the post-condition. This allows compilation to bytecode and execution of VCs refering to proxy methods. Tree Modifications: ------------------- - FunDef now have params, not args. - VarDecl is renamed ValDef. - Added methods in ClassDef, as well as This and MethodInvocation, both are converted to normal function calls by the MethodLifting phase.
Showing
- Library.scala 78 additions, 0 deletionsLibrary.scala
- library/src/main/scala/leon/Annotations.scala 2 additions, 0 deletionslibrary/src/main/scala/leon/Annotations.scala
- src/main/scala/leon/LeonFatalError.scala 5 additions, 1 deletionsrc/main/scala/leon/LeonFatalError.scala
- src/main/scala/leon/Main.scala 17 additions, 3 deletionssrc/main/scala/leon/Main.scala
- src/main/scala/leon/Reporter.scala 1 addition, 1 deletionsrc/main/scala/leon/Reporter.scala
- src/main/scala/leon/codegen/CodeGeneration.scala 5 additions, 4 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/codegen/CompilationUnit.scala 40 additions, 32 deletionssrc/main/scala/leon/codegen/CompilationUnit.scala
- src/main/scala/leon/evaluators/RecursiveEvaluator.scala 1 addition, 1 deletionsrc/main/scala/leon/evaluators/RecursiveEvaluator.scala
- src/main/scala/leon/evaluators/TracingEvaluator.scala 1 addition, 1 deletionsrc/main/scala/leon/evaluators/TracingEvaluator.scala
- src/main/scala/leon/frontends/scalac/ASTExtractors.scala 23 additions, 79 deletionssrc/main/scala/leon/frontends/scalac/ASTExtractors.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 542 additions, 438 deletionssrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/frontends/scalac/ExtractionPhase.scala 16 additions, 5 deletionssrc/main/scala/leon/frontends/scalac/ExtractionPhase.scala
- src/main/scala/leon/frontends/scalac/LeonExtraction.scala 8 additions, 2 deletionssrc/main/scala/leon/frontends/scalac/LeonExtraction.scala
- src/main/scala/leon/purescala/CallGraph.scala 91 additions, 0 deletionssrc/main/scala/leon/purescala/CallGraph.scala
- src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala 44 additions, 0 deletions...in/scala/leon/purescala/CompleteAbstractDefinitions.scala
- src/main/scala/leon/purescala/Definitions.scala 49 additions, 114 deletionssrc/main/scala/leon/purescala/Definitions.scala
- src/main/scala/leon/purescala/Extractors.scala 1 addition, 0 deletionssrc/main/scala/leon/purescala/Extractors.scala
- src/main/scala/leon/purescala/FunctionClosure.scala 28 additions, 24 deletionssrc/main/scala/leon/purescala/FunctionClosure.scala
- src/main/scala/leon/purescala/MethodLifting.scala 111 additions, 0 deletionssrc/main/scala/leon/purescala/MethodLifting.scala
- src/main/scala/leon/purescala/PrettyPrinter.scala 51 additions, 10 deletionssrc/main/scala/leon/purescala/PrettyPrinter.scala
Loading
Please register or sign in to comment