Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src @ 37419cf4

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

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)

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

Revert some ocaml code to ocaml 4.01 compatibility

3ebf9aa2 01/11/2017 12:40 AM Pierre-Loïc Garoche

Remove generated files (.h for include for as well as .in files of configure)

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

0a6648a3 01/04/2017 12:32 AM Pierre-Loïc Garoche

Double call to main function. Wasa clearly a typo

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.

0bb94b98 01/04/2017 12:28 AM Pierre-Loïc Garoche

I can't recall where we use ocamlgraph

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

2dd3d358 12/29/2016 07:18 AM Teme Kahsai

making library statically link to horn backend

7db425aa 12/28/2016 01:31 AM Teme Kahsai

adding missing stuff

fc476249 12/28/2016 01:00 AM Teme Kahsai

adding -I options to lustrec

822f31e1 12/08/2016 05:55 PM Teme Kahsai

updating to onera version 30f766a:2016-12-04

323c5b19 12/08/2016 05:46 PM Teme Kahsai

updating to onera version 30f766a:2016-12-04

3b2bd83d 12/08/2016 05:37 PM Teme Kahsai

updating to onera version 30f766a:2016-12-04

9c734e5f 11/22/2016 07:38 PM Pierre-Loïc Garoche

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

eb837d74 10/21/2016 01:52 AM Xavier Thirioux

slight improvement of causality error messages

84902260 10/12/2016 11:44 PM jbraine

Arrays

85a6f473 09/30/2016 06:41 PM Teme Kahsai

adding onera automata version

bb1b5e04 09/28/2016 10:16 AM Pierre-Loïc Garoche

Ongoing work on c backend for makefile. Does not compile yet

dc893173 09/07/2016 05:38 PM Pierre-Loïc Garoche

moving C files name declaration in backend. Preparation for additional cmake target

41e48ef3 09/01/2016 11:18 AM Eric NOULARD

Add codename to version handling. This should ease making release.
Development codename is "dev"

f3d244c1 08/09/2016 10:01 PM Xavier Thirioux

...

45f0f48d 08/09/2016 09:31 PM Xavier Thirioux

...

fea041c5 08/09/2016 09:25 PM Xavier Thirioux

new branch for merging mpfr and horn

50d39c99 08/06/2016 10:43 AM Xavier Thirioux

...

66e25f0f 08/06/2016 10:41 AM Xavier Thirioux

...

04a63d25 08/06/2016 10:29 AM Xavier Thirioux

full merge of salsa/mpfr and master

3cdd2147 06/02/2016 01:45 AM Teme Kahsai

fixed assert compilation in case of stateless program

28d2185f 04/12/2016 09:24 AM Xavier Thirioux

bug removed: with dummy automata, lustrec would generate parameterless nodes, which is forbidden in Lustre (and would raise an exception)

a406ac67 04/12/2016 12:49 AM Xavier Thirioux

removed a bug in automata code generation

bad9b6b2 02/23/2016 10:49 PM Teme Kahsai

Updated to onera_git commit version 9421e24

a1daa793 02/23/2016 10:47 PM Teme Kahsai

Updated to onera_git commit version 9421e24

60aab16d 02/02/2016 06:35 PM Xavier Thirioux

Bug solved in automaton part

868650b1 01/18/2016 08:19 PM Teme Kahsai

travis

ca88e660 01/08/2016 05:37 PM Pierre-Loïc Garoche

Resolved conflict when merging salsa with horn_encoding. The current branch is the most updated.

5775ac97 01/08/2016 03:00 PM Xavier Thirioux

bug correction in automata.ml (order of assigned variables was not always coherent between automata branches)

f0bff3e5 01/08/2016 01:41 PM Pierre-Loïc Garoche

Merge branch 'salsa' into merge_salsa_horn_2
Postponed conflicts to be solved
Conflicts:
src/_tags
src/backends/Horn/horn_backend.ml
src/machine_code.ml
src/main_lustre_compiler.ml
src/myocamlbuild.ml.in
src/optimize_machine.ml

a7e70823 01/07/2016 10:55 PM Pierre-Loïc Garoche

Clean old and resolved TODO

8d0c1f8e 01/07/2016 06:44 PM Pierre-Loïc Garoche

fixed a z3 bug for => within Horn clauses

cf9cc6f9 01/07/2016 04:43 PM Pierre-Loïc Garoche

Introduced the opposite of Reset call: NoReset. This simplify the general compilation process and makes the code more symmetric, hence simpler and clearer code.

c4f14d0a 01/07/2016 04:42 PM Pierre-Loïc Garoche

Removed file thanks to the use of ocamlfind

2ed9b6f2 01/07/2016 04:41 PM Pierre-Loïc Garoche

solved bug: missing parenthesis in enum typedef

8eee42de 01/07/2016 04:41 PM Pierre-Loïc Garoche

Refined the dependencies in the generated makefile

92aa8330 01/07/2016 04:40 PM Pierre-Loïc Garoche

Using ocamlfind to link with ocamlgraph

5df5dd85 12/16/2015 03:18 PM Pierre-Loïc Garoche

Merge branch 'master' into horn_enum_types

Conflicts:
src/backends/Horn/horn_backend.ml

bdcbb2a1 12/15/2015 05:40 PM Pierre-Loïc Garoche

Solved bug with C backend

8b450806 12/15/2015 01:56 PM Pierre-Loïc Garoche

Enable expressions in array indices

84462531 12/15/2015 01:56 PM Pierre-Loïc Garoche

Added by default -O0

7ec8e203 12/09/2015 12:40 AM Teme Kahsai

travis

d97c196a 12/08/2015 03:39 PM Xavier Thirioux

Changed mpfr threshold to 2

0f36882c 11/29/2015 01:20 PM Xavier Thirioux

several bugs/oddities corrected:
- bizarre date stamping (when generating .lusi files)
- bug in loading libraries, forbidding several (transitive) imports of the same library.
- plugin scopes was wrongly always activated