-
- Downloads
fixed (I believe) redundant precondition generation. Now printing lines/cols...
fixed (I believe) redundant precondition generation. Now printing lines/cols for precondtions and match expressions. Functions in result table are also sorted by appearance in the file. Less useless println'ing
Showing
- src/funcheck/AnalysisComponent.scala 2 additions, 2 deletionssrc/funcheck/AnalysisComponent.scala
- src/funcheck/CodeExtraction.scala 9 additions, 5 deletionssrc/funcheck/CodeExtraction.scala
- src/purescala/Analysis.scala 14 additions, 11 deletionssrc/purescala/Analysis.scala
- src/purescala/Common.scala 29 additions, 0 deletionssrc/purescala/Common.scala
- src/purescala/DefaultTactic.scala 66 additions, 29 deletionssrc/purescala/DefaultTactic.scala
- src/purescala/Definitions.scala 1 addition, 1 deletionsrc/purescala/Definitions.scala
- src/purescala/Extensions.scala 5 additions, 1 deletionsrc/purescala/Extensions.scala
- src/purescala/IterativeZ3Solver.scala 17 additions, 0 deletionssrc/purescala/IterativeZ3Solver.scala
- src/purescala/PrettyPrinter.scala 6 additions, 2 deletionssrc/purescala/PrettyPrinter.scala
- src/purescala/Trees.scala 32 additions, 28 deletionssrc/purescala/Trees.scala
- src/purescala/VerificationCondition.scala 9 additions, 8 deletionssrc/purescala/VerificationCondition.scala
- src/purescala/Z3Solver.scala 1 addition, 1 deletionsrc/purescala/Z3Solver.scala
- src/purescala/z3plugins/instantiator/Instantiator.scala 1 addition, 1 deletionsrc/purescala/z3plugins/instantiator/Instantiator.scala
- testcases/RedBlack.scala 0 additions, 288 deletionstestcases/RedBlack.scala
Loading
Please register or sign in to comment