Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends @ e4edf171

# Date Author Comment
e4edf171 04/03/2018 04:38 PM Pierre-Loïc Garoche

Zustre backend

6eda0c25 03/30/2018 11:40 PM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal

ea8f51ae 03/30/2018 11:23 PM Pierre-Loïc Garoche

Basic library printers moved into backend specific printer files

2863281f 03/30/2018 11:14 PM Pierre-Loïc Garoche

Further restructuring:
- arrow.ml* to define basic builder for arrow (node, name, ...)
- machine_code_common similar to corelang but for machine_code (printers, some builders, ...)
- machine_code restricted to the translatation from normalized nodes to machines

089f94be 03/30/2018 10:43 PM Pierre-Loïc Garoche

MLI for normalization and machine_code.
Structs defining machines are now in machine_code_types

8446bf03 03/30/2018 05:54 PM Pierre-Loïc Garoche

- Makefile: solved dependency problem when compiling include lusi
- Renamed type declarations as lustre_types and machine_code_types

c1785a55 03/28/2018 10:35 AM Pierre-Loïc Garoche

ongoing work on zustre backend

0bca9d53 03/15/2018 02:58 AM Pierre-Loïc Garoche

Recursive resolution of dependencies

ad4774b0 03/15/2018 12:07 AM Pierre-Loïc Garoche

- Normalization parameters (alias and unfold_array) are now provided as parameter
- program type renamed as program_t
- Initiating the lustrev tool with dependencies to z3 and seal.

66359a5e 01/31/2018 07:27 AM Pierre-Loïc Garoche

[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program

185ddf4d 01/30/2018 03:01 PM Pierre-Loïc Garoche

Type issue Bytes vs string

13aec2da 01/18/2018 05:31 PM Pierre-Loïc Garoche

[main] enum typedef in C use the original lustre filename as identifier. This commit cleans the filename to remove dots.

2196948d 12/12/2017 09:25 AM Pierre-Loïc Garoche

[EMF] Less verbose

7c79dd93 11/14/2017 07:22 PM Pierre-Loïc Garoche

[EMF] adding original name field in the JSON

7eafa0e1 11/10/2017 12:19 AM Pierre-Loïc Garoche

[EMF] Added the reset signal (the every argument) as input to the JSON struct

c80e92d1 11/09/2017 10:58 PM Pierre-Loïc Garoche

Solving a warning with ocaml 4.04 and uppercase_ascii. Provides backward compatibility for 4.02

953879f0 11/09/2017 10:45 PM Pierre-Loïc Garoche

Issue with clocked expressions. Now handled throught a local branch, ie. a single action block in Simulink

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

Printing reals in Horn backend

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

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.

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

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

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

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

042dc586 01/11/2017 10:02 AM Pierre-Loïc Garoche

Revert some ocaml code to ocaml 4.01 compatibility

dcafc99b 01/11/2017 12:28 AM Pierre-Loïc Garoche

Merge branch 'github_master' into integ_github_jan10
Intregrate all modifs by Teme et al

60f23302 01/10/2017 01:35 PM Pierre-Loïc Garoche

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

6fa45cb6 01/10/2017 01:35 PM Pierre-Loïc Garoche

Changed the generated C file to produce input and output csv files (named inXX and outXX)

d128bbd4 01/06/2017 08:04 PM Teme Kahsai

fixed sfunction detetction

9f77bff7 01/06/2017 08:11 AM Teme Kahsai

adding math.smt2

44ce4da8 01/04/2017 12:30 AM Pierre-Loïc Garoche

Solved some issues with commited code (like it doesn't compile). The code was written by Teme's student and
- did not rely on existing typing.ml function
- used strange fprintf code

Code was refactored but old stuff kept in comment just in case. Will have to be cleaned at some point.

e057dd08 12/30/2016 10:47 PM Teme Kahsai

adjusting travis

7ad4ff7c 12/30/2016 09:29 PM Teme Kahsai

Merge branch 'master' into master

1b57e111 12/30/2016 09:20 PM Teme Kahsai

adding sfunction support