| Branch: | Tag: | Revision:

lustrec @ 93119c3f

# Date Author Comment
93119c3f 09/21/2017 01:48 PM Pierre-Loïc Garoche

Moved stateflow tool in src/tool
Updated the makefile to compile lustresf
Not working yet

cb781911 09/15/2017 02:19 PM Pierre-Loïc Garoche

Missing readme file in the import

2de7fa82 09/15/2017 02:16 PM Pierre-Loïc Garoche

Initial import of stateflow_cps_semantics (github)

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

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

0a10042e 07/27/2017 10:43 PM Pierre-Loïc Garoche

Normalization: force normalization of "every" arguments

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

8f0e9f74 07/21/2017 08:48 PM Pierre-Loïc Garoche

[EMF] improved feedback on reset calls

714bb286 07/20/2017 10:21 PM Pierre-Loïc Garoche

Merge branch 'dynamic_inlining' into unstable

264a4844 07/20/2017 10:20 PM Pierre-Loïc Garoche

First working version of algebraic loop resolution. Disabled by default.

12c62417 07/18/2017 10:07 PM Pierre-Loïc Garoche

[EMF} missing brace

9f158b2b 07/18/2017 10:01 PM Pierre-Loïc Garoche

[EMF] missing quotes

23ce017b 07/18/2017 09:59 PM Pierre-Loïc Garoche

Ongoing work

e1ef00d0 07/18/2017 05:19 PM Pierre-Loïc Garoche

Merge branch 'unstable' into dynamic_inlining

568b5a26 07/18/2017 09:24 AM Pierre-Loïc Garoche

[EMF] improved alignement of braces + solved (naother) bug in shortening of ids

333f42fd 07/18/2017 06:15 AM Pierre-Loïc Garoche

[EMF] more hash

049f3b17 07/18/2017 05:15 AM Pierre-Loïc Garoche

Merge branch 'unstable' of into unstable

329774de 07/18/2017 05:14 AM Pierre-Loïc Garoche

[EMF] bug solved, some ids were not hashed

714588bf 07/18/2017 01:59 AM Bourbouh

ange ID length

def94a59 07/18/2017 12:42 AM Pierre-Loïc Garoche


9f231bff 07/18/2017 12:37 AM Pierre-Loïc Garoche

[EMF] simplify branches with single case as regular instructions

43b5fabc 07/18/2017 12:09 AM Pierre-Loïc Garoche

[EMF] Disable join of guards in EMF backend

9094307a 07/18/2017 12:04 AM Pierre-Loïc Garoche

Working on algebraic loop diagnostic and resolution

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

Refactor error printing.

fbad3c4b 07/14/2017 11:02 PM Pierre-Loïc Garoche

[EMF] protect machine names

69c8d06c 07/14/2017 10:51 PM Pierre-Loïc Garoche

[EMF] protect more field

785b64f9 07/14/2017 07:32 AM Pierre-Loïc Garoche

[EMF] Protecting print of names to ensure a length < 50. Remove the middle part of the string and inject a hash of it.

40ad675e 07/14/2017 06:32 AM Pierre-Loïc Garoche

A math library for some functions used in Simulink

30f46c0c 07/14/2017 06:30 AM Pierre-Loïc Garoche

Renamed math lib into lustrec_math to avoid conflicting calls to <math.h>

212d6eff 07/13/2017 06:40 PM Pierre-Loïc Garoche

[HORN] handled asserts in stateless node step rule definition

07ceae4c 07/13/2017 05:47 PM Pierre-Loïc Garoche

[HORN] Protect names of stateless nodes with a _fun suffix. This was conflicting with existing names in Z3, ie. "abs".
[HORN] Better treatment of stateless nodes collecting semantics
Fixes issue #13 on github:

7352a936 07/13/2017 08:41 AM Pierre-Loïc Garoche

Addressing node calls in asserts

ef8a361a 07/13/2017 01:00 AM Pierre-Loïc Garoche

Provides type compatible with Matlab types in EMF backend

01b501ca 07/12/2017 09:06 PM Pierre-Loïc Garoche

