Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

# Date Author Comment
6d1693b9 06/14/2021 07:06 PM Lélio Brun

work on spec generation almost done

9e277169 06/04/2021 10:09 AM Lélio Brun

forgotten file

6cbbe1c1 06/03/2021 04:44 PM Lélio Brun

start again with spec representation

75c459f4 05/04/2021 06:24 PM Lélio Brun

start with Spec AST generation

f69e7ea2 05/04/2021 10:58 AM Lélio Brun

add -O -1 flag to disable fusion of conditionals

7a1b2819 05/04/2021 10:26 AM Lélio Brun

missing file

7ee5f69e 05/04/2021 10:20 AM Lélio Brun

corrections on loggers + spec in AST

dfce5630 04/26/2021 05:12 PM Lélio Brun

patch de Xavier pour réparer -O 3

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)

ed1ff359 04/21/2021 06:09 PM BRUN Lelio

Update .gitlab-ci.yml file

8060f89a 04/21/2021 06:01 PM Lélio Brun

forgotten file

d8144228 04/21/2021 05:55 PM BRUN Lelio

Update .gitlab-ci.yml file

eb557ef7 04/21/2021 05:49 PM BRUN Lelio

Update .gitlab-ci.yml file

a230aa0a 04/21/2021 05:39 PM BRUN Lelio

Update .gitlab-ci.yml file

3e74e89b 04/21/2021 05:39 PM BRUN Lelio

Update .gitlab-ci.yml file

9f0cd2c4 04/21/2021 05:38 PM BRUN Lelio

Update .gitlab-ci.yml file

66284cfb 04/21/2021 05:22 PM BRUN Lelio

Update .gitlab-ci.yml file

1802e98c 04/21/2021 05:21 PM BRUN Lelio

Update .gitlab-ci.yml file

561a028e 04/21/2021 05:16 PM Lélio Brun

update CI

383a7762 04/21/2021 05:15 PM Lélio Brun

Merge branch 'master' of gitlab.isae-supaero.fr:l.brun/lustrec

efcc8d7f 04/21/2021 05:15 PM Lélio Brun

move arrow spec in its own header

dcbc211b 04/21/2021 04:40 PM BRUN Lelio

Update .gitlab-ci.yml file

d62bba1b 04/21/2021 04:36 PM BRUN Lelio

Update .gitlab-ci.yml file

18f496c5 04/21/2021 02:55 PM BRUN Lelio

Update .gitlab-ci.yml file

c5537f80 04/21/2021 02:10 PM BRUN Lelio

Update .gitlab-ci.yml file

de5eaf78 04/21/2021 02:01 PM BRUN Lelio

Update .gitlab-ci.yml file

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

2756319f 03/29/2021 11:12 AM Lélio Brun

messages d'erreurs terminés

e78eb9f5 03/25/2021 06:23 PM Lélio Brun

more error messages

78013d1e 03/19/2021 03:11 PM Lélio Brun

more error messages

91e96bd8 03/18/2021 04:32 PM Lélio Brun

some more error messages

a2327c71 03/10/2021 05:22 PM Lélio Brun

start to write error messages

90e83deb 03/09/2021 01:20 PM Lélio Brun

prepare for the modern error handling of Menhir

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

b20c1e19 02/19/2021 11:21 AM Lélio Brun

Merge branch 'dune'

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

971a4d81 02/16/2021 12:33 PM Lélio Brun

missing header files in dune install targets

ac6ce5a1 02/15/2021 02:59 PM Lélio Brun

disable tests in gitlab CI

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

setup tests for dune

97d4e95e 02/08/2021 10:23 AM Lélio Brun

add gmp dep

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

fix almost all warnings

3dfb5cd8 02/05/2021 02:36 PM Lélio Brun

rewrite a bit the menhir parser

b9e707e8 02/03/2021 03:36 PM Lélio Brun

forgot to generate opam file

3daa3cc3 02/03/2021 03:31 PM Lélio Brun

missing dune-site dep

e60a3711 02/03/2021 03:27 PM Lélio Brun

missing zarith dep

d88b417f 02/03/2021 03:01 PM Lélio Brun

try to fix ci

66b7c74d 02/03/2021 02:57 PM Lélio Brun

isae gitlab version does not support parallel jobs matrices

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

migration draft on dune

b43b8eb5 01/26/2021 10:11 AM Pierre-Loic Garoche

add thread dependency required by z3 lib

7332c335 01/21/2021 10:56 AM Lélio Brun

Merge remote-tracking branch 'origin/unstable'

0b7cffef 01/21/2021 10:27 AM BRUN Lelio

master creation

ef598ac3 11/17/2020 04:38 PM Pierre-Loïc Garoche

