Download (13.3 KB) Statistics
| Branch: | Tag: | Revision:

# Date Author Comment
ca7ff3f7 06/17/2021 11:33 AM Lélio Brun


6d1693b9 06/14/2021 07:06 PM Lélio Brun

work on spec generation almost done

75c459f4 05/04/2021 06:24 PM Lélio Brun

start with Spec AST generation

7ee5f69e 05/04/2021 10:20 AM Lélio Brun

corrections on loggers + spec in AST

15c3e4e7 03/08/2021 10:58 AM Lélio Brun

generic ACSL spec generation

c226a3ba 03/01/2021 03:56 PM Lélio Brun

start generating ACSL spec

90cc3b8e 02/19/2021 11:19 AM Lélio Brun

some rewriting in C backend pretty-printer

1df55e58 02/16/2021 04:21 PM Lélio Brun

minor rewriting

ca7e8027 02/05/2021 02:36 PM Lélio Brun

fix almost all warnings

719ae9fd 02/03/2021 02:47 PM Lélio Brun

migration draft on dune

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.

5de4dde4 11/24/2018 12:16 AM Pierre-Loïc Garoche

Major refreshing of machine generation

217837e2 11/21/2018 08:15 PM Pierre-Loïc Garoche

Unified compilation of lusi and lus files
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...

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

Merge branch 'unstable' into lustrec-seal

778c80fd 10/05/2018 07:54 PM Pierre-Loïc Garoche

Some refactoring
Adapted the parser/types/constructors for cocospec syntax