- Apr 13, 2022
-
-
BRUN Lelio authored
-
- Jun 30, 2021
-
-
BRUN Lelio authored
-
- Jun 29, 2021
-
-
BRUN Lelio authored
-
- Jun 17, 2021
-
-
BRUN Lelio authored
-
- Mar 09, 2021
-
-
BRUN Lelio authored
-
- Feb 05, 2021
-
-
BRUN Lelio authored
-
- Jan 27, 2020
-
-
Pierre Loic Garoche authored
-
- Nov 21, 2019
-
-
Pierre Loic Garoche authored
- Bugs in partial evaluation for equalities among bool constants and a nice recursive call generating a stack overflow! Now solved - Setup a timeout for z3 in seal - Better log for seal
-
- Nov 14, 2019
-
-
Pierre Loic Garoche authored
- real constants are hidden in Real.ml{i} module
-
- Jul 11, 2019
-
-
Pierre Loic Garoche authored
-
- Jul 04, 2019
-
-
Pierre Loic Garoche authored
-
- Nov 21, 2018
-
-
Pierre Loic Garoche authored
Different parsers yet but shared process. In case of lusi input the C backend is bypassed since the .h is generated from the lusic and no C code should be generated since it may overwrite existing manually written code But
-
- Nov 12, 2018
-
-
Pierre Loic Garoche authored
-
- Mar 30, 2018
-
-
Pierre Loic Garoche authored
-
- Mar 14, 2018
-
-
Pierre Loic Garoche authored
- program type renamed as program_t - Initiating the lustrev tool with dependencies to z3 and seal.
-
- Jan 31, 2018
-
-
Pierre Loic Garoche authored
[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8) typing was transformed as a functor and parametrized by basic types (int/real/bool) it can also be applied multiple times on the same program
-
- Jan 16, 2018
-
-
Pierre Loic Garoche authored
-
- Nov 14, 2017
-
-
Pierre Loic Garoche authored
-
- Nov 09, 2017
-
-
Pierre Loic Garoche authored
-
- Jul 20, 2017
-
-
Pierre Loic Garoche authored
-
- Jul 17, 2017
-
-
Pierre Loic Garoche authored
-
- Jul 12, 2017
-
-
Pierre Loic Garoche authored
-
- Jul 03, 2017
-
-
Pierre Loic Garoche authored
-
- Jun 23, 2017
-
-
Pierre Loic Garoche authored
- EMF backend now impose the optimization level to be set to 0 in order to avoid equation elimination that would render traceability difficult - Options.ml has been split into Options.ml / Options_management.ml. Options.ml only contains references and no functions
-
Pierre Loic Garoche authored
- Addtional encapsulation of machine_code instr in a struct to enable future extension of type with more metadata. - Improved EMF backend with META information
-
- Jun 22, 2017
-
-
Pierre Loic Garoche authored
[bug] seems to crash with EMF backend
-
Pierre Loic Garoche authored
Impact: - EMF backend has an extra machines argument - specific option to avoid merge of ite constructs - set_backend function to improve backend selection Most code was extracted from seahorn_backend through c0f8
-
- May 16, 2017
-
-
Pierre Loic Garoche authored
- allow multiple -I dir, will be used in order (first one declared is first used) - when declaring a global library #open <foo>, foo is first checked in local folders, than in global one (install path). This does not apply to local libraries opened with #open "foo".
-
Pierre Loic Garoche authored
-
- Apr 25, 2017
-
-
Pierre Loic Garoche authored
-
- Apr 05, 2017
-
-
THIRIOUX Xavier authored
mostly a recovery of an ancient svn repo: mutations
-
- Jan 31, 2017
-
-
Pierre Loic Garoche authored
-
- Jan 03, 2017
-
-
Pierre Loic Garoche authored
-
- Dec 30, 2016
-
-
Temesghen Kahsai authored
-
- Dec 29, 2016
-
-
Temesghen Kahsai authored
-
- Dec 08, 2016
-
-
Temesghen Kahsai authored
-
- Oct 20, 2016
-
-
THIRIOUX Xavier authored
-
- Oct 12, 2016
-
-
Julien Braine authored
-
- Sep 30, 2016
-
-
Temesghen Kahsai authored
-
- Sep 07, 2016
-
-
Pierre Loic Garoche authored
-