| Branch: | Tag: | Revision:

# Date Author Comment
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

90cc3b8e 02/19/2021 11:19 AM Lélio Brun

some rewriting in C backend pretty-printer

1df55e58 02/16/2021 04:21 PM Lélio Brun

minor rewriting

57c96fb7 02/15/2021 02:26 PM Lélio Brun

setup tests for dune

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

fix almost all warnings

719ae9fd 02/03/2021 02:47 PM Lélio Brun

migration draft on dune

f0195e96 01/28/2020 05:26 AM Pierre-Loïc Garoche

- Primitive Tiny backend
- Renamed Mpfr to lustrec_mpfr
- Introduced dependency in Zarith. Trying to move away from Num

8d164031 12/09/2019 04:43 PM Pierre-Loïc Garoche

[MPFR] add more functions and better treatment of print output variables in main.c

04a188ec 11/21/2019 03:45 AM Pierre-Loïc Garoche

- Refactored Error exception and messages
- Bugs in partial evaluation for equalities among bool constants
and a nice recursive call generating a stack overflow! Now solved
- Setup a timeout for z3 in seal
- Better log for seal

1147e80a 11/20/2019 08:57 PM Pierre-Loïc Garoche

Array access: solved issues in C backend when basic operations in array access dimensions. Also better handling in EMF, ie further normalization through new equations

e8f55c25 11/15/2019 12:34 AM Pierre-Loïc Garoche

- tag_true and tag_false moved to lustre_types
- real constants are hidden in{i} module

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

Cleaning C backend - removing unused functiions
Preparing for coming ACSL

c3b0a8c9 03/16/2019 03:28 PM Pierre-Loïc Garoche

Merge branch 'salsa' into lustrec-seal

f0a067e9 03/15/2019 10:14 PM Pierre-Loïc Garoche

Better production of trace files.
By default traces are not produced. Requires the option -t to produce them

e8250987 11/22/2018 12:16 AM Pierre-Loïc Garoche

Unevaluation of types and clocks dimension has been already performed before producing the lusic.

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

59803095 11/16/2018 11:30 PM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal

d948c0bd 11/16/2018 04:18 AM Pierre-Loïc Garoche

math fun lib support in MPFR

ae7d913d 11/16/2018 04:18 AM Pierre-Loïc Garoche

Merlin files

c35de73b 11/15/2018 03:18 AM Pierre-Loïc Garoche

Pretty serious update:
- a bug in regressio ntest Simulink/integrator_ext_IC_matrix_test revealed the following (serious issue):
when building the list of instruction (in the machine code) the access to variable were hardcoded to LocalVar or StateVAr depending whether the variables was part of the identified memories....

0d54d8a8 11/13/2018 02:01 AM Pierre-Loïc Garoche

Removed Contract contruct: imported node should be enough. Solved some warning at compile time

b0c381d0 07/12/2018 04:04 PM Pierre-Loïc Garoche

Merge branch 'vhdl' of into lustrec-seal

1d0fd52b 05/18/2018 12:28 AM Xavier Thirioux

updated division for Horn clauses

14da5302 05/17/2018 05:08 PM Xavier Thirioux

corrected euclidean division in C code

2bb5ab71 05/17/2018 04:57 PM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal

5318ad88 05/17/2018 03:29 PM Xavier Thirioux

introduced euclidean/C-like division in C code generation

3cd040e3 05/17/2018 02:42 PM Pierre-Loïc Garoche

Issues with typing pp_basic_lib_fun

8e6cab20 05/15/2018 11:49 AM Pierre-Loïc Garoche

Tuning the pretty printing of Salsa plugin

e4edf171 04/03/2018 04:38 PM Pierre-Loïc Garoche

Zustre backend

ea8f51ae 03/30/2018 11:23 PM Pierre-Loïc Garoche

Basic library printers moved into backend specific printer files

2863281f 03/30/2018 11:14 PM Pierre-Loïc Garoche

