package lustre-v6

  1. Overview
  2. Docs

Static evaluation of clocks.

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).

val check_res : Lxm.t list -> UnifyClock.subst -> Lic.left list -> Lic.id_clock list -> unit
OCaml

Innovation. Community. Security.