diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index 4bb057e..b10f85e 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -225,10 +225,12 @@ let typing_contract loc contract = let teq = typing_eqs b.b_equs in let t_contract = cseq - (typing e_a) - (cseq (typing e_g) - (cseq (typing e_a_loc) - (cseq (typing e_g_loc) teq))) in + teq + (ctuplelist + [(typing e_a); + (typing e_g); + (typing e_a_loc); + (typing e_g_loc)]) in Causal.check loc t_contract; let t_contract = clear (build b.b_local) t_contract in t_contract diff --git a/compiler/minils/analysis/interference.ml b/compiler/minils/analysis/interference.ml index 3b84db5..b6bebe1 100644 --- a/compiler/minils/analysis/interference.ml +++ b/compiler/minils/analysis/interference.ml @@ -158,6 +158,12 @@ module World = struct let env = build Env.empty f.n_input in let env = build env f.n_output in let env = build env f.n_local in + let env = + match f.n_contract with + None -> env + | Some c -> + let env = build env c.c_local in + build env c.c_controllables in igs := []; vds := env; (* build the set of memories *) diff --git a/compiler/minils/transformations/schedule_interf.ml b/compiler/minils/transformations/schedule_interf.ml index 70b8945..52ae38b 100644 --- a/compiler/minils/transformations/schedule_interf.ml +++ b/compiler/minils/transformations/schedule_interf.ml @@ -137,14 +137,22 @@ let schedule eq_list inputs node_list = let rem_eqs = free_eqs node_list in List.rev (schedule_aux rem_eqs [] node_list Clocks.Cbase costs) -let schedule_contract c = - c +let schedule_contract contract c_inputs = + match contract with + None -> None, [] + | Some c -> + let node_list, _ = DataFlowDep.build c.c_eq in + (Some { c with c_eq = schedule c.c_eq c_inputs node_list; }), + c.c_controllables let node _ () f = Interference.World.init f; - let contract = optional schedule_contract f.n_contract in + let contract,controllables = schedule_contract f.n_contract (f.n_input@f.n_output) in let node_list, _ = DataFlowDep.build f.n_equs in - let f = { f with n_equs = schedule f.n_equs f.n_input node_list; n_contract = contract } in + (* Controllable variables are considered as inputs *) + let f = { f with + n_equs = schedule f.n_equs (f.n_input@controllables) node_list; + n_contract = contract } in f, () let program p =