Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec @ 5538b7ac

# Date Author Comment
5538b7ac 03/17/2014 12:17 AM Xavier Thirioux

Added declaration/definition of stateless/stateful nodes.
The 'function' keyword is for stateless nodes only,
the 'node' keyword is any kind of node.
Improves compilation and paves the way for more optimizations.

d3e4c22f 03/14/2014 05:45 PM Xavier Thirioux

- work in progress for stateless/stateful status computation
(to turn conditionals into merges, which yield more efficient C code)

2ea1e4a6 03/13/2014 05:30 PM Xavier Thirioux

corrected bugs in clock generalization that produced pessimistic C code (not wrong though); corrected bug with node importation policy wrt (re)declaration, (re)definition...

6affc9f5 03/11/2014 03:41 PM Xavier Thirioux

- added struct types declaration
- added constant definition with a struct type
- added checking for multiple definitions of nodes (behavior was buggy)
- better and more uniform error messages
for undefined/already defined symbols

We still need struct expressions...
51768260 03/10/2014 05:56 PM Xavier Thirioux

work in progress for struct types...

aa223e69 03/10/2014 09:55 AM Xavier Thirioux

more steps towards struct types...
Cette ligne, et les suivantes ci-dessous, seront ignorées--

M trunk/src/corelang.mli
M trunk/src/type_predef.ml
M trunk/src/main_lustre_compiler.ml
M trunk/src/types.ml
M trunk/src/printers.ml
M trunk/src/typing.ml...

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.

3e79b3a5 03/01/2014 03:38 PM Xavier Thirioux

- stupid svn had removed a file, again

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

626e6f03 02/28/2014 11:59 PM Pierre-Loïc Garoche

Updated script. Does not seem to be fully functional yet.

3e36d4e0 02/28/2014 11:59 PM Pierre-Loïc Garoche

Added default ensures statements

7f611a35 02/28/2014 05:09 PM Xavier Thirioux

- added dummy_lib.lusi (accidentally removed !?)

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

f1da5111 02/24/2014 04:47 PM Pierre-Loïc Garoche

Updated version of test script: timeout for z3

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

Fixed bug on the main part

433b1e6b 02/24/2014 11:48 AM Pierre-Loïc Garoche

Cleaning useless files

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

3a9e1fe8 02/21/2014 05:34 PM Pierre-Loïc Garoche

Manually corrected version of ex3. Should integrate the modifications

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

7bc15356 02/05/2014 03:03 PM Pierre-Loïc Garoche

lego robot example

ed226e0d 11/25/2013 10:39 AM Xavier Thirioux

missing dummy lib for arrays

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

fdeaac38 10/22/2013 10:01 AM Pierre-Loïc Garoche

Lustre interfaces: lusi files are generated and used. Remaining work: create a good makefile and add the appropriate #include, fix issues with Arnaud's benchmarks (old syntax)

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

Moved files to trunk in lustre_compiler

0f649de9 10/02/2013 08:05 AM Pierre-Loïc Garoche

Moved files to trunk in lustre_compiler