[bug cavale 93] solved: issue when resetting a stateless node. Now generating a warning and forcing the stateful status. Could be improved to remove the reset statement. (TODO)
printing nodes + more progress on seal export
temporary changed in the expression printer
kind2 option for printing expressions
More kind2 outputs: clocked fun call + clocked and restart fun call
when condition in kind2 printer
every in kind2 syntax
kind2 output for printer. global option available
No space in comments
Contract printer cocospec
No space before contract kwd
Printing trailing zeros in real constants
minor bugs solved in printer: guarantee vs guarantees in cocospec. Imported node shall not be printed as regular code since it is not part of the grammar yet. Kept them as comment.
Cocospec: parsing, normalizing and processing machines for contracts.
Some progress on compiling cocospec contract.Contract resolution still need to be done as well as dealing with the machine code level and so on.
Unified compilation of lusi and lus filesDifferent parsers yet but shared process.In case of lusi input the C backend is bypassed since the .h is generated from the lusic and no C code should be generated since it may overwrite existing manually written code...
Added include directive that directly inject a lustre source file in the prog
Printers bug solved: now properly printing lustre file as open/types/other decls
Print the spec within the node
Removed Contract contruct: imported node should be enough. Solved some warning at compile time
Further processing of contract in the typing. More to go
Some refactoringAdapted the parser/types/constructors for cocospec syntax
Tentative to rely on Kind parser for contracts
- Makefile: solved dependency problem when compiling include lusi- Renamed type declarations as lustre_types and machine_code_types
[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
[main] cleaned superfluous empty line in generated lustre output
[general] Refactor get_node_eqs to produce (eqs, auts) with automatons
[general] print types before nodes in lustre output
solved bug 56: missing last node in generated lusi
A fresh option to print with declared types instead of inferred ones
Even prettier pretty printing. Is it even possible to improve?
EMF backend: each branch provides the inputs and outputs
Full rewrite of EMF backend.
trying to improving pretty printing. Not so perfect for the moment
Merge branch 'github_master' into integ_github_jan10Intregrate all modifs by Teme et al
adding sfunction support
updating to onera version 30f766a:2016-12-04
adding onera automata version
full merge of salsa/mpfr and master
Updated to onera_git commit version 9421e24
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
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...
- Added major feature: Lustre V6 automata !!! - one automata example added - changed the reset condition in node calls (now a simple bool expr) - bug corrected in clock calculus - bug corrected in traceability info - added field in variables to test whether they are original...
- work in progress for automata...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@333 041b043f-8d7c-46b2-b46e-ef0dd855326e
- corrected bugs with the inlining mode
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@329 041b043f-8d7c-46b2-b46e-ef0dd855326e
This is a major revision: - added interface files (.lusi) in the language, that can be compiled on their own, giving an object file (.lusic) and a header file (.h) - modular code generation, from Lustre to C level included. - nice amount of code refactoring...
added some functions, prior to code refactoring
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@322 041b043f-8d7c-46b2-b46e-ef0dd855326e
- started refactoring type definitions in .lus/.lusi, in order to ease the way .lusi interface files are handled.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@321 041b043f-8d7c-46b2-b46e-ef0dd855326e
Updated the licence info and header for each file.Moved backends in separate folders
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@313 041b043f-8d7c-46b2-b46e-ef0dd855326e
Merged horn_traces branch
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@303 041b043f-8d7c-46b2-b46e-ef0dd855326e
Prepared first stage of code reorg:1. moved type def in lustrespec.ml2. moved constructor and basic functions in corelang3. Modified eexpr with prenext quantifiers
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/specification_reorg_corelang_parser@297 041b043f-8d7c-46b2-b46e-ef0dd855326e
Added the lustre backendStill some work on adapating the instruction scheduling
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/cleaner_backend@279 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.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@242 041b043f-8d7c-46b2-b46e-ef0dd855326e
- corrected causality bug (cf. previous commit)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@227 041b043f-8d7c-46b2-b46e-ef0dd855326e
Added declaration/definition of stateless/stateful nodes. The 'function' keyword is for stateless nodes only, the 'node' keyword is any kind of node. Improves compilation and paves the way for more optimizations.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@202 041b043f-8d7c-46b2-b46e-ef0dd855326e
- work in progress for stateless/stateful status computation (to turn conditionals into merges, which yield more efficient C code)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@198 041b043f-8d7c-46b2-b46e-ef0dd855326e
more steps towards struct types...Cette ligne, et les suivantes ci-dessous, seront ignorées--
M trunk/src/corelang.mliM trunk/src/type_predef.mlM trunk/src/main_lustre_compiler.mlM trunk/src/types.mlM trunk/src/printers.mlM trunk/src/typing.ml...
first steps towards struct types...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@182 041b043f-8d7c-46b2-b46e-ef0dd855326e
- added generation of clock information in interface (.lusi) files- added clock checking between interface and implementation files
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@176 041b043f-8d7c-46b2-b46e-ef0dd855326e
- merged test script - added -d support - corrected #open parser problem - corrected interface/implementation (.lusi/.lus) checking for types (not yet for clocks)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@171 041b043f-8d7c-46b2-b46e-ef0dd855326e
Solved some bugs in the lustre printerGeneration of a witness with both the main node and hte inlined main nodeTest script modified to check consistency of the inlining process
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/inlining@162 041b043f-8d7c-46b2-b46e-ef0dd855326e
Merge (if it works) of the lustre interfaces branche providing lusi files into trunk
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@123 041b043f-8d7c-46b2-b46e-ef0dd855326e
Moved files to trunk in lustre_compiler
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@116 041b043f-8d7c-46b2-b46e-ef0dd855326e