CristalCaveGem » LustreC

fix handling of state variables in spec expressions

fix bug where singleton tuples were generated

fix offline tests

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

fix tests procedure

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

working version for stateful contracts

proper generation of stateful contracts

proper handling of stateless nodes and automata

proper inductive case and no code generated for contracts

working version with additional asserts to make the axiom work

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

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

first draft with translated cocospec

first version working with stateless contracts

more precise spec for stdout

working spec in the main function

start instrumenting the main C function

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

another step towards refactoring

refactoring first step

implement optimization on spec: IT WORKS

add memory instances to footprint lemmas

corrections for stateless nodes

reformatting

it works

work on new reset functions generation

work on spec generation almost done

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

move arrow spec in its own header

working proto

Almost works!

first version that is parsed correctly by Frama-C

first draft: to be tested with frama-c

generic ACSL spec generation

start generating ACSL spec

fix almost all warnings

Cleaning C backend - removing unused functiions
Preparing for coming ACSL

- 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

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

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

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@380 041b043f-8d7c-46b2-b46e-ef0dd855326e

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...

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

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@313 041b043f-8d7c-46b2-b46e-ef0dd855326e

Merged horn_traces branch

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@303 041b043f-8d7c-46b2-b46e-ef0dd855326e

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

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/specification_reorg_corelang_parser@297 041b043f-8d7c-46b2-b46e-ef0dd855326e

Merged trunk updates

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/specification_acsl_new_backend@288 041b043f-8d7c-46b2-b46e-ef0dd855326e

Specialized the prefix/postfix modifiers through functors arguments

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/cleaner_backend@281 041b043f-8d7c-46b2-b46e-ef0dd855326e

Split all functions of C backends in separate files

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/cleaner_backend@280 041b043f-8d7c-46b2-b46e-ef0dd855326e

Moved c_backend in separate folder

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/cleaner_backend@278 041b043f-8d7c-46b2-b46e-ef0dd855326e