Ada: pretty printing of reset function
Merge branch 'ada' of https://cavale.enseeiht.fr/git/lustrec into ada
Ada Change private to limited private for State type package.
Ada: first pretty printing functions for adb
Ada: Temporary change
Ada: Add local variable declaration for step
Ada: Last correction was incorrect
Ada: Correct a bad copy-paste
Ada: Add the generation of the wrapper file : the main ada file and the project. It is calledonly if the main node option is given to lustrec. This feature implied some refactoring. Alsoadded some OCaml Doc to undocummented functions.
Ada: Add to the machine state all its subinstance states. Improve also identifier cleaning
Ada: Changed type name for states and normalized variable name to match ada requirements.
Ada: Add prototype of the four procedure in the adb generation
Ada: Add the state variable in the ads, type definition and as parameter of all procedure
Ada: Move some functions from ada_backend_ads.ml to ada_backend_common.ml
Ada: Remove useless comment
3 main modifications : - Create a new file : ada_backend_common.ml which contains all the function common to adb and ads. - Add comment to function - Generate the procedure prototype in the ads
Basic structure for Ada backend
Ada: skeletons for Ada compiler
Num module for mli
Num is a package in recent ocaml
Cleaning warning in mpfr
math fun lib support in MPFR
EMF export of local type definition (for simple types)
mutation bug solved: improper access to an element of an empty list of bindings
Printers bug solved: now properly printing lustre file as open/types/other decls
Lustre test gen mutation: bug solved. The path to the installation was hardcoded.
Bug solved in MCDC generation: Some annotations generated were producing problems
Print the spec within the node
Pretty serious update:- a bug in regressio ntest Simulink/integrator_ext_IC_matrix_test revealed the following (serious issue): when building the list of instruction (in the machine code) the access to variable were hardcoded to LocalVar or StateVAr depending whether the variables was part of the identified memories....
Moved back mpfr to its folder. Previsouly there was two competing files :(
MPFR bug solved: typing of function argument was not properly building tuples of types.
Removed Contract contruct: imported node should be enough. Solved some warning at compile time
Further processing of contract in the typing. More to go
Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable
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
- 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.
updated luster lexer ??
bug wrt normalization. Didn't take clock into account.
strange bug (ill-typed source) wrt Bytes/String conversion
bug in CSE, was disregarding clock
corrected kind parsing
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
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
Recursive resolution of dependencies
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
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.