Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec @ e8250987

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

95944ba1 11/21/2018 11:53 PM Pierre-Loïc Garoche

Cleaning up stuff in normalization. Mainly replace arguments with only required elements
node_Table hashtbl is now only available through functions of the corelang.mli

684d39e7 11/21/2018 09:19 PM Pierre-Loïc Garoche

Moved lusic to .h printer after normalizing in case we want one day to produce ACSL from a normalized spec
Trying also to extend the parser to deal with imported nodes....

217837e2 11/21/2018 08:15 PM Pierre-Loïc Garoche

Unified compilation of lusi and lus files
Different parsers yet but shared process.
In case of lusi input the C backend is bypassed since the .h is generated from the lusic and no C code should be generated since it may overwrite existing manually written code...

19a1e66b 11/21/2018 05:58 AM Pierre-Loïc Garoche

Added include directive that directly inject a lustre source file in the prog

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

f9f06e7d 11/20/2018 11:21 PM Pierre-Loïc Garoche

- Module.load_header and load_program were merged.
- Contract were extended with list of statements.

a4158a4b 11/20/2018 11:20 PM Pierre-Loïc Garoche

Added back the gitbranch option ins configure.ac. Was wrongly removed in the release process

32bafa6f 11/20/2018 11:20 PM Pierre-Loïc Garoche

Some thoughts about lusic

7f2309bc 11/20/2018 07:02 PM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal

95b507a8 11/17/2018 07:18 AM Pierre-Loïc Garoche

Merge branch 'master' of https://cavale.enseeiht.fr/git/lustrec

a7ce880f 11/17/2018 07:17 AM Pierre-Loïc Garoche

Initiating nwew version 1.7 Xia/Huai

531c07e4 11/17/2018 06:46 AM Pierre-Loïc Garoche

Cleaning git references for release

efe57954 11/17/2018 06:37 AM Pierre-Loïc Garoche

Recording the opam file

690eb3a5 11/17/2018 06:30 AM Pierre-Loïc Garoche

Preparing release 1.6 Xia/Zhui

b2b2ac74 11/17/2018 06:26 AM Pierre-Loïc Garoche

Merge branch 'master' into unstable

fb716d2c 11/17/2018 06:07 AM Pierre-Loïc Garoche

Some autoconf update

e491c34a 11/17/2018 01:56 AM Pierre-Loïc Garoche

Issues with linking Z3 on OSX

51106b7e 11/16/2018 11:31 PM Pierre-Loïc Garoche

Fixing issues with changes in machine code

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

Merge branch 'unstable' into lustrec-seal

673bf87c 11/16/2018 07:56 PM Pierre-Loïc Garoche

Num module for mli

ce0f282d 11/16/2018 07:54 PM Pierre-Loïc Garoche

Num is a package in recent ocaml

1a05d45a 11/16/2018 07:19 AM Pierre-Loïc Garoche

Cleaning warning in mpfr

3ea2599d 11/16/2018 06:42 AM Pierre-Loïc Garoche

No more uses of kind files

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

45d53dc3 11/16/2018 02:46 AM Pierre-Loïc Garoche

EMF export of local type definition (for simple types)

4c3c6658 11/16/2018 12:46 AM Pierre-Loïc Garoche

mutation bug solved: improper access to an element of an empty list of bindings

a879351b 11/16/2018 12:44 AM Pierre-Loïc Garoche

Printers bug solved: now properly printing lustre file as open/types/other decls

5c3b45a0 11/15/2018 08:23 PM Pierre-Loïc Garoche

Lustre test gen mutation: bug solved. The path to the installation was hardcoded.

c95a441d 11/15/2018 08:22 PM Pierre-Loïc Garoche

Bug solved in MCDC generation: Some annotations generated were producing problems

bc3139b0 11/15/2018 08:21 PM Pierre-Loïc Garoche

Print the spec within the node

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

05ca2715 11/15/2018 03:16 AM Pierre-Loïc Garoche

