- May 21, 2014
-
-
Etienne Kneuss authored
More info at https://z3.codeplex.com/workitem/113
-
Etienne Kneuss authored
-
- May 06, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- May 05, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
- Ensurings/Require are now proper purescala trees - Introduce Assert as a tree - Simplify tactics to support arbitrary asserts/errors/inner ensurings - New phase to inject assertions for unsafe calls (array/map access) - Refactor Default and Induction tactic
-
- Apr 25, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Apr 11, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Nicolas Voirol authored
-
Etienne Kneuss authored
- NormalizationRule becomes priorities, so that we can have multiple distinct layers - Use the @library annotation, move synthesis stuff to synthesis, Oracles. - Make sure tests use PreprocessingPhase and import synthesis when adequate - Extract proper package objects fix patternRecons and simplifiers - Reorganize library: - leon.{choose,???} -> leon.lang.synthesis - leon.{waypoint,epsilon} -> leon.lang.xlang
-
- Apr 09, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Apr 08, 2014
-
-
Etienne Kneuss authored
-
- Apr 07, 2014
-
-
Etienne Kneuss authored
-
- Mar 25, 2014
-
-
Etienne Kneuss authored
-
- Mar 21, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Mar 20, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
- Holes become chooses - Unhandled types are removed, Untyped is now checked for and a warning is issued if an untyped expression is found.
-
- Mar 17, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
This allows us to use them in synthesis. Expose --solvers=.. option for synthesis.
-
Etienne Kneuss authored
-
- Mar 14, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Mar 13, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Mar 11, 2014
-
-
Lomig Mégard authored
-
Lomig Mégard authored
-
- Mar 05, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Mar 04, 2014
-
-
Etienne Kneuss authored
-
- Mar 03, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Feb 28, 2014
-
-
Etienne Kneuss authored
- Implement the Leon Library in Leon-land rather than Scala-land. import leon.Utils._ becomes import leon.lang._ import leon.Annotations._ becomes import leon.annontation._ For now, the library defines generic Options and Lists. The library is automatically imported from the ./leon script, unless the --library=no option is passed. - Support parsing of multiple files and modules. - Introduce new annontations: @ignore: remove definition from Leon @verified: do not consider for verification unless explicitly specified
-