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

# Date Author Comment
e77a0fa5 10/06/2021 11:25 AM Lélio Brun

fix handling of state variables in spec expressions

81d69074 10/06/2021 10:18 AM Lélio Brun

fix bug where singleton tuples were generated

9c227bad 10/05/2021 01:55 PM Lélio Brun

fix offline tests

10131419 10/05/2021 11:17 AM Lélio Brun

add offline tests and fix a bug in generated spec where optimization was not performed

b2ad5de3 10/01/2021 01:46 PM Lélio Brun

fix tests procedure

89fd79f0 09/27/2021 06:00 PM Lélio Brun

a working version for automata with 'last' case of enums as default case

d29fbec5 09/27/2021 01:36 PM Lélio Brun

working version for stateful contracts

4fef1a04 09/23/2021 05:51 PM Lélio Brun

proper generation of stateful contracts

478edbed 09/23/2021 04:40 PM Lélio Brun

proper handling of stateless nodes and automata

0988cb68 09/23/2021 03:40 PM Lélio Brun

proper inductive case and no code generated for contracts

e164af45 09/21/2021 11:23 AM Lélio Brun

working version with additional asserts to make the axiom work

dccec723 09/20/2021 06:46 PM Lélio Brun

a version that almost work for the k-inuctive two_counters example

f51926b8 09/07/2021 04:10 PM Lélio Brun

no need to reschedule in order to "clock-protect" the unitialized state variables in ACSL !

70710795 08/25/2021 12:00 PM Lélio Brun

first draft with translated cocospec

5b98398a 07/29/2021 04:02 PM Lélio Brun

first version working with stateless contracts

f1518c7c 07/05/2021 03:42 PM Lélio Brun

more precise spec for stdout

18dada08 07/01/2021 01:56 PM Lélio Brun

working spec in the main function

d978c46e 06/30/2021 06:10 PM Lélio Brun

start instrumenting the main C function

cc852504 06/30/2021 11:21 AM Lélio Brun

comment dead code with (* XXX: UNUSED *) disclaimer

a7062da6 06/28/2021 09:52 PM Lélio Brun

another step towards refactoring

50a8778a 06/25/2021 12:35 PM Lélio Brun

refactoring first step

0406ab94 06/18/2021 06:08 PM Lélio Brun

implement optimization on spec: IT WORKS

27502d69 06/18/2021 12:35 PM Lélio Brun

add memory instances to footprint lemmas

d0f26f04 06/17/2021 07:00 PM Lélio Brun

corrections for stateless nodes

ca7ff3f7 06/17/2021 11:33 AM Lélio Brun


aaa8e454 06/16/2021 06:44 PM Lélio Brun

it works

c4780a6a 06/15/2021 05:34 PM Lélio Brun

work on new reset functions generation

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

work on spec generation almost done

9d693675 04/22/2021 03:06 PM Lélio Brun

the generation of ACSL from machine code reveal too fragile as it occurs after several transformations (eg. fusion)

efcc8d7f 04/21/2021 05:15 PM Lélio Brun

move arrow spec in its own header

186e1aef 04/21/2021 01:52 PM Lélio Brun

working proto

8d2d6fa0 04/20/2021 06:51 PM Lélio Brun

Almost works!

7f03f62d 04/16/2021 11:33 AM Lélio Brun

first version that is parsed correctly by Frama-C

4b596770 04/12/2021 05:48 PM Lélio Brun

first draft: to be tested with frama-c

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

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

fix almost all warnings

71999483 03/21/2019 05:18 PM Pierre-Loïc Garoche

Cleaning C backend - removing unused functiions
Preparing for coming ACSL

5fccce23 11/21/2018 03:23 AM Pierre-Loïc Garoche

- Dep type with a tuple has been replaced by a record type
- Modules now is more integrated and performed the building of the type/clock env.
previously some computation were performed twice by different functions. Some of these functions have been moved from compiler_common to modules

8446bf03 03/30/2018 05:54 PM Pierre-Loïc Garoche

- Makefile: solved dependency problem when compiling include lusi
- Renamed type declarations as lustre_types and machine_code_types

58a463e7 12/08/2014 09:09 PM Pierre-Loïc Garoche

Added a construct for Dependencies (was a tuple before) and a boolean attribute stateful

git-svn-id: 041b043f-8d7c-46b2-b46e-ef0dd855326e

ef34b4ae 09/02/2014 02:43 PM Xavier Thirioux

This is a major revision:
- added interface files (.lusi) in the language, that can be compiled on their own, giving an object file (.lusic) and a header file (.h)
- modular code generation, from Lustre to C level included.
- nice amount of code refactoring...

a2d97a3e 07/09/2014 09:57 AM Pierre-Loïc Garoche

Updated the licence info and header for each file.
Moved backends in separate folders

git-svn-id: 041b043f-8d7c-46b2-b46e-ef0dd855326e

af5af1e8 07/03/2014 10:46 PM Pierre-Loïc Garoche

Merged horn_traces branch

git-svn-id: 041b043f-8d7c-46b2-b46e-ef0dd855326e

01c7d5e1 07/02/2014 05:29 PM Pierre-Loïc Garoche

Prepared first stage of code reorg:
1. moved type def in
2. moved constructor and basic functions in corelang
3. Modified eexpr with prenext quantifiers

git-svn-id: 041b043f-8d7c-46b2-b46e-ef0dd855326e

d4107cf2 06/25/2014 05:37 PM Pierre-Loïc Garoche

Merged trunk updates

git-svn-id: 041b043f-8d7c-46b2-b46e-ef0dd855326e

cefc3744 06/25/2014 12:47 PM Pierre-Loïc Garoche

Specialized the prefix/postfix modifiers through functors arguments

git-svn-id: 041b043f-8d7c-46b2-b46e-ef0dd855326e

cd670fe1 06/25/2014 11:13 AM Pierre-Loïc Garoche

Split all functions of C backends in separate files

git-svn-id: 041b043f-8d7c-46b2-b46e-ef0dd855326e

13eb21df 06/25/2014 10:15 AM Pierre-Loïc Garoche

Moved c_backend in separate folder

git-svn-id: 041b043f-8d7c-46b2-b46e-ef0dd855326e