moved from Num to Zarith. IMpacted main.ml ad uses of Z3 in zustre_cex and seal-extract

e1f49bdb 07/16/2020 10:09 AM Xavier Thirioux

work in progress for ACSL support

8c36178f 07/09/2020 03:33 PM Pierre-Loïc Garoche

Merge branch 'lustrec-seal' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal

58fd528a 07/09/2020 03:27 PM Pierre-Loïc Garoche

Added some missing locations in tiny plugin

3e039a34 07/02/2020 03:32 PM Pierre-Loïc Garoche

Tiny: solved issue with a change in the Location.dummy signature

af49e9a4 03/12/2020 11:26 AM Xavier Thirioux

forgotten to uodate log.ml

574c671b 03/12/2020 11:21 AM Xavier Thirioux

1) log messages are now flushed. 2) very long computation times due to naive code to check for unused variables are now much shorter

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

2120af73 01/27/2020 07:00 PM Pierre-Loïc Garoche

[bug cavale 93] solved: issue when resetting a stateless node. Now generating a warning and forcing the stateful status. Could be improved to remove the reset statement. (TODO)

a0c92fa8 01/27/2020 04:24 PM Pierre-Loïc Garoche

printing nodes + more progress on seal export

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

4e9ba094 12/09/2019 04:42 PM Pierre-Loïc Garoche

temporary changed in the expression printer

c4521397 12/09/2019 09:53 AM Pierre-Loïc Garoche

preserving types/clocks when possible

f3574a72 11/21/2019 03:49 AM Pierre-Loïc Garoche

Moved some code

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

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

Commenting out unused variables

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

c2db420f 11/20/2019 05:09 PM Pierre-Loïc Garoche

comment some code to avoid warning at compile time

9b2c037f 11/20/2019 04:42 PM Pierre-Loïc Garoche

solved bug 91 on cavale: spurious commas in emf backend

490f1952 11/20/2019 04:38 PM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal

94a9e2c3 11/20/2019 04:10 PM Pierre-Loïc Garoche

better location error

60fbbbd9 11/19/2019 06:32 AM Pierre-Loïc Garoche

Optimize_machine
- Constants were improperly unfolded
- Do not unfold clock definition

b309c9b7 11/18/2019 05:25 PM Pierre-Loïc Garoche

big: missing case with substituting expressions

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 Real.ml{i} module

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

[seal] more progress on seal extract

720c7244 11/15/2019 12:33 AM Pierre-Loïc Garoche

sort of slicing for machine code

7075d9fc 11/15/2019 12:32 AM Pierre-Loïc Garoche

kind2 option for printing expressions

8df40160 11/15/2019 12:27 AM Pierre-Loïc Garoche

Reactivated Unfold constant

2d2d89d7 11/15/2019 12:25 AM Pierre-Loïc Garoche

partial evaluation for basic lib

de8e9811 11/15/2019 12:02 AM Pierre-Loïc Garoche

Module to manipulate real constants. For the moment we Num

3066247f 11/14/2019 05:56 PM Pierre-Loïc Garoche

cleaning debug logs

e47138b8 11/14/2019 05:56 PM Pierre-Loïc Garoche

reactivating the unfolding of constants

2db953dd 11/14/2019 05:55 PM Pierre-Loïc Garoche

flatten dependencies in schedule to make sure all required equations are used

8a11dc80 11/14/2019 05:54 PM Pierre-Loïc Garoche

cleaning debug logs

ab8388cf 11/06/2019 10:19 AM Pierre-Loïc Garoche

[emf] added the names of the cocospec properties in the output json

e6b644f4 11/06/2019 07:53 AM Pierre-Loïc Garoche

better negation of constants

51aef490 11/05/2019 12:11 AM Pierre-Loïc Garoche

Better treatment of arrays in EMF backend. Be careful it may have changed the way enum types are declared

0323b9e6 07/18/2019 09:38 PM Pierre-Loïc Garoche

More kind2 outputs: clocked fun call + clocked and restart fun call

73a4995a 07/18/2019 09:02 AM Pierre-Loïc Garoche

seal: now deals with enum

ff61a638 07/18/2019 07:52 AM Pierre-Loïc Garoche

when condition in kind2 printer

3b007718 07/18/2019 07:39 AM Pierre-Loïc Garoche

EMF backend issue

72a93147 07/17/2019 11:12 PM Pierre-Loïc Garoche

seal: stateless systems

1d3f2f66 07/17/2019 07:40 PM Pierre-Loïc Garoche

every in kind2 syntax

ae08b9fc 07/17/2019 07:30 PM Pierre-Loïc Garoche

[seal] delt with Merge and when
[printer] more kind2 syntax