- Controllable-Nbac export (CtrlNbacGen): correct handling of float
expressions, as well as alias types;
- Controllable-Nbac controller importer (CtrlNbacAsEpt): Declaration
of enumerated types and aliases that are relocated to controller
modules is now performed based on the interface. Dependencies
between type aliases are also taken into account now;
- ctrl2ept tool: correct loading of pervasives module.
To avoid cyclic module dependencies (that show up when trying to
compile, e.g, the generated C code), enumerated types declared in the
main program are now "moved" into the module containing the generated
controllers.
To enable recovery of parameter and output ordering by `ctrl2ept', the
Controllable-Nbac generation procedure now declares a new module
dedicated to the encapsulation of the controller functions yet to be
synthesized.
Handling of type declarations are probably buggy.
Handling of contracts when the "z3z" target is off. Equations of contracts are
put into the node in the Mls2obc pass (done by the "z3z" code generation).
Allowing additional inputs from abstractions within contracts. Thus,
calling non-inlined subnodes is allowed, as well as operations on
non-Boolean inputs or states (in contracts).
- Stripped portions of `myocamlbuild{,_config}.ml' that seem useless
when `-use-ocamlfind' is passed to ocamlbuild.
- Added some code in `myocamlbuild_config.ml' to be able to generate
documentation by merging interface and implementation files.
- CtrlNbac: new module for internal representation and output code for
Controllable-Nbac format;
- CtrlNbacGen: translation into Controllable-Nbac of Minils nodes
necessitating controller synthesis; the insertion of calls to
controllers is not yet done, and the nodes are left unchanged.
- Translation to z3z now evaluates constant expressions instead of
abstracting them. This non-feature could cause "false" synthesis
failures due to non-translatable yet constant expressions possibly
introduced by tomato (or manually), for instance `not false' in node
`n' bellow:
node n (a: bool) returns (ok: bool)
contract assume true enforce ok with ()
let
ok = a or not false;
tel
Corrected a somewhat unnoticeable but ugly bug in the generation of C
records, that could mess up the field names when they were not
assigned in the same order as in the declaration of the type.