Further restructuring:
-* to define basic builder for arrow (node, name, ...)
- machine_code_common similar to corelang but for machine_code (printers, some builders, ...)
- machine_code restricted to the translatation from normalized nodes to machines

089f94be 03/30/2018 10:43 PM Pierre-Loïc Garoche

MLI for normalization and machine_code.
Structs defining machines are now in machine_code_types

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

0bca9d53 03/15/2018 02:58 AM Pierre-Loïc Garoche

Recursive resolution of dependencies

66359a5e 01/31/2018 07:27 AM Pierre-Loïc Garoche

[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program

13aec2da 01/18/2018 05:31 PM Pierre-Loïc Garoche

[main] enum typedef in C use the original lustre filename as identifier. This commit cleans the filename to remove dots.

c80e92d1 11/09/2017 10:58 PM Pierre-Loïc Garoche

Solving a warning with ocaml 4.04 and uppercase_ascii. Provides backward compatibility for 4.02

6a078e8a 07/27/2017 10:46 PM Pierre-Loïc Garoche

C backend: solved the issue of long name in generated binaries.

f76eae4f 07/27/2017 07:44 PM Pierre-Loïc Garoche

first solution to address very large identifiers in node names, logs, and generated binaries

e7cc5186 07/18/2017 12:03 AM Pierre-Loïc Garoche

Refactor error printing.

1bff14ac 06/23/2017 06:13 PM Pierre-Loïc Garoche

- Added a field lustre_eq to machine instruction in order to record the originating lustre equation
- EMF backend now impose the optimization level to be set to 0 in order to avoid equation elimination that would render traceability difficult
- has been split into / only contains references and no functions

3ca27bc7 06/23/2017 04:07 AM Pierre-Loïc Garoche

- Addtional encapsulation of machine_code instr in a struct to enable future extension of type with more metadata.
- Improved EMF backend with META information

7ab1c5bd 06/22/2017 05:21 PM Pierre-Loïc Garoche

- Added a precision parameter for io_frontend "real" types
- New fonction in plugins: main_loop_body_prefix

990210f3 05/16/2017 04:57 PM Pierre-Loïc Garoche

Improved include folders behaviors:
- allow multiple -I dir, will be used in order (first one declared
is first used)

- when declaring a global library #open <foo>, foo is first checked
in local folders, than in global one (install path). This
does not apply to local libraries opened with #open "foo".

521e2a6b 05/16/2017 10:56 AM Pierre-Loïc Garoche

trying to improving pretty printing. Not so perfect for the moment

44686ab5 04/28/2017 08:07 PM Pierre-Loïc Garoche

Missing file c_backend_lusic

2fdbc781 04/27/2017 10:42 PM Pierre-Loïc Garoche

Cleaning output:
- no more classic display for ocamlc
- compilation warnings removed

375cbca2 04/27/2017 09:57 PM Pierre-Loïc Garoche

Merge branch 'unstable' into merge_mauve_unstable

09121c1a 04/27/2017 12:19 AM Pierre-Loïc Garoche

Merge branch 'testgen' into merging_unstable_testgen

85da3a4b 04/26/2017 11:23 PM Pierre-Loïc Garoche

Merge branch 'unstable' into merging_plugins
Non regression results were similar to master branch

5e7cecdd 04/25/2017 09:41 AM Pierre-Loïc Garoche

More informative error message in case of untyped value

4dc6ecde 04/06/2017 04:31 PM Xavier Thirioux

Deprecated function changed for compatibility with ocaml 4.04

86854b27 03/06/2017 01:43 PM David Doose

adding dealloc

7fcfaf49 03/06/2017 01:32 PM David Doose

Merge branch 'master' into mauve

80f93e0a 03/03/2017 05:12 PM Xavier Thirioux

added deallocation for dynamic memory allocation scheme

be206ad8 03/03/2017 03:32 PM David Doose

adding & in shell

08fd9ec8 03/03/2017 03:26 PM David Doose

mauve generator with annotations

d1b9423d 03/02/2017 06:12 PM David Doose

mauve generator: first shot

52c5ba00 03/01/2017 10:47 AM David Doose

adding c++ backend

042dc586 01/11/2017 10:02 AM Pierre-Loïc Garoche

Revert some ocaml code to ocaml 4.01 compatibility

dcafc99b 01/11/2017 12:28 AM Pierre-Loïc Garoche

Merge branch 'github_master' into integ_github_jan10
Intregrate all modifs by Teme et al

60f23302 01/10/2017 01:35 PM Pierre-Loïc Garoche

Merge branch 'master' of

6fa45cb6 01/10/2017 01:35 PM Pierre-Loïc Garoche

Changed the generated C file to produce input and output csv files (named inXX and outXX)

2dd3d358 12/29/2016 07:18 AM Teme Kahsai

making library statically link to horn backend

fc476249 12/28/2016 01:00 AM Teme Kahsai

adding -I options to lustrec

3b2bd83d 12/08/2016 05:37 PM Teme Kahsai

updating to onera version 30f766a:2016-12-04

bb1b5e04 09/28/2016 10:16 AM Pierre-Loïc Garoche

Ongoing work on c backend for makefile. Does not compile yet

dc893173 09/07/2016 05:38 PM Pierre-Loïc Garoche

moving C files name declaration in backend. Preparation for additional cmake target

f3d244c1 08/09/2016 10:01 PM Xavier Thirioux


45f0f48d 08/09/2016 09:31 PM Xavier Thirioux


04a63d25 08/06/2016 10:29 AM Xavier Thirioux

full merge of salsa/mpfr and master

a1daa793 02/23/2016 10:47 PM Teme Kahsai

Updated to onera_git commit version 9421e24

f0bff3e5 01/08/2016 01:41 PM Pierre-Loïc Garoche

Merge branch 'salsa' into merge_salsa_horn_2
Postponed conflicts to be solved

cf9cc6f9 01/07/2016 04:43 PM Pierre-Loïc Garoche

Introduced the opposite of Reset call: NoReset. This simplify the general compilation process and makes the code more symmetric, hence simpler and clearer code.

8eee42de 01/07/2016 04:41 PM Pierre-Loïc Garoche

Refined the dependencies in the generated makefile

bdcbb2a1 12/15/2015 05:40 PM Pierre-Loïc Garoche

Solved bug with C backend

84462531 12/15/2015 01:56 PM Pierre-Loïc Garoche

Added by default -O0

f6acf47b 11/26/2015 06:17 PM Pierre-Loïc Garoche

Plugin based framework

445e80ae 11/26/2015 05:30 PM Xavier Thirioux
53206908 11/26/2015 04:45 PM Xavier Thirioux

major branche merging salsa/mpfr with trunk

d7b73fed 11/21/2015 10:14 PM Xavier Thirioux

bug correction in typing: tuple types were computed but not recorded

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

89137ae1 11/21/2015 10:14 PM Xavier Thirioux

bug correction in typing: tuple types were computed but not recorded

55537f48 11/07/2015 11:48 PM Xavier Thirioux

bug corrected: in some cases, local const vars were assigned twice

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

da07e470 11/07/2015 11:48 PM Xavier Thirioux

bug corrected: in some cases, local const vars were assigned twice

2d179f5b 11/07/2015 07:40 PM Xavier Thirioux

numerous bugs corrected:
- bug in expansion of array accesses with constant arrays
- bug in printing complex array indexes (not C compliant)
- bug wrt C99 typing policy for constant arrays
- bug in signaling wrong useless static input

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

79614a15 11/07/2015 07:40 PM Xavier Thirioux

numerous bugs corrected:
- bug in expansion of array accesses with constant arrays
- bug in printing complex array indexes (not C compliant)
- bug wrt C99 typing policy for constant arrays
- bug in signaling wrong useless static input

e2068500 05/05/2015 01:54 AM Teme Kahsai

first commit

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

some tiny mistakes corrected...

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

4f4a77a4 04/08/2015 11:01 PM Xavier Thirioux

some tiny mistakes corrected...

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