[EMF backend] Merging branches

13507742 07/12/2017 09:06 PM Pierre-Loïc Garoche

Refactored some code: optimization of machine

1b721bfd 07/11/2017 08:09 AM Pierre-Loïc Garoche

bug fixed: Inputs for branches solved

2823bc51 07/11/2017 01:16 AM Pierre-Loïc Garoche

Proper integer index for enumerated branches

c82ea2ca 07/11/2017 01:07 AM Pierre-Loïc Garoche

Enumerated datatypes as integer

2475c9e8 07/10/2017 11:43 PM Pierre-Loïc Garoche

Refactored EMF backend. Handle now the call to existing math and conv libraries

dd71e482 07/10/2017 06:52 PM Pierre-Loïc Garoche

EMF backend: each branch provides the inputs and outputs

017eec6a 07/10/2017 06:04 PM Pierre-Loïc Garoche

Renamed ISet of Machine_code to VSet: was sets of variable and was conflicting with ISet from Utils which carries strings.

a6b58a46 07/10/2017 05:14 PM Bourbouh

Merge branch 'unstable' of into unstable

ab1c9ed2 07/10/2017 05:03 PM Bourbouh

small modifs in EMF format

27d18db9 07/08/2017 05:29 PM Pierre-Loïc Garoche

Branchs output in EMF is only the intersection of each branch defined flows

9f0f88dd 07/07/2017 10:53 PM Pierre-Loïc Garoche

Full rewrite of EMF backend.

3436d1a6 07/07/2017 10:52 PM Pierre-Loïc Garoche

New global option to normalize simple call to std lib functions (+,-,*, comparison ops, etc).
This is used in EMF backend.

524060b3 07/07/2017 07:11 AM Pierre-Loïc Garoche

Ongoin work on EMF backend. Commit to store a working version. More work to do on clocks and resets

27dc3869 07/04/2017 01:22 AM Pierre-Loïc Garoche

Added a feature to alias ite contructs argument. To be used by EMF backend

fa880262 07/04/2017 01:21 AM Pierre-Loïc Garoche

Bug solved: lusic dependency of mpfr

7629d67b 07/03/2017 08:45 PM Pierre-Loïc Garoche

Bug solved in include dependencies in install target

145379a9 06/30/2017 06:58 PM Pierre-Loïc Garoche

Improved EMF backend. Working on the whole fmcad suite

397d5ae3 06/27/2017 06:36 PM Pierre-Loïc Garoche

Copied Printers.pp_expr functions to Horn backend to escape < and > in XML traces output

c9043042 06/27/2017 12:22 AM Pierre-Loïc Garoche

Issues with Causality and asserts

7d640c88 06/26/2017 11:47 PM Pierre-Loïc Garoche

const that are not dimension types should not be used to evaluate dimension expression. This happened with const variables denoting real values.

bd1bb668 06/26/2017 10:29 PM Pierre-Loïc Garoche

Moved to 1.5 dev

72b80590 06/26/2017 08:20 PM Pierre-Loïc Garoche

Preparing relaease LustreC 1.4 Xia/Xiang

9205fd1a 06/26/2017 08:11 PM Pierre-Loïc Garoche

Print branch in

d4205dc8 06/26/2017 07:41 PM Pierre-Loïc Garoche

Merge branch 'unstable' into master

3a4cc4d5 06/26/2017 07:38 PM Pierre-Loïc Garoche

More tests in default test target: main focus on C backend

a85ca7df 06/26/2017 06:51 PM Pierre-Loïc Garoche

Cleaning debug messages

728be1e1 06/26/2017 06:51 PM Pierre-Loïc Garoche

forcing introduction of new equations for fcn calls in asserts

380a8d33 06/23/2017 11:11 PM Pierre-Loïc Garoche

Solved bug in machine code generation for asserts that contain memories

1b683c9a 06/23/2017 08:10 PM Pierre-Loïc Garoche

Cleaned horrible ocaml practice (optional parameters and mli issues)

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

64385d42 06/22/2017 11:44 PM Pierre-Loïc Garoche

Turn an option to off by default: it was triggering scope plugin automatically

