Zustre: timeout and slicing
zustre progress. Issues with sliced predicates
package z3 to Z3 when using z3 github repo.
Adding input in MAIN fdecl
[lustrev] forced the z3 lib to be loaded before others when using the provided bash script.
[lustrev] fixed some issues when calling Z3. Seems working for the moment: basic call to Z3 and sat/unsat result
Some progress on zustre
Merge branch 'unstable' into lustrec-seal
Integer div choices
Provide back the previous behavior concerning parsing spec.
Merge branch 'cocospec' of https://cavale.enseeiht.fr/git/lustrec into unstable
Merge branch 'euclidean' into unstable
Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable
Merge branch 'euclidean' of https://cavale.enseeiht.fr/git/lustrec into euclidean
introduced euclidean/C-like division in C code generation
install of yojson depends on lustresf in configure now
Euclidean div/mod treatment in Horn backend
Issues with typing pp_basic_lib_fun
Kind licence file
Tentative to rely on Kind parser for contracts
Produce condition coverage for basic boolean expressions. To be improved with a simpler condition.
[lustrec/mcdc/ improved the MCDC output
Tuning the pretty printing of Salsa plugin
Homogenizing the API for salsa and its use within the plugin
Some tentative improvement of Salsa plugin. Not satisfying yet
Moved mk_fresh_var from normalization to corelang
[scopes] Producing the appropriate scope label
Merging unstable into salsa
Merge branch 'unstable' into salsa
Try to debug the use of Z3 API. Still having troubles
Zustre: do not declare variables as Fixedpoint relations
Filtering out ERR and MAIN from the forall quantification
Some progress on zustre2
zustre: missing basic ops
Merge branch 'lustrec-seal' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal
Merge conflict solved
Basic library printers moved into backend specific printer files
Further restructuring:- arrow.ml* to define basic builder for arrow (node, name, ...)- machine_code_common similar to corelang but for machine_code (printers, some builders, ...)- machine_code restricted to the translatation from normalized nodes to machines
MLI for normalization and machine_code.Structs defining machines are now in machine_code_types
- Makefile: solved dependency problem when compiling include lusi- Renamed type declarations as lustre_types and machine_code_types
Updated TODOChanged selection of files in odocl
Ongoing work on zustre
ongoing work on zustre backend
Add the script to update LD_LIBRARY_PATH for z3
add lustrec math functions
Recursive resolution of dependencies
- 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.
Ongoing work on salsa: introduce slicing of expr
[lustresf] work in progress. Added global env with initial values
Conditional activation of machine type plugin. currently a little buggy. Shall be desactivated.
Updated Salsa plugin to latest version of Salsa.Some issues wrt machine type features.Work in progress
Solved issue with typing of enumerated 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
[lustret] improved enumeration of mutants
[lustret] When generating MC/DC conditions, produce them as EMF XML output
Solved issues with configure and ocaml libs dependencies
Type issue Bytes vs string
[lustret] More effective mutants generation Solved the misrenaming of imported nodes (eg int_to_real)
[main] node locals are now sorted according to their dependencies wrt clocks. The produced lustre node with types shall now be compilable
[main] cleaned superfluous empty line in generated lustre output
[main] enum typedef in C use the original lustre filename as identifier. This commit cleans the filename to remove dots.
[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.
Added cmake basic functionsImproved the Cmake Lustre_Compile function
No existing input file returns a 1 error code
[stateflow] some progress, linking the parsed json to lustrec engine. Some variables are not yet typed. To investigate ...
[general] adding more entry rules for lustre parser to extract expressions, vdecl_list and statement list
[global] reordered local vars, keeping the declared ones before the others. Was mandatory for clocked expressions in compiled automata.
[salsa] cleaning verbose logs
[general] Refactor get_node_eqs to produce (eqs, auts) with automatons
Forcing mpfr status when -real mpfr asked. Default precision is 100 bits.
add uninstall target in Makefile
correct install target in Makefile
[lustresf] lustresf targets are optional in Makefiles (see configure.ac)
Merge branch 'unstable-merge' into unstable
[lustresf] use Unix package
[lustresf] add Program constructor in model examples + sf_sem
[JSON] remove pretty-printing functions declarations in cPS_transformer
[lustresf] refactoring automata generation using Automata.ml functions
simple conflict when merging unstable and json-parser
[general] print types before nodes in lustre output
typo in src/Makefile.in
[lustresf] Some progress: automaton compiles but not when preprocessed
[EMF] Less verbose
add fmod function in include/simulink_math_fcn.lusi
Added some libm functions to lustrec_math.lusi
[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