Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src @ 38ae7765

# Date Author Comment
38ae7765 10/06/2017 10:10 AM Pierre-Loïc Garoche

no comment

c5d45c13 09/22/2017 05:43 PM Pierre-Loïc Garoche

[lustresf]: tuple of false values for initial state

74ca6b61 09/22/2017 05:38 PM Pierre-Loïc Garoche

A fresh option to print with declared types instead of inferred ones

69c96b6c 09/22/2017 04:39 PM Pierre-Loïc Garoche

lustresf: Better construction of lustre ast. Still more work to be done.

27e5a70d 09/22/2017 04:38 PM Pierre-Loïc Garoche

Even prettier pretty printing. Is it even possible to improve?

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

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 https://cavale.enseeiht.fr/git/lustrec 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

blup

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.

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: https://github.com/coco-team/lustrec/issues/13

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

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.

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

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

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

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

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

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

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

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

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

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

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