Avoid exporting contract-less or parametric nodes into DCS tool formats.

This commit is contained in:
Nicolas Berthier 2014-12-15 15:56:37 +01:00
parent 307f3d8418
commit 177f5f9f3e
2 changed files with 15 additions and 6 deletions

View file

@ -528,6 +528,10 @@ let gen_ctrlf_calls ~requal_types gd node_name equs =
contract. *)
let translate_node ~requal_types typdefs = function
| ({ n_contract = None } as node) -> node, None
| ({ n_name; n_params } as node) when n_params <> [] ->
warn "Unsupported@ translation@ of@ parametric@ node@ `%s'@ with@ \
contract@ into@ Controllable-Nbac!" (Names.fullname n_name);
node, None
| ({ n_name; n_input; n_output; n_local; n_equs;
n_contract = Some contr } as node) ->

View file

@ -522,12 +522,17 @@ let translate_node
let program p =
let acc_proc, acc_p_desc =
List.fold_left
(fun (acc_proc,acc_p_desc) p_desc ->
match p_desc with
| Minils.Pnode(node) ->
let (node,proc) = translate_node node in
(proc::acc_proc),((Minils.Pnode(node))::acc_p_desc)
| p -> (acc_proc,p::acc_p_desc))
(fun (acc_proc,acc_p_desc) -> function
| Minils.Pnode(node) as p when node.Minils.n_contract = None ->
(acc_proc,p::acc_p_desc)
| Minils.Pnode(node) as p when node.Minils.n_params <> [] ->
warn "Unsupported@ translation@ of@ parametric@ node@ `%s'@ with@ \
contract@ into@ Z/3Z!" (Names.fullname node.Minils.n_name);
(acc_proc,p::acc_p_desc)
| Minils.Pnode(node) ->
let (node,proc) = translate_node node in
(proc::acc_proc),((Minils.Pnode(node))::acc_p_desc)
| p -> (acc_proc,p::acc_p_desc))
([],[])
p.Minils.p_desc in
let procs = List.rev acc_proc in