Moved back mpfr to its folder. Previsouly there was two competing files :(

307c32f5 11/14/2018 06:13 PM Pierre-Loïc Garoche

MPFR bug solved: typing of function argument was not properly building tuples of types.

6de6bcf4 11/13/2018 04:16 PM Pierre-Loïc Garoche

Improved configure.ac

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

34d3f022 11/12/2018 11:43 PM Pierre-Loïc Garoche

Further processing of contract in the typing. More to go

0d79d0f3 11/12/2018 02:06 AM Pierre-Loïc Garoche

First working version of switched system extraction for seal tool

1cc047f9 11/10/2018 02:07 PM Pierre-Loïc Garoche

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

a5dc55ca 11/09/2018 07:43 AM Pierre-Loïc Garoche

Restructuring code in SEAL

82906771 11/08/2018 03:58 PM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal

1c9625b4 11/08/2018 03:46 PM Pierre-Loïc Garoche

Merge branch 'cocospec_to_be_merged' into unstable
Mainly adapting to new cocospec syntax for contracts

73ccaf2f 11/08/2018 03:29 PM Pierre-Loïc Garoche

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

ec8fc65e 11/08/2018 09:53 AM Pierre-Loïc Garoche

configure.ac tuning

a742719e 11/08/2018 09:12 AM Pierre-Loïc Garoche

SEAL: compute the projection to switched systems. Some issues with intermediate variables and a better selection of split guard have to be addressed

7c8a7647 11/08/2018 09:11 AM Pierre-Loïc Garoche

log new option to mention plugin or module

eb9a8c3c 11/04/2018 07:00 AM Pierre-Loïc Garoche

Moved find_eq from Machine_code to Corelang and sort_eqs from Machine_code to Scheduling

a703ed0c 11/03/2018 12:03 AM Pierre-Loïc Garoche

Preprocess the selected node in seaL BACKEND: focus on memories and perform node slicing.

95fb046e 10/24/2018 01:33 PM Pierre-Loïc Garoche

Scheduling of node equations is now attached to machine type

365d1b07 10/24/2018 01:31 PM Pierre-Loïc Garoche

Moved definition of graph modules from Causality to Utils to avoid cyclic deps

99cb0623 10/19/2018 12:32 AM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal

2d27eedd 10/08/2018 04:52 PM Pierre-Loïc Garoche

- Global type env and clock env now availble as a global reference (Global module)
- Adapted the parsing of specification with a cocospec compatible one
- The data structure of contracts is now almost cocospec compatible
- Lustrec-test has been updated to use the newest syntax

778c80fd 10/05/2018 07:54 PM Pierre-Loïc Garoche

Some refactoring
Adapted the parser/types/constructors for cocospec syntax

8fa4e28e 09/25/2018 11:23 AM Pierre-Loïc Garoche

[bug solved] do not normalize eexpr in annotations, only in specification.

987fa573 09/25/2018 10:16 AM Pierre-Loïc Garoche

Merge branch 'git-configure' into cocospec

3471cb4d 09/25/2018 10:12 AM Pierre-Loïc Garoche

Better management of git branch in configure.ac

949b2e1e 09/24/2018 02:18 PM Pierre-Loïc Garoche

Normalizing eexpr

1569a55a 09/21/2018 03:25 PM Pierre-Loïc Garoche

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

27446b88 09/14/2018 06:02 PM Pierre-Loïc Garoche

Improving connection with CDash

e82e03c6 09/14/2018 04:32 PM Christophe Garion

doc: add HTML grammar file

57392da1 09/14/2018 10:43 AM Christophe Garion

solve error in lexer introduced by previous merge

3b5419a8 09/14/2018 10:36 AM Christophe Garion

finishing solving strange conflicts for merge...

4f26dcf5 09/13/2018 03:36 PM Pierre-Loïc Garoche

Renamed annots into contracts. Preparing for syntax extension

17e1d0f4 09/13/2018 03:14 PM Pierre-Loïc Garoche

- Removed the kind2 file (parser/lexer/types)
- Cleaned a little bit our parser: removal of old prelude constructs

f09146ae 09/13/2018 02:58 PM Christophe Garion

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

37d3e0eb 09/13/2018 01:55 PM Pierre-Loïc Garoche

Cocospec discussions in the TODO.org

e4811e4c 08/04/2018 12:58 AM Bourbouh

add more conversion libraries

239f4429 07/24/2018 03:05 AM Bourbouh

fix rem and mod

8be49798 07/24/2018 02:39 AM Bourbouh

Merge branch 'master' of https://cavale.enseeiht.fr/git/lustrec

4d841db7 07/24/2018 02:38 AM Bourbouh

add tanh

d0d8fe27 07/13/2018 11:34 PM Pierre Loic Garoche

Updating dependencies in the READ:E

d7e89c59 07/13/2018 08:25 PM Pierre-Loïc Garoche

Merge branch 'master' into unstable

88df55b3 07/13/2018 08:25 PM Pierre-Loïc Garoche

Merge branch 'merge' into unstable

de041ec0 07/13/2018 08:21 PM Pierre-Loïc Garoche

Update the configure to prepare the next release 1.6 Xia/Zhu

83dc064f 07/13/2018 08:05 PM Pierre-Loïc Garoche

Byte/String bug reappeared

f9d0c175 07/13/2018 07:52 PM Pierre-Loïc Garoche

Merge branch 'master' of https://cavale.enseeiht.fr/git/lustrec

c1c4263c 07/13/2018 07:44 PM Pierre-Loïc Garoche

Preparing release of 1.5 Xia/Shao Kang

681f591b 07/13/2018 07:39 PM Pierre-Loïc Garoche

Preparing release 1.6 Xia/Zhu

2d2144c0 07/13/2018 05:18 PM Pierre-Loïc Garoche

Solved bug#57: issues when indirect init of a pre in horn-traces

bc9fd714 07/12/2018 07:35 PM Pierre-Loïc Garoche

Temporily disabling Mehnir as a parser.

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

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

fbc571e6 07/04/2018 04:06 PM Arnaud Dieumegard

Refactoring of vhdl data types

7d77632f 06/22/2018 06:24 PM Pierre-Loïc Garoche

Added two fresh vars counter and uid.
uid is a list of integer denoting the specific instance of a stateful/stateless node.

57d61d67 06/22/2018 11:24 AM Pierre-Loïc Garoche

New option to select github version of Z3
Added Yojson dependency in lustrev
Some progress on Cex generation

fae1790f 06/21/2018 05:42 PM Arnaud Dieumegard

Added support for Process statements, signal assignment, If, Exit and Null sequential statements

d77323b8 06/15/2018 05:45 PM Arnaud Dieumegard

Added postprocessing for numeric literals

55963629 06/12/2018 05:10 PM Arnaud Dieumegard

Ongoing work on json vhdl to vhdl structure conversion

998766b4 06/11/2018 09:37 PM Pierre-Loïc Garoche

missing file

4300981b 06/11/2018 06:44 PM Pierre-Loïc Garoche

Zustre: timeout and slicing

31027df4 06/08/2018 06:45 PM Xavier Thirioux

updated luster lexer ??

dea84f9e 06/01/2018 05:23 PM Pierre-Loïc Garoche

Working example!

8f9ce6d4 06/01/2018 04:15 PM Pierre-Loïc Garoche

Pom pom pom

5daedd81 06/01/2018 04:14 PM Pierre-Loïc Garoche

Sample value for VHDL

3ca452f3 06/01/2018 04:12 PM Pierre-Loïc Garoche

Main lustrei

090baab6 06/01/2018 10:02 AM Pierre-Loïc Garoche

Compiling - while doing nothing :)

91cc0f70 06/01/2018 09:32 AM Pierre-Loïc Garoche

Bootstrapping VHDL importer/exporter

0bd19a92 05/31/2018 04:39 PM Xavier Thirioux

bug wrt normalization. Didn't take clock into account.

bec3cf3d 05/31/2018 04:35 PM Xavier Thirioux

strange bug (ill-typed source) wrt Bytes/String conversion

cff64531 05/31/2018 04:33 PM Xavier Thirioux

bug in CSE, was disregarding clock