- Bugs in partial evaluation for equalities among bool constants
  and a nice recursive call generating a stack overflow! Now solved
- Setup a timeout for z3 in seal
- Better log for seal

we generate the transition pridicate but also the invariant. But two problems, occured.
The first one is a visibility problem for the record which is private but must be
public for ghost variable which have to be public for specifaction. The second
problem is that the approache requires existential quantification for inputs and
locals. It works for integers and boolean but not for floats. Some complex
solution could be found like writing an iterator for floats, expanding all
local variable and store all the required inputs in ghost variable.

     more simple.

  - Correct the merge with lustrec-seal
  - Improve support for builtin function(still work to do)
  - Add generation of a gpr file for lib(without main).
  - Add var initialisation in the reset, still work to do.

  instance.

to the pp_file and all subfunction in adb generation we pass a list of typed instance which
contains the submachines directly with the instance name and the substitution.

     package using it. It required a lot of refactoring.

only if the main node option is given to lustrec. This feature implied some refactoring. Also
added some OCaml Doc to undocummented functions.

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

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

 - corrected a regression bug in main_lustre_compiler.ml (optional generation of lusic files was in a bad ocaml pattern-matching rule...)
 - added a flush in Log to help find out the exact phase when the compiler crashes or stops silently 

 - corrected a regression bug in main_lustre_compiler.ml (optional generation of lusic files was in a bad ocaml pattern-matching rule...)
 - added a flush in Log to help find out the exact phase when the compiler crashes or stops silently 


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

Moved backends in separate folders

Moved backends in separate folders



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

Changed the load of lusi files: imported nodes or function can specify the linking lib and/or use a classical C prototype (without pointers).
Parse updated as well as Makefile generation.

Changed the load of lusi files: imported nodes or function can specify the linking lib and/or use a classical C prototype (without pointers).
Parse updated as well as Makefile generation.



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