Support FiniteArray in CodeGen
NonEmptyArray is required to be nonempty Allow arbitrary expression as length in CodeGeneration Handle FiniteArray in valueToJVM Add integration tests finiteArray makes EmptyArray for arrays of size 0 Fail when z3 returns negative size array
Showing
- src/main/java/leon/codegen/runtime/ArrayBox.java 0 additions, 2 deletionssrc/main/java/leon/codegen/runtime/ArrayBox.java
- src/main/scala/leon/codegen/CodeGeneration.scala 22 additions, 6 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/codegen/CompilationUnit.scala 39 additions, 0 deletionssrc/main/scala/leon/codegen/CompilationUnit.scala
- src/main/scala/leon/evaluators/Evaluator.scala 1 addition, 1 deletionsrc/main/scala/leon/evaluators/Evaluator.scala
- src/main/scala/leon/purescala/Constructors.scala 1 addition, 1 deletionsrc/main/scala/leon/purescala/Constructors.scala
- src/main/scala/leon/purescala/Expressions.scala 1 addition, 0 deletionssrc/main/scala/leon/purescala/Expressions.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 5 additions, 0 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala 46 additions, 35 deletions...a/leon/integration/evaluators/CodegenEvaluatorSuite.scala
Loading
Please register or sign in to comment