First working version of switched system extraction for seal tool
Restructuring code in SEAL
Merge branch 'unstable' into lustrec-seal
Merge branch 'cocospec_to_be_merged' into unstableMainly adapting to new cocospec syntax for contracts
Merge branch 'cocospec' of https://cavale.enseeiht.fr/git/lustrec into cocospec
SEAL: compute the projection to switched systems. Some issues with intermediate variables and a better selection of split guard have to be addressed
log new option to mention plugin or module
Moved find_eq from Machine_code to Corelang and sort_eqs from Machine_code to Scheduling
Preprocess the selected node in seaL BACKEND: focus on memories and perform node slicing.
Scheduling of node equations is now attached to machine type
Moved definition of graph modules from Causality to Utils to avoid cyclic deps
- 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
Some refactoringAdapted the parser/types/constructors for cocospec syntax
[bug solved] do not normalize eexpr in annotations, only in specification.
solve error in lexer introduced by previous merge
finishing solving strange conflicts for merge...
Renamed annots into contracts. Preparing for syntax extension
- Removed the kind2 file (parser/lexer/types)- Cleaned a little bit our parser: removal of old prelude constructs
Byte/String bug reappeared
Merge branch 'master' of https://cavale.enseeiht.fr/git/lustrec
Solved bug#57: issues when indirect init of a pre in horn-traces
Temporily disabling Mehnir as a parser.
Merge branch 'vhdl' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal
Refactoring of vhdl data types
Added two fresh vars counter and uid.uid is a list of integer denoting the specific instance of a stateful/stateless node.
New option to select github version of Z3Added Yojson dependency in lustrevSome progress on Cex generation
Added support for Process statements, signal assignment, If, Exit and Null sequential statements
Added postprocessing for numeric literals
Ongoing work on json vhdl to vhdl structure conversion
Zustre: timeout and slicing
updated luster lexer ??
Pom pom pom
Sample value for VHDL
Compiling - while doing nothing :)
Bootstrapping VHDL importer/exporter
bug wrt normalization. Didn't take clock into account.
strange bug (ill-typed source) wrt Bytes/String conversion
bug in CSE, was disregarding clock
Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable
zustre progress. Issues with sliced predicates
package z3 to Z3 when using z3 github repo.
Adding input in MAIN fdecl
[lustrev] fixed some issues when calling Z3. Seems working for the moment: basic call to Z3 and sat/unsat result
corrected kind parsing
Some progress on zustre
updated division for Horn clauses
corrected euclidean division in C code
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 'euclidean' of https://cavale.enseeiht.fr/git/lustrec into euclidean
introduced euclidean/C-like division in C code generation
Euclidean div/mod treatment in Horn backend
Issues with typing pp_basic_lib_fun
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
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