Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src @ 6560bb94

# Date Author Comment
6560bb94 03/06/2014 04:33 PM Xavier Thirioux

first steps towards struct types...

9bdfc99f 03/06/2014 03:39 PM Xavier Thirioux

corrected bug in arrow macros names, added storage attribute for static alloc macros, option -d now creates the destination directory if needed, with current dir as file permissions

c6acbdaa 03/05/2014 04:32 PM Xavier Thirioux

answer to #feature 50:
- arrows are now factorized out and become part of include
as files arrow.h and arrow.c
- no more arrows in generated code
- compiling and linking arrow.c is only necessary
in case of dynamic allocation
- version now includes installation prefix (for the standard lib)...

6bab3787 03/05/2014 02:35 PM Xavier Thirioux

In order to export any type of constants, moved type definitions from .c to .h

b3202935 03/04/2014 02:41 PM Eric Noulard

Generate extern declarations for constant as well.

c518d082 03/01/2014 03:37 PM Xavier Thirioux

- added generation of clock information in interface (.lusi) files
- added clock checking between interface and implementation files

2842f7ca 03/01/2014 12:01 AM Pierre-Loïc Garoche

Reenabled the generation of witnesses for inline process.
Systematic use of the build path

8b3afe43 02/28/2014 04:56 PM Xavier Thirioux

- merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
for types (not yet for clocks)

29ad4531 02/28/2014 03:28 PM Pierre-Loïc Garoche

Merge back horn backend branch in trunk

64aa99c4 02/28/2014 02:05 PM Pierre-Loïc Garoche

Merge trunk modif in branch

addb1a3a 02/28/2014 02:04 PM Pierre-Loïc Garoche

desome

49b32cb6 02/28/2014 01:52 PM Pierre-Loïc Garoche

Merge inlining branch within trunk.
The test target requires branch lustrec/horn as binary lustreh.

274c72ec 02/28/2014 01:43 PM Pierre-Loïc Garoche

inliner function

b63536a0 02/28/2014 10:39 AM Pierre-Loïc Garoche

Minor bugs

ae78dfee 02/28/2014 10:35 AM Eric Noulard

Do not use stable sort because it requires recent ocamlgraph
library (1.8.3) which is not widely available in distro repository.
Moreover "stable" sort is not necessary, sort will do.
Fixes Issue #49: https://cavale.enseeiht.fr/redmine/issues/49

c02d255e 02/28/2014 10:33 AM Pierre-Loïc Garoche

Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency of the inlining process

06fa8b5e 02/26/2014 03:37 PM Xavier Thirioux

better error message for tuple type mismatch

fbda2f96 02/26/2014 02:37 PM Xavier Thirioux

again, debugged tuple subtyping

45ca90f5 02/26/2014 02:04 PM Xavier Thirioux

removed debug printing

1cb216b4 02/26/2014 02:02 PM Xavier Thirioux

corrected wrong subtyping rule for tuple assignment

b580c8f8 02/26/2014 01:42 PM Xavier Thirioux

added subtyping in equations (rhs may be a subtype of lhs)

b8ae1bbc 02/26/2014 07:48 AM Pierre-Loïc Garoche

Improvements as suggested by e. Noulard: better install of include; modified generated makefile

9334747d 02/24/2014 04:26 PM Pierre-Loïc Garoche

Fixed bug on the main part

3e209698 02/24/2014 11:47 AM Pierre-Loïc Garoche

First fully working version of horn backend.

Has to be called with "-horn -node main_node"

The test script compute the smt2 file and calls z3 on them.

3a60ec17 02/24/2014 11:25 AM Pierre-Loïc Garoche

...

4f3cc9f3 02/24/2014 10:50 AM Pierre-Loïc Garoche

Is it working?

c0003810 02/24/2014 09:46 AM Pierre-Loïc Garoche

Working on bugs

40f8d0f9 02/21/2014 05:11 PM Pierre-Loïc Garoche

Second (almost) working version

faa5e5c5 02/21/2014 04:39 PM Pierre-Loïc Garoche

First (almost) working version

fc7a01ce 02/21/2014 12:42 PM Pierre-Loïc Garoche

Ongoing ...

23bdf881 02/21/2014 12:38 PM Pierre-Loïc Garoche

Ongoing ...

04a7df69 02/21/2014 08:37 AM Pierre-Loïc Garoche

In the middle of the coding process. Just pushing thinks

aa6b7d46 02/20/2014 06:45 AM Pierre-Loïc Garoche

The missing file

f6923c9e 02/19/2014 05:02 PM Pierre-Loïc Garoche

Initial copy of the horn output version. Not really working yet

f485f585 11/14/2013 12:15 PM Pierre-Loïc Garoche

- Renamed the only target of the generated makefile
- Solved bug: xor are now printed as bitwise xor in c : a ^ b and not a xor b.

b878abe5 11/12/2013 11:20 PM Xavier Thirioux

- work in progress for interface typing

accbb04d 11/07/2013 07:03 PM Xavier Thirioux

- small bug correction in dimension typing
- #open keyword instead of open
- dummy generic matrix/vector library interface added
- modified examples according to the new syntax

f22632aa 10/22/2013 10:39 AM Pierre-Loïc Garoche

Merge (if it works) of the lustre interfaces branche providing lusi files into trunk

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

Moved files to trunk in lustre_compiler