CristalCaveGem » LustreC

Merged the master branch into mutation. Mutation of floats has been removed (temporarily)

Merge branch 'master' into mutation

Merge branch 'master' into mutation

Merge branch 'master' into mutation

Conflicts:
_oasis
_tags
configure
myocamlbuild.ml
setup.ml
src/c_backend.ml
src/main_lustre_compiler.ml
src/options.ml
src/printers.ml
test/test-compile.sh

Revert some ocaml code to ocaml 4.01 compatibility

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

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

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

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

fixed sfunction detetction

adding math.smt2

Double call to main function. Wasa clearly a typo

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.

I can't recall where we use ocamlgraph

adjusting travis

Merge branch 'master' into master

adding sfunction support

making library statically link to horn backend

adding missing stuff

adding -I options to lustrec

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

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

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

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

slight improvement of causality error messages

Arrays

adding onera automata version

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

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

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

...

...

new branch for merging mpfr and horn

...

...

full merge of salsa/mpfr and master

fixed assert compilation in case of stateless program

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

removed a bug in automata code generation

Updated to onera_git commit version 9421e24

Updated to onera_git commit version 9421e24

Bug solved in automaton part

travis

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

travis

corrected pessimistic behavior of optimization phase -O 3

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@486 041b043f-8d7c-46b2-b46e-ef0dd855326e

bug correction in typing: tuple types were computed but not recorded

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@485 041b043f-8d7c-46b2-b46e-ef0dd855326e

remove duplication

bug corrected: in some cases, local const vars were assigned twice

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@483 041b043f-8d7c-46b2-b46e-ef0dd855326e

numerous bugs corrected:
- bug in expansion of array accesses with constant arrays
- bug in printing complex array indexes (not C compliant)
- bug wrt C99 typing policy for constant arrays
- bug in signaling wrong useless static input

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@482 041b043f-8d7c-46b2-b46e-ef0dd855326e

fixed a printing bug in horn backend

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@481 041b043f-8d7c-46b2-b46e-ef0dd855326e

changes to horn

revereted to previous commit

adjusted the makefile

sync

Post 1.1 release.
Back to dev version

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@473 041b043f-8d7c-46b2-b46e-ef0dd855326e

prepare lustrec 1.1

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@471 041b043f-8d7c-46b2-b46e-ef0dd855326e

Merge of last trunk commits
Added fbyn(expr, n, init) to encode
init -> pre (init -> pre (init -> ... pre expr))
with n occurences of init

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/fby_n@460 041b043f-8d7c-46b2-b46e-ef0dd855326e

Bug fixed (454), more on travis

build status

first commit

changed name from -horn-queries to -horn-query

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@452 041b043f-8d7c-46b2-b46e-ef0dd855326e

do not use lusi for horn, and some logging for horn

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@451 041b043f-8d7c-46b2-b46e-ef0dd855326e

corrected a small bug when -horn option was active

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@450 041b043f-8d7c-46b2-b46e-ef0dd855326e

some optimization in code optimization !!

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@449 041b043f-8d7c-46b2-b46e-ef0dd855326e

corrected a bug when activating optimization (-O 3) (edge missing in a dep graph)

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@448 041b043f-8d7c-46b2-b46e-ef0dd855326e

some tiny mistakes corrected...

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@445 041b043f-8d7c-46b2-b46e-ef0dd855326e

some cosmetic changes in error messages when loading libraries

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@444 041b043f-8d7c-46b2-b46e-ef0dd855326e

Major revision due to severe limitations and bugs of inlining capabilities:
- destination dir should now work properly
- lusic files now have a version number, to avoid nasty segfaults
when loading lusic files created by an older compiler version
- inlining should now work with generic nodes and generic array library...

horn queries back

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@441 041b043f-8d7c-46b2-b46e-ef0dd855326e

Post Xia dev

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@439 041b043f-8d7c-46b2-b46e-ef0dd855326e

