Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec @ ef8a361a

# Date Author Comment
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 https://cavale.enseeiht.fr/git/lustrec 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 configure.ac

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
- Options.ml has been split into Options.ml / Options_management.ml. Options.ml 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.
Impact:
- 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 https://cavale.enseeiht.fr/git/lustrec 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

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

9a555140 04/27/2017 01:38 PM Pierre-Loïc Garoche

_tags is generated now

1954d776 04/27/2017 01:38 PM Pierre-Loïc Garoche

Cleaner configure autoconf script

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

Merge branch 'testgen' into merging_unstable_testgen

d2d9d4cb 04/26/2017 11:25 PM Pierre-Loïc Garoche

Missing files

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

8d184ba8 04/26/2017 02:15 PM Pierre-Loïc Garoche

Removing generated file

a97d3e02 04/25/2017 10:57 PM Pierre-Loïc Garoche

Printing reals in Horn backend

0d065e73 04/25/2017 09:43 AM Pierre-Loïc Garoche

Solved a bug in the compilation of asserts. Now different behavior depending on the backend:
functional: keep it as is
non func: introduce a fresh local var v and replace assert(e) by v=e; assert (v);

76c7023b 04/25/2017 09:42 AM Pierre-Loïc Garoche

functional_backend function moved to corelang

4e809854 04/25/2017 09:41 AM Pierre-Loïc Garoche

Cosmetic changes

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

More informative error message in case of untyped value

5cd53307 04/25/2017 09:40 AM Pierre-Loïc Garoche

Updated deps: requires ocamlgraph as an ocamlfind package

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

Deprecated function changed for compatibility with ocaml 4.04

bde99c3f 04/06/2017 04:27 PM Xavier Thirioux

This is the first merge that does compile. Not tested yet.

40d33d55 04/05/2017 04:53 PM Xavier Thirioux

first version (doesn't even compile) of mutation and test generation standalone command: lustret
mostly a recovery of an ancient svn repo: mutations

a69af35f 03/20/2017 02:20 PM Pierre-Loïc Garoche

another issue with an old merge: missing nums dep

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

e49b6d55 02/14/2017 12:11 PM Xavier Thirioux

nice bug correction wrt constants with a large number of digits. Would raise exception when comparing these constants

301f18e6 02/01/2017 12:21 AM Teme Kahsai

remove deps

92ff8f1b 02/01/2017 12:21 AM Teme Kahsai

fix tracebility

a6df3992 01/31/2017 08:22 PM Pierre-Loïc Garoche

Working on EMF backend to express cocospec infos as Simulink blocks

5fb5b031 01/31/2017 01:40 AM Pierre-Loïc Garoche

cosmetic changes

d7e04983 01/13/2017 01:17 PM Pierre-Loïc Garoche

[Horn] Updated traceability of Horn backend to deal with fby (arrow machines)