removed some stupid warnings.
This commit is contained in:
parent
ee2f5ca443
commit
ef4478e37e
11 changed files with 33 additions and 35 deletions
|
@ -22,9 +22,9 @@ let rec clock_compare ck1 ck2 = match ck1, ck2 with
|
|||
if cr1 <> 0 then cr1 else
|
||||
let cr2 = ident_compare vi1 vi2 in
|
||||
if cr2 <> 0 then cr2 else clock_compare ck1 ck2
|
||||
| Cbase _, _ -> 1
|
||||
| Cbase , _ -> 1
|
||||
|
||||
| Cvar _, Cbase _ -> -1
|
||||
| Cvar _, Cbase -> -1
|
||||
| Cvar _, _ -> 1
|
||||
|
||||
| Con _, _ -> -1
|
||||
|
|
|
@ -204,8 +204,7 @@ let build ac =
|
|||
| Atuple l ->
|
||||
(try
|
||||
node_for_tuple l
|
||||
with Not_found
|
||||
_ -> make ac)
|
||||
with Not_found -> make ac)
|
||||
| _ -> make ac
|
||||
in
|
||||
|
||||
|
|
|
@ -145,7 +145,7 @@ and apply op e_list =
|
|||
let i3 = typing e3 in
|
||||
cseq t1 (cor i2 i3)
|
||||
| ( Efun _| Enode _ | Econcat | Eselect_slice
|
||||
| Eselect_dyn | Eselect_trunc | Eselect _ | Earray_fill) ->
|
||||
| Eselect_dyn | Eselect_trunc | Eselect | Earray_fill) ->
|
||||
ctuplelist (List.map typing e_list)
|
||||
| (Earray | Etuple) ->
|
||||
candlist (List.map typing e_list)
|
||||
|
|
|
@ -81,7 +81,7 @@ let present_handler funs acc ph =
|
|||
if stateful then
|
||||
message ph.p_cond.e_loc Eexp_should_be_stateless;
|
||||
let p_block, acc = Hept_mapfold.block_it funs acc ph.p_block in
|
||||
{ ph with p_cond = p_cond; p_block = p_block }, acc
|
||||
{ p_cond = p_cond; p_block = p_block }, acc
|
||||
|
||||
|
||||
(* Funs with states are rejected, nodes without state are set as funs *)
|
||||
|
|
|
@ -217,7 +217,7 @@ and present_handler_it funs acc ph = funs.present_handler funs acc ph
|
|||
and present_handler funs acc ph =
|
||||
let p_cond, acc = exp_it funs acc ph.p_cond in
|
||||
let p_block, acc = block_it funs acc ph.p_block in
|
||||
{ ph with p_cond = p_cond; p_block = p_block }, acc
|
||||
{ p_cond = p_cond; p_block = p_block }, acc
|
||||
|
||||
and var_dec_it funs acc vd = funs.var_dec funs acc vd
|
||||
and var_dec funs acc vd =
|
||||
|
@ -242,8 +242,7 @@ and contract funs acc c =
|
|||
let c_enforce, acc = exp_it funs acc c.c_enforce in
|
||||
let c_block, acc = block_it funs acc c.c_block in
|
||||
let c_controllables, acc = mapfold (var_dec_it funs) acc c.c_controllables in
|
||||
{ c with
|
||||
c_assume = c_assume;
|
||||
{ c_assume = c_assume;
|
||||
c_enforce = c_enforce;
|
||||
c_block = c_block;
|
||||
c_controllables = c_controllables },
|
||||
|
|
|
@ -211,7 +211,7 @@ and present_handler_it funs acc ph = funs.present_handler funs acc ph
|
|||
and present_handler funs acc ph =
|
||||
let p_cond, acc = exp_it funs acc ph.p_cond in
|
||||
let p_block, acc = block_it funs acc ph.p_block in
|
||||
{ ph with p_cond = p_cond; p_block = p_block }, acc
|
||||
{ p_cond = p_cond; p_block = p_block }, acc
|
||||
|
||||
and var_dec_it funs acc vd = funs.var_dec funs acc vd
|
||||
and var_dec funs acc vd =
|
||||
|
|
|
@ -241,14 +241,14 @@ module Printer =
|
|||
| Attractivity(_) -> failwith("Attractivity verification not allowed")
|
||||
|
||||
let sigali_head = "
|
||||
set_reorder(2);
|
||||
|
||||
read(\"Property.lib\");
|
||||
read(\"Synthesis.lib\");
|
||||
read(\"Verif_Determ.lib\");
|
||||
read(\"Simul.lib\");
|
||||
read(\"Synthesis_Partial_order.lib\");
|
||||
read(\"Orbite.lib\");
|
||||
set_reorder(2);\
|
||||
\
|
||||
read(\"Property.lib\");\
|
||||
read(\"Synthesis.lib\");\
|
||||
read(\"Verif_Determ.lib\");\
|
||||
read(\"Simul.lib\");\
|
||||
read(\"Synthesis_Partial_order.lib\");\
|
||||
read(\"Orbite.lib\");\
|
||||
"
|
||||
|
||||
let sigali_foot = ""
|
||||
|
|
|
@ -137,9 +137,9 @@ struct
|
|||
if cr1 <> 0 then cr1 else
|
||||
let cr2 = ident_compare_modulo vi1 vi2 in
|
||||
if cr2 <> 0 then cr2 else clock_compare ck1 ck2
|
||||
| Cbase _, _ -> 1
|
||||
| Cbase , _ -> 1
|
||||
|
||||
| Cvar _, Cbase _ -> -1
|
||||
| Cvar _, Cbase -> -1
|
||||
| Cvar _, _ -> 1
|
||||
|
||||
| Con _, _ -> -1
|
||||
|
|
|
@ -75,7 +75,7 @@ let is_modified_handlers j e handlers =
|
|||
List.exists (fun x -> is_modified_handlers j x handlers) vars
|
||||
|
||||
let fuse_blocks b1 b2 =
|
||||
{ b1 with b_locals = b1.b_locals @ b2.b_locals;
|
||||
{ b_locals = b1.b_locals @ b2.b_locals;
|
||||
b_body = b1.b_body @ b2.b_body }
|
||||
|
||||
let rec find c = function
|
||||
|
|
|
@ -140,7 +140,7 @@ and block_it funs acc b = funs.block funs acc b
|
|||
and block funs acc b =
|
||||
let b_locals, acc = var_decs_it funs acc b.b_locals in
|
||||
let b_body, acc = mapfold (act_it funs) acc b.b_body in
|
||||
{ b with b_locals = b_locals; b_body = b_body }, acc
|
||||
{ b_locals = b_locals; b_body = b_body }, acc
|
||||
|
||||
and var_dec_it funs acc vd = funs.var_dec funs acc vd
|
||||
and var_dec funs acc vd =
|
||||
|
|
|
@ -237,31 +237,31 @@ let rec map3 f l1 l2 l3 = match l1, l2, l3 with
|
|||
|
||||
exception Assert_false
|
||||
let internal_error passe =
|
||||
Format.eprintf "@.---------@\n
|
||||
Internal compiler error@\n
|
||||
Passe : %s@\n
|
||||
Format.eprintf "@.---------@\n\
|
||||
Internal compiler error@\n\
|
||||
Passe : %s@\n\
|
||||
----------@." passe;
|
||||
raise Assert_false
|
||||
|
||||
exception Unsupported
|
||||
let unsupported passe =
|
||||
Format.eprintf "@.---------@\n
|
||||
Unsupported feature, please report it@\n
|
||||
Passe : %s@\n
|
||||
----------@." passe;
|
||||
Format.eprintf "@.---------@\n\
|
||||
Unsupported feature, please report it@\n\
|
||||
Passe : %s@\n\
|
||||
----------@." passe;
|
||||
raise Unsupported
|
||||
|
||||
(* Functions to decompose a list into a tuple *)
|
||||
let _arity_error i l =
|
||||
Format.eprintf "@.---------@\n
|
||||
Internal compiler error: wrong list size (found %d, expected %d).@\n
|
||||
----------@." (List.length l) i;
|
||||
Format.eprintf "@.---------@\n\
|
||||
Internal compiler error: wrong list size (found %d, expected %d).@\n\
|
||||
----------@." (List.length l) i;
|
||||
raise Assert_false
|
||||
|
||||
let _arity_min_error i l =
|
||||
Format.eprintf "@.---------@\n
|
||||
Internal compiler error: wrong list size (found %d, expected %d at least).@\n
|
||||
----------@." (List.length l) i;
|
||||
Format.eprintf "@.---------@\n\
|
||||
Internal compiler error: wrong list size (found %d, expected %d at least).@\n\
|
||||
----------@." (List.length l) i;
|
||||
raise Assert_false
|
||||
|
||||
let assert_empty = function
|
||||
|
|
Loading…
Reference in a new issue