Prepare for tagging : Xia version 1.0

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@437 041b043f-8d7c-46b2-b46e-ef0dd855326e

corrected various bugs in the compilation/installation Makefile.in.

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@435 041b043f-8d7c-46b2-b46e-ef0dd855326e

LOTS of bug correction wrt inlining, still a work in progress...
- global constants were not accounted for
- no good avoidance of name capture when inlining
- static parameters (array sizes and clocks) not handled
- ill-typed generated expressions, when inlining array expressions...

added some test files

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@432 041b043f-8d7c-46b2-b46e-ef0dd855326e

correction of bugs:
- a small problem in the parser
- regarding the handling of destination directory, source directory, current directory, etc.
It seems to be working now. A nice chasing after weird behaviors...

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@430 041b043f-8d7c-46b2-b46e-ef0dd855326e

synch with svn

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@429 041b043f-8d7c-46b2-b46e-ef0dd855326e

fixing double printing of horn rules

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@428 041b043f-8d7c-46b2-b46e-ef0dd855326e

Fixed conflict with the svn trunk version

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@427 041b043f-8d7c-46b2-b46e-ef0dd855326e

Added local inlining using the keyword (*! /inlining/:true *)

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@426 041b043f-8d7c-46b2-b46e-ef0dd855326e

Print the types

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@425 041b043f-8d7c-46b2-b46e-ef0dd855326e

revert back to previous expression for path

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@424 041b043f-8d7c-46b2-b46e-ef0dd855326e

mapping horn values to lustre values in xml format

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@423 041b043f-8d7c-46b2-b46e-ef0dd855326e

sync horn backend

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@422 041b043f-8d7c-46b2-b46e-ef0dd855326e

sync horn backend

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@421 041b043f-8d7c-46b2-b46e-ef0dd855326e

modifed / to div in horn backend

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@420 041b043f-8d7c-46b2-b46e-ef0dd855326e

fixing double printing of horn rules

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@419 041b043f-8d7c-46b2-b46e-ef0dd855326e

Fixed conflict with the svn trunk version

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@417 041b043f-8d7c-46b2-b46e-ef0dd855326e

Changed the option horntraces to a general traces option
This annotation phases would have to be moved in optimization of normalized code

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@415 041b043f-8d7c-46b2-b46e-ef0dd855326e

Reactivated the generation of traceability information
Changed the test-compile to use the horn-traces and the horn-queries option

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@414 041b043f-8d7c-46b2-b46e-ef0dd855326e

added invariants

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@412 041b043f-8d7c-46b2-b46e-ef0dd855326e

including invariants

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@411 041b043f-8d7c-46b2-b46e-ef0dd855326e

Fixed horn backend to make query for properties. More work needed for cex

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@410 041b043f-8d7c-46b2-b46e-ef0dd855326e

Solved bug found by Teme about asserts.

Previously assert expression containing -> would lead to unnormalized ite. Now each expression within the assert is normalized and may bind new node equations.
This could be later optimized but is working now.

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@406 041b043f-8d7c-46b2-b46e-ef0dd855326e

Revert the commit 384 by Xavier: adding dirname to the source_name introduced a bug: the .h file is empty!!! Strange behavior.

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@387 041b043f-8d7c-46b2-b46e-ef0dd855326e

Added an install target in the src folder

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@386 041b043f-8d7c-46b2-b46e-ef0dd855326e

modified optimization info printout (option -print_reuse)

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@385 041b043f-8d7c-46b2-b46e-ef0dd855326e

supports again relative path for lustre source file (regression bug)

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@384 041b043f-8d7c-46b2-b46e-ef0dd855326e

added a new option -print_reuse that prints clock disjoint variables and reuse policy.
useful for debugging and carrying correctness proofs to the C code level.
non trivial result only when option -O 3 or above is activated.

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@383 041b043f-8d7c-46b2-b46e-ef0dd855326e

Moved Makefile into src folder

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@382 041b043f-8d7c-46b2-b46e-ef0dd855326e