| Branch: | Tag: | Revision:

lustrec / @ d75eb6f1

History | View | Annotate | Download (11.1 KB)

# Date Author Comment
f4cba4b8 03/12/2019 11:23 AM Pierre-Loïc Garoche

Some progress on compiling cocospec contract.
Contract resolution still need to be done as well as dealing with the machine code level and so on.

32bafa6f 11/20/2018 11:20 PM Pierre-Loïc Garoche

Some thoughts about lusic

59803095 11/16/2018 11:30 PM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal

0d54d8a8 11/13/2018 02:01 AM Pierre-Loïc Garoche

Removed Contract contruct: imported node should be enough. Solved some warning at compile time

82906771 11/08/2018 03:58 PM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal

a703ed0c 11/03/2018 12:03 AM Pierre-Loïc Garoche

Preprocess the selected node in seaL BACKEND: focus on memories and perform node slicing.

4f26dcf5 09/13/2018 03:36 PM Pierre-Loïc Garoche

Renamed annots into contracts. Preparing for syntax extension

17e1d0f4 09/13/2018 03:14 PM Pierre-Loïc Garoche

- Removed the kind2 file (parser/lexer/types)
- Cleaned a little bit our parser: removal of old prelude constructs

37d3e0eb 09/13/2018 01:55 PM Pierre-Loïc Garoche

Cocospec discussions in the

2fb97ad4 03/30/2018 11:43 PM Pierre-Loïc Garoche

Merge conflict solved

53472c83 03/29/2018 03:53 PM Pierre-Loïc Garoche

Updated TODO
Changed selection of files in odocl

0dee2bc1 11/20/2015 06:41 PM Pierre-Loïc Garoche

Refactoring of the horn backend with Reset/Step instead of Init/Step.
Teme, please perform a string non regression test wrt the previous version, to make sure we have the same model checking results.

7c95dcab 10/08/2015 07:11 PM Pierre-Loïc Garoche

Two fresh branches :)
to manage enum and arrays in the horn backend.

0cbf0839 10/02/2013 08:13 AM Pierre-Loïc Garoche

Moved files to trunk in lustre_compiler