package lustre-v6

You can search for identifiers within the package.

in-package search v0.2.0

The Lustre V6 Verimag compiler

Install

Dune Dependency

www-verimag.imag.fr Edit opam file Versions (4)

Authors

E

Erwan Jahier and Pascal Raymond

Maintainers

E

erwan.jahier@univ-grenoble-alpes.fr

Sources

lustre-v6.6.103.3.tgz

md5=755e46de4d57d4c489f5b0a0f2b8663d

sha512=8d452184ee68edda1b5a50717e6a5b13fb21f9204634fc5898280e27a1d79c97a6e7cc04424fc22f34cdd02ed3cc8774dca4f982faf342980b5f9fe0dc1a017d

doc/lustre-v6/EvalClock/index.html

Module `EvalClock`Source

Static evaluation of clocks.

Source

val f : 
  IdSolver.t ->
  UnifyClock.subst ->
  Lic.val_exp ->
  Lxm.t list ->
  Lic.clock list ->
  Lic.val_exp * Lic.id_clock list * UnifyClock.subst

f lxm ids s ve exp_cl checks that ve is well-clocked (i.e., for node calls, it checks that the argument and the parameter clocks are compatible), and returns a clock profile that contains all the necessary information so that the caller can perform additional clock checks.

exp_cl is the expected clock profile; if cl is empty, no check is done (should be an option type)

check_res lxm cel cil checks that the expected output clock profile of an expression "cil" is compatible with the result clocks "cel" of the expression.

For instance, in order to clock check the equation

(x,y)=toto(a,b);

it checks that the clock of "(x,y)" (cel) is compatible with the output clock profile of node toto (cil).