epfl-lara/leon

Issues

• Termination -- java.lang.IllegalArgumentException

  #213 opened 9 years ago by BLepers
  3

• Invalid methods actually compiles

  #312 opened 8 years ago by Atry
  0

• Web interface appears to be failing

  #310 opened 8 years ago by eglassman
  3

• Bug in ImperativeCodeElimination

  #288 opened 8 years ago by mantognini
  0

• Can the leon library be published as a maven artifact?

  #303 opened 8 years ago by NicolasRouquette
  1

• Organization of the leon library

  #304 opened 8 years ago by NicolasRouquette
  0

• Support for generic copy() method

  #302 opened 8 years ago by pjmkrpg
  0

• Z3 exception

  #296 opened 8 years ago by BLepers
  3

• Moving to GPL from BSD

  #282 opened 8 years ago by sirinath
  2

• Bug in RecursionCountInstrumenter(?)

  #289 opened 8 years ago by mantognini
  0

• Bug in program evaluation/verification

  #287 opened 8 years ago by mantognini
  0

• Bug in proofs

  #279 opened 8 years ago by BLepers
  10

• Problem with preprocessing?

  #261 opened 8 years ago by jad-hamza
  3

• Termination checker is unsound in handling streams

  #248 opened 8 years ago by ravimad
  0

• Add doc for @traceInduct

  #249 opened 8 years ago by ravimad
  0

• Adding ensuring(rec < ...) in a function prevents other functions from being verified

  #243 opened 9 years ago by BLepers
  0

• Prover error in operation functions: ERROR "Type unification failed: Clash of types \"<markup>\" and \"<markup>\"\n\nType error in application: incompatible operand type\n\n<markup>\n<markup>\n\n<markup>"

  #238 opened 9 years ago by tomjridge
  4

• leon with isabelle, undefined session, documentation

  #237 opened 9 years ago by tomjridge
  4

• ensuring(rec <= ...) -- big verification time variation

  #214 opened 9 years ago by BLepers
  21

• TODO exception with Map's and class Invariants

  #226 opened 9 years ago by jad-hamza
  0

• Termination checker unable to prove termination of mutually recursive functions

  #225 opened 9 years ago by Sumith1896
  1

• Compilation issue

  #223 opened 9 years ago by BLepers
  2

• Simple use of lemmas for preconditions (feature request?)

  #218 opened 9 years ago by BLepers
  4

• Termination issue

  #212 opened 9 years ago by BLepers
  1

• Use cla-assistant to manage CLAs

  #182 opened 9 years ago by Sumith1896
  0

• Improving the code for declaring ADTs.

  #206 opened 9 years ago by ravimad
  0

• Counter-example not well typed in presence of lambdas

  #203 opened 9 years ago by jad-hamza
  1

• List.find(lambda) is of type <untyped>

  #204 opened 9 years ago by BLepers
  3

• Fatal error with class invariants

  #197 opened 9 years ago by jad-hamza
  3

• Feature Request: Class State Invariant

  #103 opened 9 years ago by liufengyun
  10

• Missing import statement in documentation example

  #199 opened 9 years ago by nunomota
  2

• State#forever doesn't terminate

  #148 opened 9 years ago by larsrh
  1

• Evaluation of passes fails to record positions of patterns, guards, scrutinees

  #161 opened 9 years ago by colder
  1

• Closures inside case classes

  #155 opened 9 years ago by jad-hamza
  3

• PortfolioSolver with incremental smtlib solvers

  #156 opened 9 years ago by colder
  0

• Use SMTLIB solvers in Orb to prevent solver handups and JVM crashes

  #154 opened 9 years ago by ravimad
  1

• CallGraph doesn't track function calls in patterns

  #143 opened 9 years ago by larsrh
  0

• Pretty printing doesn't print annotation (arguments)

  #146 opened 9 years ago by larsrh
  0

• CodeGenPhase is dead code

  #144 opened 9 years ago by larsrh
  2

• Map#get vs. Map#apply

  #133 opened 9 years ago by larsrh
  1

• ListSpecs.reverseIndex does not terminate

  #129 opened 9 years ago by larsrh
  2

• smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file

  #127 opened 9 years ago by larsrh
  3

• Missing filename from compiler errors/warnings

  #105 opened 10 years ago by olafurpg
  1

• Analyze division by zero-bitvector, modulo/remainder by zero

  #114 opened 10 years ago by samuelgruetter
  3

• Using TailRecursive printer in scala-smtlib

  #112 opened 10 years ago by samarion
  0

• Counterexample does not violate precondition of lambda passed to HOF

  #109 opened 10 years ago by samuelgruetter
  1

• --eval crashes with lambdas

  #110 opened 10 years ago by samuelgruetter
  1

• evaluation and verification don't agree on modulo

  #108 opened 10 years ago by samuelgruetter
  2

• Leon fails to verify simple list filtering

  #106 opened 10 years ago by liufengyun
  2

• Cryptic error message: "Don't know what to do with this. Not purescala?"

  #107 opened 10 years ago by olafurpg
  2