History | View | Annotate | Download (6.97 KB)
lustret: do not reload opened modules when generating the mcdc output
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...
- Dep type with a tuple has been replaced by a record type- Modules now is more integrated and performed the building of the type/clock env. previously some computation were performed twice by different functions. Some of these functions have been moved from compiler_common to modules
Merge branch 'unstable' into lustrec-seal
Lustre test gen mutation: bug solved. The path to the installation was hardcoded.
- Global type env and clock env now availble as a global reference (Global module)- Adapted the parsing of specification with a cocospec compatible one- The data structure of contracts is now almost cocospec compatible- Lustrec-test has been updated to use the newest syntax
- Makefile: solved dependency problem when compiling include lusi- Renamed type declarations as lustre_types and machine_code_types
- 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.
[lustret] When generating MC/DC conditions, produce them as EMF XML output
[lustret] More effective mutants generation Solved the misrenaming of imported nodes (eg int_to_real)
[mutations] solved issues with - mutations that could not be performed (ie. changing an integer constants when no integer constant appear in the program) - infinite computation of mutants, because of unproper randomization.
[MCDC] Solved some issues and transformed the code from iterators to fold
[lustret] bug solved in file path
[lustret] mutation report is create in initial folder
[lustret] Improved mutation with json traceability
First working version of algebraic loop resolution. Disabled by default.
- 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
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".
Cleaning output:- no more classic display for ocamlc- compilation warnings removed
This is the first merge that does compile. Not tested yet.
first version (doesn't even compile) of mutation and test generation standalone command: lustretmostly a recovery of an ancient svn repo: mutations