unsafe in minils node

This commit is contained in:
Léonard Gérard 2011-12-12 11:27:18 +01:00
parent b86555e013
commit f0cbbccc2a
2 changed files with 5 additions and 1 deletions

View file

@ -189,6 +189,7 @@ let translate_contract contract =
let node n =
{ n_name = n.Heptagon.n_name;
n_stateful = n.Heptagon.n_stateful;
n_unsafe = n.Heptagon.n_unsafe;
n_input = List.map translate_var n.Heptagon.n_input;
n_output = List.map translate_var n.Heptagon.n_output;
n_contract = translate_contract n.Heptagon.n_contract;

View file

@ -128,6 +128,7 @@ type contract = {
type node_dec = {
n_name : qualname;
n_stateful : bool;
n_unsafe : bool;
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
@ -140,6 +141,7 @@ type node_dec = {
n_param_constraints : constrnt list;
n_mem_alloc : (ty * Interference_graph.ivar list) list; }
type const_dec = {
c_name : qualname;
c_type : ty;
@ -202,11 +204,12 @@ let mk_equation ?(loc = no_location) unsafe pat exp =
let mk_node
?(input = []) ?(output = []) ?(contract = None) ?(pinst = ([],[]))
?(local = []) ?(eq = [])
?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = [])
?(stateful = true) ~unsafe ?(loc = no_location) ?(param = []) ?(constraints = [])
?(mem_alloc=[])
name =
{ n_name = name;
n_stateful = stateful;
n_unsafe = unsafe;
n_input = input;
n_output = output;
n_contract = contract;