e70326c9 06/22/2017 05:26 PM Pierre-Loïc Garoche

Providing means to have specification as dynamic checks.
[bug] seems to crash with EMF backend

e7def055 06/22/2017 05:24 PM Pierre-Loïc Garoche

Updated scope plugin

59fc6b1c 06/22/2017 05:24 PM Pierre-Loïc Garoche

Default precision for real values printing

9a7268ba 06/22/2017 05:22 PM Pierre-Loïc Garoche

io_frontend header with new functions

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

f5a568dd 06/22/2017 05:14 PM Pierre-Loïc Garoche

Flushing after printing in io_frontend functions

32539b6d 06/22/2017 04:25 AM Pierre-Loïc Garoche

Changed encoding of matlab expression inputs from u(xx) to uxx.

f7caf067 06/22/2017 04:18 AM Pierre-Loïc Garoche

EMF backend now relies on machine code representation.
- EMF backend has an extra machines argument
- specific option to avoid merge of ite constructs
- set_backend function to improve backend selection

Most code was extracted from seahorn_backend through c0f8

d6976d31 06/22/2017 03:49 AM Pierre-Loïc Garoche

Removed duplicate tan definition in math.lusi

2800921b 06/22/2017 03:47 AM Bourbouh

add tan function to math.lusi

97be8db8 06/22/2017 03:45 AM Teme Kahsai

fixed matlab output

1411704e 06/22/2017 03:44 AM Pierre-Loïc Garoche

Changed the matlab function backend

5d6fc968 06/22/2017 03:37 AM Pierre-Loïc Garoche

Merge branch 'unstable' into seahorn_a6df3

489bd646 06/22/2017 02:35 AM Pierre-Loïc Garoche

Merge branch 'unstable' of into unstable

86aadaf1 06/22/2017 02:34 AM Pierre-Loïc Garoche

Improved dependencies for install target

2dae76da 06/21/2017 11:03 PM Pierre-Loïc Garoche

Restored common_option definition. Was removed by a non delicate merge.

b6d37e71 06/21/2017 08:50 PM Pierre-Loïc Garoche

Bug solved: EMF backend was forced

37419cf4 06/21/2017 08:46 PM Pierre-Loïc Garoche

Missing file

30dee850 06/21/2017 08:46 PM Teme Kahsai

fixed matlab output

d3e837ea 06/21/2017 08:46 PM Pierre-Loïc Garoche

Changed the matlab function backend

e0597d49 06/21/2017 08:45 PM Pierre-Loïc Garoche

_Bool are unsigned integer. The cast as a _Bool is delayed until the end of the function

b7258fa5 06/21/2017 08:42 PM Pierre-Loïc Garoche

Merge branch 'unstable' into seahorn_a6df3
a6df3 is the initial commit of branch seahorn

afbf8da2 06/20/2017 10:51 PM Bourbouh

add tan function in math.lusi

a6974c82 05/17/2017 12:21 PM Pierre-Loïc Garoche

[Horn] Workaround to prevent the use of declared keywords as node name

e656160b 05/17/2017 10:14 AM Pierre-Loïc Garoche

Better dist-clean

5d08c49e 05/17/2017 10:13 AM Pierre-Loïc Garoche

Solved printing bug in Horn backend

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

0cddb853 05/16/2017 03:18 PM Pierre-Loïc Garoche

Solved dependency in Makefile

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

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

7354c96c 05/16/2017 10:56 AM Pierre-Loïc Garoche

[bug solved] issues with asserts (invalid eqs scheduling)

4d138e19 05/16/2017 10:51 AM Pierre-Loïc Garoche

added pp_imap function

a86bae77 05/05/2017 10:09 PM Pierre-Loïc Garoche

- Adding new Makefile target for regression test
- Version now includes current git branch

b9af4e0c 05/05/2017 10:07 PM Pierre-Loïc Garoche

Cleaning test folder. Now generated with ctest/cmake

63f10e14 04/28/2017 10:11 PM Pierre-Loïc Garoche

Removing silly warning message

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

Missing file c_backend_lusic