Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends @ b98a4a58

# Date Author Comment
8deaa2dd 05/05/2015 01:17 AM Teme Kahsai

do not use lusi for horn, and some logging for horn

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

14c56a07 04/08/2015 11:01 PM Xavier Thirioux

some tiny mistakes corrected...

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

ec433d69 04/08/2015 10:03 PM Xavier Thirioux

Major revision due to severe limitations and bugs of inlining capabilities:
- destination dir should now work properly
- lusic files now have a version number, to avoid nasty segfaults
when loading lusic files created by an older compiler version
- inlining should now work with generic nodes and generic array library...

0b352b14 04/04/2015 03:59 PM Xavier Thirioux

corrected various bugs in the compilation/installation Makefile.in.

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

c89faaa4 03/24/2015 09:54 PM Teme Kahsai

synch with svn

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

3a87efb8 03/24/2015 09:54 PM Teme Kahsai

fixing double printing of horn rules

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

228ebb2c 03/17/2015 08:30 AM Pierre-Loïc Garoche

Print the types

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

922ed789 03/16/2015 08:31 PM Teme Kahsai

mapping horn values to lustre values in xml format

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

b701409d 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

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

193a5ca6 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

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

99d9ac94 03/16/2015 08:30 PM Teme Kahsai

fixing double printing of horn rules

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

c7c6ef4c 03/16/2015 08:30 PM Teme Kahsai

Fixed conflict with the svn trunk version

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

3ca6d126 03/05/2015 11:48 PM Pierre-Loïc Garoche

Reactivated the generation of traceability information
Changed the test-compile to use the horn-traces and the horn-queries option

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

7d9df109 03/03/2015 09:10 PM Teme Kahsai

added invariants

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

8d4fddd8 03/03/2015 09:10 PM Teme Kahsai

including invariants

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

5cf953ec 03/03/2015 09:10 PM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex

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

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: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@380 041b043f-8d7c-46b2-b46e-ef0dd855326e

1e48ef45 12/01/2014 11:32 PM Pierre-Loïc Garoche

- Dealt with compiling lusic from distant lusi files.
- Header now do not allow the generation of function previously declared as C prototype

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

080a6d0b 09/29/2014 05:33 PM Xavier Thirioux

- corrected a bug in C code generation for multi-dimension arrays

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

b4d9710b 09/18/2014 05:25 PM Xavier Thirioux

- corrected bug in node reset clock
- cleaner (but heavier !) code generation scheme for automata

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

54d032f5 09/14/2014 08:08 PM Xavier Thirioux

- Added major feature: Lustre V6 automata !!!
- one automata example added
- changed the reset condition in node calls (now a simple bool expr)
- bug corrected in clock calculus
- bug corrected in traceability info
- added field in variables to test whether they are original...

b08ffca7 09/09/2014 06:03 PM Xavier Thirioux

- work in progress for automata...

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@333 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: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@313 041b043f-8d7c-46b2-b46e-ef0dd855326e

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

Merged horn_traces branch

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@303 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 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

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

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

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

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

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

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

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

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