diff --git a/.ocamlformat b/.ocamlformat
index 3130eeb6152502c709096e85e50cbe43f2e913ce..dbb4a3874a9c74f82f2ccf905418fcfc415661b9 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,4 +1,4 @@
-version=0.18.0
+version=0.19.0
parens-tuple=multi-line-only
wrap-comments=true
cases-exp-indent=2
diff --git a/src/automata.ml b/src/automata.ml
index 67477d4841dc7edee1388ccb8a5d268eefcc472a..715af1ebe3601271df61a97b41d047e1d3f52240 100644
--- a/src/automata.ml
+++ b/src/automata.ml
@@ -88,7 +88,8 @@ let unless_read reads handler =
(* Format.eprintf "unless_reads %s = %a@." handler.hand_state (fprintf_list
~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements reads);
Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list
- ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res); *)
+ ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements
+ res); *)
res
let until_read reads handler =
@@ -381,7 +382,7 @@ let node_of_assign_until nused used node aut_id aut_state handler =
node_gencalls = [];
node_checks = [];
node_asserts = handler.hand_asserts;
- node_stmts = until_eq :: new_output_eqs @ handler.hand_stmts;
+ node_stmts = (until_eq :: new_output_eqs) @ handler.hand_stmts;
node_dec_stateless = false;
node_stateless = None;
node_spec = None;
@@ -544,7 +545,7 @@ let rec expand_decls_rec nused top_decls =
top_decl.top_decl_owner
nd
in
- top_types' @ top_decl' :: expand_decls_rec nused (top_nodes' @ q)
+ top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes' @ q))
| _ ->
top_decl :: expand_decls_rec nused q)
diff --git a/src/backends/Ada/ada_backend_wrapper.ml b/src/backends/Ada/ada_backend_wrapper.ml
index c105bf6de16362c692ad74dddbf59ad3e37fccf1..6f3af04ef52becd7919e2a786a2d130fb5cc1b22 100644
--- a/src/backends/Ada/ada_backend_wrapper.ml
+++ b/src/backends/Ada/ada_backend_wrapper.ml
@@ -111,10 +111,9 @@ let pp_main_adb fmt machine =
let pp_loop fmt =
let args =
pp_state_name
- ::
- List.map
- pp_var_name
- (machine.mstep.step_inputs @ machine.mstep.step_outputs)
+ :: List.map
+ pp_var_name
+ (machine.mstep.step_inputs @ machine.mstep.step_outputs)
in
fprintf
fmt
diff --git a/src/backends/C/c_backend_cmake.ml b/src/backends/C/c_backend_cmake.ml
index ef03dda321cb1e2d6b3880985d9c48f93983c227..7c3d2945ab788121fa46c1ec9e2b715cc94f57ab 100644
--- a/src/backends/C/c_backend_cmake.ml
+++ b/src/backends/C/c_backend_cmake.ml
@@ -53,12 +53,11 @@ let fprintf_dependencies fmt (dep : dep_t list) =
(* Format.eprintf "Adding dependency: %s@." s; *)
fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
("${INC}/io_frontend.c"
- ::
- (* IO functions when a main function is computed *)
- List.map
- (fun (Dep (local, s, _, _)) ->
- (if local then s else Version.include_path ^ "/" ^ s) ^ ".c")
- compiled_dep)
+ :: (* IO functions when a main function is computed *)
+ List.map
+ (fun (Dep (local, s, _, _)) ->
+ (if local then s else Version.include_path ^ "/" ^ s) ^ ".c")
+ compiled_dep)
module type MODIFIERS_MKF = sig
(* dep was (bool * ident * top_decl list) *)
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 31205279c917bbe276c59838385bfeab71ee60fb..6bf4212285cdc64d754291abdb87eb80c94a43e9 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -276,7 +276,8 @@ let pp_basic_c_type ?(pp_c_basic_type_desc = pp_c_basic_type_desc) ?var_opt fmt
| _ ->
fprintf fmt "%s" (pp_c_basic_type_desc t)
-let pp_c_type ?(var_is_contract=false) ?pp_c_basic_type_desc ?var_opt var_id fmt t =
+let pp_c_type ?(var_is_contract = false) ?pp_c_basic_type_desc ?var_opt var_id
+ fmt t =
let rec aux t pp_suffix =
if is_basic_c_type t then
fprintf
@@ -439,7 +440,12 @@ let pp_c_decl_input_var fmt id =
the case for generics *)
let pp_c_decl_output_var fmt id =
if (not !Options.ansi) && Types.is_address_type id.var_type then
- pp_c_type ~var_is_contract:id.var_is_contract ~var_opt:id id.var_id fmt id.var_type
+ pp_c_type
+ ~var_is_contract:id.var_is_contract
+ ~var_opt:id
+ id.var_id
+ fmt
+ id.var_type
else
pp_c_type
~var_is_contract:id.var_is_contract
@@ -937,9 +943,7 @@ module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct
name
(pp_comma_list pp_c_decl_input_var)
inputs
- (pp_comma_list
- ~pp_prologue:pp_print_comma
- pp_c_decl_output_var)
+ (pp_comma_list ~pp_prologue:pp_print_comma pp_c_decl_output_var)
outputs
end
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index b6e91347ad4c3fda06a9db61e17d5c7c9358e1d8..8856b2514a3f7b442ab4818a3b3d8f6c178ea991 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -72,7 +72,8 @@ functor
a predicate: function step and reset are associated to ACSL predicate -
the node is associated to a refinement contract, wrt its ACSL sem - if
the node is a regular node associated to a contract, print the contract
- as function contract. - do not print anything if this is a contract node *)
+ as function contract. - do not print anything if this is a contract
+ node *)
let pp_machine_alloc_decl fmt m =
Mod.pp_machine_decl_prefix fmt m;
if not (fst (get_stateless_status m)) then
@@ -125,7 +126,8 @@ functor
fprintf fmt "extern %a;" pp_stateless_C_prototype prototype
else (
(* TODO: raise proper error *)
- Format.eprintf "internal error: pp_machine_decl_top_decl_from_header";
+ Format.eprintf
+ "internal error: pp_machine_decl_top_decl_from_header";
assert false)
else if inode.nodei_stateless then
fprintf fmt "extern %a;" Protos.pp_stateless_prototype prototype
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 56447ce80d016b9d11fea53e34e3d4f361ae6c74..ba36c690d6d77b7323f9970a8a8d1479a099869c 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -481,7 +481,8 @@ module Main (Mod : MODIFIERS_MAINSRC) = struct
content = [];
is_stateful = true (* assuming it is stateful*);
}
- (* Print the svn version number and the supported C standard (C90 or C99) *)
+ (* Print the svn version number and the supported C standard (C90 or
+ C99) *)
pp_print_version
()
(pp_main_code machines)
diff --git a/src/backends/C/c_backend_makefile.ml b/src/backends/C/c_backend_makefile.ml
index 6db2a679b00d63924ba867e3afbe5c75675af25d..8ad84ab602fcba15af76fd99f29a8d20a58f4e54 100644
--- a/src/backends/C/c_backend_makefile.ml
+++ b/src/backends/C/c_backend_makefile.ml
@@ -63,13 +63,13 @@ let fprintf_dependencies fmt (deps : dep_t list) =
Log.report ~level:1 (fun fmt -> fprintf fmt "Adding dependency: %s@." s);
fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
("${INC}/io_frontend.c"
- ::
- (* IO functions when a main function is computed *)
- List.map
- (fun dep ->
- (if dep.local then dep.name else Version.include_path ^ "/" ^ dep.name)
- ^ ".c")
- compiled_deps)
+ :: (* IO functions when a main function is computed *)
+ List.map
+ (fun dep ->
+ (if dep.local then dep.name
+ else Version.include_path ^ "/" ^ dep.name)
+ ^ ".c")
+ compiled_deps)
module type MODIFIERS_MKF = sig
(* dep was (bool * ident * top_decl list) *)
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index bae653b0917800fc57685c3204616cbb025535cb..9c99cd41ca97870ee1aa9f0ad1aa751fedbbcecd 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -35,14 +35,13 @@ let pp_acsl_basic_type_desc t_desc =
else assert false
(* Not a basic C type. Do not handle arrays or pointers *)
-let pp_acsl pp fmt =
- fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
+let pp_acsl pp fmt = fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp)
let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp
-let pp_acsl_line' ?(ghost=false) pp fmt x =
+let pp_acsl_line' ?(ghost = false) pp fmt x =
let op = if ghost then "" else "*" in
let cl = if ghost then "@" else "*" in
fprintf fmt "/%s%@ @[<h>%a@] %s/" op pp x cl
@@ -109,8 +108,7 @@ let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
let pp_at_pre pp_v fmt v = pp_at pp_v fmt (v, "Pre")
-let find_machine f =
- List.find (fun m -> m.mname.node_id = f)
+let find_machine f = List.find (fun m -> m.mname.node_id = f)
let instances machines m =
let open List in
@@ -242,8 +240,7 @@ let pp_paren pp fmt v = fprintf fmt "(%a)" pp v
let pp_initialization pp_mem fmt (name, mem) =
fprintf fmt "%s_initialization(%a)" name pp_mem mem
-let pp_init pp_mem fmt (name, mem) =
- fprintf fmt "%s_init(%a)" name pp_mem mem
+let pp_init pp_mem fmt (name, mem) = fprintf fmt "%s_init(%a)" name pp_mem mem
let pp_initialization' = pp_initialization pp_print_string
@@ -340,7 +337,8 @@ let pp_transition_aux ?i stateless pp_mem_in pp_mem_out pp_var fmt
vars
(fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
-let pp_transition stateless pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
+let pp_transition stateless pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out)
+ =
pp_transition_aux
?i:t.tindex
stateless
@@ -503,18 +501,15 @@ module PrintSpec = struct
match v.value_desc with
| Var v ->
is_memory m v
- | Array vl
- | Fun (_, vl) ->
+ | Array vl | Fun (_, vl) ->
List.exists has_mem vl
- | Access (t, i)
- | Power (t, i) ->
+ | Access (t, i) | Power (t, i) ->
has_mem t || has_mem i
| _ ->
false
- let has_memory : type a. machine_t -> (value_t, a) expression_t -> bool = fun m -> function
- | Val v -> has_memory_val m v
- | _ -> false
+ let has_memory : type a. machine_t -> (value_t, a) expression_t -> bool =
+ fun m -> function Val v -> has_memory_val m v | _ -> false
let pp_spec mode m =
let rec pp_spec mode fmt f =
@@ -565,13 +560,10 @@ module PrintSpec = struct
if has_memory m b then
let inst = find_arrow m in
pp_paren
- (pp_implies
- (pp_not (pp_initialization pp_access'))
- pp_eq)
+ (pp_implies (pp_not (pp_initialization pp_access')) pp_eq)
fmt
((Arrow.arrow_id, (mem_in, inst)), ())
- else
- pp_eq fmt ()
+ else pp_eq fmt ()
| And fs ->
pp_and_l pp_spec' fmt fs
| Or fs ->
@@ -622,8 +614,8 @@ module PrintSpec = struct
((f, mk_mem_reset m), (rc, tr))
| Value v ->
pp_c_val m mem_in (pp_c_var_read ~test_output:true m) fmt v
-
in
+
pp_spec mode
end
@@ -662,7 +654,9 @@ let pp_memory_pack_def m fmt mp =
let mem = mk_mem m in
pp_acsl_cut
(pp_predicate
- (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
+ (pp_memory_pack
+ (pp_machine_decl' ~ghost:true)
+ (pp_machine_decl pp_ptr))
(PrintSpec.pp_spec MemoryPackMode m))
fmt
((mp, (name, mem), (name, self)), mp.mpformula)
@@ -1008,27 +1002,24 @@ module SrcMod = struct
fmt
()
- let spec_from_contract c =
- Spec_common.red (Imply (c.mc_pre, c.mc_post))
+ let spec_from_contract c = Spec_common.red (Imply (c.mc_pre, c.mc_post))
let pp_contract m fmt c =
PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (spec_from_contract c)
let contract_of machines m =
match m.mspec.mnode_spec with
- | Some spec ->
- begin match spec with
- | Contract c ->
- Some c, None
- | NodeSpec f ->
- let m_f = find_machine f machines in
- begin match m_f.mspec.mnode_spec with
- | Some (Contract c) ->
- Some c, Some m_f
- | _ ->
- None, None
- end
- end
+ | Some spec -> (
+ match spec with
+ | Contract c ->
+ Some c, None
+ | NodeSpec f -> (
+ let m_f = find_machine f machines in
+ match m_f.mspec.mnode_spec with
+ | Some (Contract c) ->
+ Some c, Some m_f
+ | _ ->
+ None, None))
| None ->
None, None
@@ -1046,54 +1037,81 @@ module SrcMod = struct
let rename_var_decl n vd = { vd with var_id = rename n vd.var_id }
let rec rename_value n v =
- { v with value_desc =
- match v.value_desc with
- | Machine_code_types.Var v -> Machine_code_types.Var (rename_var_decl n v)
- | Fun (f, vs) -> Fun (f, List.map (rename_value n) vs)
- | Array vs -> Array (List.map (rename_value n) vs)
- | Access (v1, v2) -> Access (rename_value n v1, rename_value n v2)
- | Power (v1, v2) -> Power (rename_value n v1, rename_value n v2)
- | v -> v
+ {
+ v with
+ value_desc =
+ (match v.value_desc with
+ | Machine_code_types.Var v ->
+ Machine_code_types.Var (rename_var_decl n v)
+ | Fun (f, vs) ->
+ Fun (f, List.map (rename_value n) vs)
+ | Array vs ->
+ Array (List.map (rename_value n) vs)
+ | Access (v1, v2) ->
+ Access (rename_value n v1, rename_value n v2)
+ | Power (v1, v2) ->
+ Power (rename_value n v1, rename_value n v2)
+ | v ->
+ v);
}
- let rename_expression: type a. int -> (value_t, a) expression_t -> (value_t, a) expression_t =
- fun n -> function
- | Val v -> Val (rename_value n v)
- | Var v -> Var (rename_var_decl n v)
- | e -> e
+ let rename_expression :
+ type a. int -> (value_t, a) expression_t -> (value_t, a) expression_t =
+ fun n -> function
+ | Val v ->
+ Val (rename_value n v)
+ | Var v ->
+ Var (rename_var_decl n v)
+ | e ->
+ e
let rename_predicate n = function
| Transition (s, f, inst, i, es, r, mf, mif) ->
Transition (s, f, inst, i, List.map (rename_expression n) es, r, mf, mif)
- | p -> p
+ | p ->
+ p
let rec rename_formula n = function
- | Equal (e1, e2) -> Equal (rename_expression n e1, rename_expression n e2)
- | And fs -> And (List.map (rename_formula n) fs)
- | Or fs -> Or (List.map (rename_formula n) fs)
- | Imply (f1, f2) -> Imply (rename_formula n f1, rename_formula n f2)
- | Exists (xs, f) -> Exists (List.map (rename_var_decl n) xs, rename_formula n f)
- | Forall (xs, f) -> Forall (List.map (rename_var_decl n) xs, rename_formula n f)
- | Ternary (e, t, f) -> Ternary (rename_expression n e, rename_formula n t, rename_formula n f)
- | Predicate p -> Predicate (rename_predicate n p)
- | ExistsMem (x, f1, f2) -> ExistsMem (rename n x, rename_formula n f1, rename_formula n f2)
- | Value v -> Value (rename_value n v)
- | f -> f
-
-
+ | Equal (e1, e2) ->
+ Equal (rename_expression n e1, rename_expression n e2)
+ | And fs ->
+ And (List.map (rename_formula n) fs)
+ | Or fs ->
+ Or (List.map (rename_formula n) fs)
+ | Imply (f1, f2) ->
+ Imply (rename_formula n f1, rename_formula n f2)
+ | Exists (xs, f) ->
+ Exists (List.map (rename_var_decl n) xs, rename_formula n f)
+ | Forall (xs, f) ->
+ Forall (List.map (rename_var_decl n) xs, rename_formula n f)
+ | Ternary (e, t, f) ->
+ Ternary (rename_expression n e, rename_formula n t, rename_formula n f)
+ | Predicate p ->
+ Predicate (rename_predicate n p)
+ | ExistsMem (x, f1, f2) ->
+ ExistsMem (rename n x, rename_formula n f1, rename_formula n f2)
+ | Value v ->
+ Value (rename_value n v)
+ | f ->
+ f
+
let rename_contract n c =
- { c with
+ {
+ c with
mc_pre = rename_formula n c.mc_pre;
- mc_post = rename_formula n c.mc_post; }
+ mc_post = rename_formula n c.mc_post;
+ }
- let but_last l =
- List.(rev (tl (rev l)))
+ let but_last l = List.(rev (tl (rev l)))
- let pp_k_induction_case case m pp_mem_in pp_mem_out pp_vars fmt (n, mem_in, mem_out) =
+ let pp_k_induction_case case m pp_mem_in pp_mem_out pp_vars fmt
+ (n, mem_in, mem_out) =
let name = m.mname.node_id in
let inputs = m.mstep.step_inputs in
let outputs = m.mstep.step_outputs in
- fprintf fmt "%s_%s_%d(@[<hov>%a,@;%a,@;%a@])"
+ fprintf
+ fmt
+ "%s_%s_%d(@[<hov>%a,@;%a,@;%a@])"
name
case
n
@@ -1104,82 +1122,115 @@ module SrcMod = struct
pp_mem_out
mem_out
- let pp_k_induction_base_case m =
- pp_k_induction_case "base" m
+ let pp_k_induction_base_case m = pp_k_induction_case "base" m
- let pp_k_induction_inductive_case m =
- pp_k_induction_case "inductive" m
+ let pp_k_induction_inductive_case m = pp_k_induction_case "inductive" m
let pp_base_cases m fmt (c, m_c, k) =
let name = m.mname.node_id in
+ let name_c = m_c.mname.node_id in
let mem = mk_mem m in
- let mem_in_c = mk_mem_in m_c in
- let mem_out_c = mk_mem_out m_c in
+ let mem_c = mk_mem_c m in
let inputs = m.mstep.step_inputs in
let outputs = m.mstep.step_outputs in
let stateless = fst (get_stateless_status m) in
let stateless_c = fst (get_stateless_status m_c) in
let l = List.init (k - 1) (fun n -> n + 1) in
- pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut
+ pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_sep:pp_print_cutcut
(fun fmt n ->
- let l = List.init (n + 1) (fun n -> n) in
- let l' = List.init n (fun n -> n) in
- let mem_in_c = rename n mem_in_c in
- let mem_out_c = rename n mem_out_c in
- let pp fmt =
- let pp =
- pp_implies
- (pp_and
- (pp_and_l (fun fmt -> function
- | 0 ->
- pp_init pp_print_string fmt (name, rename 0 mem)
- | n ->
- pp_transition_aux stateless pp_print_string pp_print_string pp_var_decl
- fmt
- (name,
- List.map (rename_var_decl n) (inputs @ outputs),
- rename (n - 1) mem,
- rename n mem)))
- (pp_transition_aux stateless_c pp_print_string pp_print_string pp_var_decl))
- (pp_contract m)
- in
- if stateless_c then pp fmt
- else fun x ->
- pp_forall (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
- pp fmt ((m_c.mname.node_id, [mem_in_c; mem_out_c]), x)
- in
- pp_predicate
- (pp_k_induction_base_case
- m
- (pp_machine_decl' ~ghost:true)
- (pp_machine_decl' ~ghost:true)
- (fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl n) xs)))
- (pp_forall (pp_locals m)
- (if n > 1 then
- pp_forall
- (fun fmt l -> fprintf fmt "%a@,%a"
- (pp_machine_decl ~ghost:true
- (pp_comma_list ~pp_eol:pp_print_comma
- (fun fmt n -> pp_print_string fmt (rename n mem))))
- (name, but_last l)
- (pp_locals m)
- (List.flatten
- (List.map (fun n ->
- List.map (rename_var_decl n) (inputs @ outputs))
- (List.tl l))))
- pp
- else
- fun fmt (_, x) -> pp fmt x))
- fmt
- ((n, (name, rename (n - 1) mem), (name, rename n mem)),
- (List.map (rename_var_decl n) m_c.mstep.step_outputs,
- (l', ((l,
- (m_c.mname.node_id,
- List.map (rename_var_decl n) (m_c.mstep.step_inputs @ m_c.mstep.step_outputs),
- mem_in_c, mem_out_c)),
- rename_contract n c)))))
- fmt
- l
+ let l = List.init (n + 1) (fun n -> n) in
+ let pp fmt =
+ let pp =
+ pp_implies
+ (pp_and_l (fun fmt -> function
+ | 0 ->
+ let pp = pp_init pp_print_string in
+ (if stateless_c then fun fmt (x, _) -> pp fmt x
+ else pp_and pp pp)
+ fmt
+ ((name, rename 0 mem), (name_c, rename 0 mem_c))
+ | n' ->
+ let pp_var_c fmt (out, vd) =
+ if out && n' < n then pp_true_c_bool fmt ()
+ else pp_var_decl fmt vd
+ in
+ let c_inputs =
+ List.map
+ (fun v -> false, rename_var_decl n' v)
+ m_c.mstep.step_inputs
+ in
+ let c_outputs =
+ List.map
+ (fun v -> true, rename_var_decl n' v)
+ m_c.mstep.step_outputs
+ in
+ let pp stateless pp_var =
+ pp_transition_aux
+ stateless
+ pp_print_string
+ pp_print_string
+ pp_var
+ in
+ pp_and
+ (pp stateless pp_var_decl)
+ (pp stateless_c pp_var_c)
+ fmt
+ ( ( name,
+ List.map (rename_var_decl n') (inputs @ outputs),
+ rename (n' - 1) mem,
+ rename n' mem ),
+ ( name_c,
+ c_inputs @ c_outputs,
+ rename (n' - 1) mem_c,
+ rename n' mem_c ) )))
+ (pp_contract m)
+ in
+ if stateless_c then pp fmt
+ else fun x ->
+ pp_forall
+ (pp_machine_decl
+ ~ghost:true
+ (pp_comma_list (fun fmt n ->
+ pp_print_string fmt (rename n mem_c))))
+ pp
+ fmt
+ ((name_c, l), x)
+ in
+ pp_predicate
+ (pp_k_induction_base_case
+ m
+ (pp_machine_decl' ~ghost:true)
+ (pp_machine_decl' ~ghost:true)
+ (fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl n) xs)))
+ (pp_forall
+ (pp_locals m)
+ (if n > 1 then
+ pp_forall
+ (fun fmt l ->
+ fprintf
+ fmt
+ "%a@,%a"
+ (pp_machine_decl
+ ~ghost:true
+ (pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
+ pp_print_string fmt (rename n mem))))
+ (name, but_last l)
+ (pp_locals m)
+ (List.flatten
+ (List.map
+ (fun n ->
+ List.map (rename_var_decl n) (inputs @ outputs))
+ (List.tl l))))
+ pp
+ else fun fmt (_, x) -> pp fmt x))
+ fmt
+ ( (n, (name, rename (n - 1) mem), (name, rename n mem)),
+ ( List.map (rename_var_decl n) m_c.mstep.step_outputs,
+ (but_last l, (l, rename_contract n c)) ) ))
+ fmt
+ l
let pp_inductive_case m fmt (c, m_c, k) =
let name = m.mname.node_id in
@@ -1195,29 +1246,47 @@ module SrcMod = struct
let pp =
pp_implies
(pp_and_l (fun fmt n ->
- let pp fmt (out, vd) =
- if out && n < k then pp_true_c_bool fmt () else pp_var_decl fmt vd
+ let pp_var_c fmt (out, vd) =
+ if out && n < k then pp_true_c_bool fmt ()
+ else pp_var_decl fmt vd
+ in
+ let c_inputs =
+ List.map
+ (fun v -> false, rename_var_decl n v)
+ m_c.mstep.step_inputs
+ in
+ let c_outputs =
+ List.map
+ (fun v -> true, rename_var_decl n v)
+ m_c.mstep.step_outputs
in
- let c_inputs = List.map (fun v -> false, rename_var_decl n v) m_c.mstep.step_inputs in
- let c_outputs = List.map (fun v -> true, rename_var_decl n v) m_c.mstep.step_outputs in
pp_and
- (pp_transition_aux stateless pp_print_string pp_print_string pp_var_decl)
- (pp_transition_aux stateless_c pp_print_string pp_print_string pp)
+ (pp_transition_aux
+ stateless
+ pp_print_string
+ pp_print_string
+ pp_var_decl)
+ (pp_transition_aux
+ stateless_c
+ pp_print_string
+ pp_print_string
+ pp_var_c)
fmt
- ((name,
- List.map (rename_var_decl n) (inputs @ outputs),
- rename (n - 1) mem,
- rename n mem),
- (m_c.mname.node_id,
- c_inputs @ c_outputs,
- rename (n - 1) mem_c,
- rename n mem_c))))
+ ( ( name,
+ List.map (rename_var_decl n) (inputs @ outputs),
+ rename (n - 1) mem,
+ rename n mem ),
+ ( m_c.mname.node_id,
+ c_inputs @ c_outputs,
+ rename (n - 1) mem_c,
+ rename n mem_c ) )))
(pp_contract m)
in
if stateless_c then pp fmt
else fun x ->
pp_forall
- (pp_machine_decl ~ghost:true
+ (pp_machine_decl
+ ~ghost:true
(pp_comma_list (fun fmt n -> pp_print_string fmt (rename n mem_c))))
pp
fmt
@@ -1229,26 +1298,31 @@ module SrcMod = struct
(pp_machine_decl' ~ghost:true)
(pp_machine_decl' ~ghost:true)
(fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl k) xs)))
- (pp_forall (pp_locals m)
+ (pp_forall
+ (pp_locals m)
(if k > 1 then
- pp_forall
- (fun fmt l -> fprintf fmt "%a@,%a"
- (pp_machine_decl ~ghost:true
- (pp_comma_list ~pp_eol:pp_print_comma
- (fun fmt n -> pp_print_string fmt (rename (n - 1) mem))))
- (name, but_last l)
- (pp_locals m)
- (List.flatten
- (List.map (fun n ->
- List.map (rename_var_decl (n - 1)) (inputs @ outputs))
- (List.tl l))))
- pp
- else
- fun fmt (_, x) -> pp fmt x))
+ pp_forall
+ (fun fmt l ->
+ fprintf
+ fmt
+ "%a@,%a"
+ (pp_machine_decl
+ ~ghost:true
+ (pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
+ pp_print_string fmt (rename (n - 1) mem))))
+ (name, but_last l)
+ (pp_locals m)
+ (List.flatten
+ (List.map
+ (fun n ->
+ List.map (rename_var_decl (n - 1)) (inputs @ outputs))
+ (List.tl l))))
+ pp
+ else fun fmt (_, x) -> pp fmt x))
fmt
- ((k, (name, rename (k - 1) mem), (name, rename k mem)),
- (List.map (rename_var_decl k) m_c.mstep.step_outputs,
- (l, (l, rename_contract k c))))
+ ( (k, (name, rename (k - 1) mem), (name, rename k mem)),
+ ( List.map (rename_var_decl k) m_c.mstep.step_outputs,
+ (l, (l, rename_contract k c)) ) )
let pp_k_induction_lemmas m fmt k =
let name = m.mname.node_id in
@@ -1257,26 +1331,29 @@ module SrcMod = struct
let inputs = m.mstep.step_inputs in
let outputs = m.mstep.step_outputs in
let l = List.init k (fun n -> n + 1) in
- pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut
+ pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_sep:pp_print_cutcut
(fun fmt n ->
- pp_lemma
- (fun fmt n -> fprintf fmt "%s_k_induction_%d" name n)
- (pp_forall
- (fun fmt () -> fprintf fmt "%a,@;%a"
- (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
- (name, [mem_in; mem_out])
- (pp_locals m)
- (inputs @ outputs))
- ((if n = k then
- pp_k_induction_inductive_case
- else
- pp_k_induction_base_case)
- m
- pp_print_string
- pp_print_string
- (pp_comma_list pp_var_decl)))
- fmt
- (n, ((), (n, mem_in, mem_out))))
+ pp_lemma
+ (fun fmt n -> fprintf fmt "%s_k_induction_%d" name n)
+ (pp_forall
+ (fun fmt () ->
+ fprintf
+ fmt
+ "%a,@;%a"
+ (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
+ (name, [ mem_in; mem_out ])
+ (pp_locals m)
+ (inputs @ outputs))
+ ((if n = k then pp_k_induction_inductive_case
+ else pp_k_induction_base_case)
+ m
+ pp_print_string
+ pp_print_string
+ (pp_comma_list pp_var_decl)))
+ fmt
+ (n, ((), (n, mem_in, mem_out))))
fmt
l
@@ -1288,61 +1365,88 @@ module SrcMod = struct
let mem_out_c = mk_mem_out_c m_c in
let inputs = m.mstep.step_inputs in
let outputs = m.mstep.step_outputs in
+ let stateless = fst (get_stateless_status m) in
let stateless_c = fst (get_stateless_status m_c) in
let l = List.init k (fun n -> n + 1) in
let pp =
pp_implies
- (pp_and
- (pp_and_l
- (fun fmt n ->
- (if n = k then
- pp_k_induction_inductive_case
- else
- pp_k_induction_base_case)
- m
- pp_print_string
- pp_print_string
- (pp_comma_list pp_var_decl)
- fmt
- (n, mem_in, mem_out)))
- (pp_transition_aux stateless_c pp_print_string pp_print_string pp_var_decl))
- (pp_contract m)
+ (pp_and_l (fun fmt n ->
+ (if n = k then pp_k_induction_inductive_case
+ else pp_k_induction_base_case)
+ m
+ pp_print_string
+ pp_print_string
+ (pp_comma_list pp_var_decl)
+ fmt
+ (n, mem_in, mem_out)))
+ (pp_forall
+ (pp_locals m)
+ (pp_implies
+ (pp_and
+ (pp_transition_aux
+ stateless
+ pp_print_string
+ pp_print_string
+ pp_var_decl)
+ (pp_transition_aux
+ stateless_c
+ pp_print_string
+ pp_print_string
+ pp_var_decl))
+ (pp_contract m)))
in
pp_axiomatic
(fun fmt () -> fprintf fmt "%s_k_Induction" name)
(pp_axiom
(fun fmt () -> fprintf fmt "%s_k_induction" name)
(pp_forall
- (pp_locals m)
- (pp_forall
- (fun fmt () -> fprintf fmt "%a,@;%a"
- (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
- (name, [mem_in; mem_out])
- (pp_locals m)
- (inputs @ outputs))
- (if stateless_c then pp else
- fun fmt x ->
- pp_forall (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
- pp fmt ((m_c.mname.node_id, [mem_in_c; mem_out_c]), x)))))
+ (fun fmt () ->
+ fprintf
+ fmt
+ "%a,@;%a"
+ (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
+ (name, [ mem_in; mem_out ])
+ (pp_locals m)
+ (inputs @ outputs))
+ (if stateless_c then pp
+ else fun fmt x ->
+ pp_forall
+ (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
+ pp
+ fmt
+ ((m_c.mname.node_id, [ mem_in_c; mem_out_c ]), x))))
fmt
- ((),
- ((),
- (m_c.mstep.step_outputs,
- ((),
- (((l,
- (m_c.mname.node_id,
- m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
- mem_in_c, mem_out_c)), c))))))
-
-
- let pp_k_induction m fmt (_, _, k as c_m_k) =
+ ( (),
+ ( (),
+ ( (),
+ ( l,
+ ( m_c.mstep.step_outputs,
+ ( ( (name, inputs @ outputs, mem_in, mem_out),
+ ( m_c.mname.node_id,
+ m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
+ mem_in_c,
+ mem_out_c ) ),
+ c ) ) ) ) ) )
+
+ let pp_k_induction m fmt ((_, m_c, k) as c_m_k) =
+ let stateless_c = fst (get_stateless_status m_c) in
pp_acsl_cut
- (fun fmt () -> fprintf fmt "%a@,@,%a@,@,%a@,@,%a@,@,%a"
- pp_init_def m
- (pp_base_cases m) c_m_k
- (pp_inductive_case m) c_m_k
- (pp_k_induction_lemmas m) k
- (pp_k_induction_axiom m) c_m_k)
+ (fun fmt () ->
+ fprintf
+ fmt
+ "%a@,@,%a@,@,%a@,@,%a@,@,%a@,@,%a"
+ pp_init_def
+ m
+ (if stateless_c then pp_print_nothing else pp_init_def)
+ m_c
+ (pp_base_cases m)
+ c_m_k
+ (pp_inductive_case m)
+ c_m_k
+ (pp_k_induction_lemmas m)
+ k
+ (pp_k_induction_axiom m)
+ c_m_k)
fmt
()
@@ -1354,7 +1458,8 @@ module SrcMod = struct
match m_c with
| Some m_c ->
pp_print_option (pp m_c) fmt c.mc_proof
- | None -> ()
+ | None ->
+ ()
let pp_step_spec fmt machines self mem m =
let name = m.mname.node_id in
@@ -1369,33 +1474,62 @@ module SrcMod = struct
let inputs = m.mstep.step_inputs in
let outputs = m.mstep.step_outputs in
let stateless = fst (get_stateless_status m) in
- let pp_if_outputs pp =
- if outputs = [] then pp_print_nothing else pp
- in
+ let pp_if_outputs pp = if outputs = [] then pp_print_nothing else pp in
let c, m_c = contract_of machines m in
- (* (\* prevent printing an ensures clause with contract name *\)
- * let spec =
- * match m.mspec.mnode_spec with
- * | Some (NodeSpec _) -> None
- * | s -> s
- * in *)
- let pp_spec = pp_print_option
- (if m.mis_contract then pp_print_nothing else pp_ensures (pp_contract m)) in
- let pp_spec_vars, pp_assigns_spec_vars =
- match m.mspec.mnode_spec with
- | Some (NodeSpec f) ->
- let m_f = find_machine f machines in
+ let pp_spec =
+ pp_print_option
+ (if m.mis_contract then pp_print_nothing
+ else fun fmt c ->
+ pp_print_option
+ (fun fmt m_c ->
+ let mem_in = mk_mem_in_c m_c in
+ let mem_out = mk_mem_out_c m_c in
+ let stateless_c = fst (get_stateless_status m_c) in
+ pp_ensures
+ (pp_implies
+ (pp_transition_aux
+ stateless_c
+ pp_print_string
+ pp_print_string
+ (fun fmt v ->
+ (if is_output m v then pp_ptr_decl else pp_var_decl)
+ fmt
+ v))
+ (pp_contract m))
+ fmt
+ ( ( m_c.mname.node_id,
+ m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
+ mem_in,
+ mem_out ),
+ c ))
+ fmt
+ m_c)
+ in
+ let pp_spec_vars =
+ match m_c with
+ | Some m_c ->
+ let mem_in = mk_mem_in_c m_c in
+ let mem_out = mk_mem_out_c m_c in
+ let stateless_c = fst (get_stateless_status m_c) in
pp_acsl_cut
- (pp_ghost
- (fun fmt () ->
- fprintf
- fmt
- "@;<0 2>@[<v>%a@]"
- (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon
- ~pp_eol:pp_print_semicolon (pp_c_decl_local_var m))
- m_f.mstep.step_outputs)),
- fun fmt () -> pp_assigns pp_var_decl fmt m_f.mstep.step_outputs
- | _ -> pp_print_nothing, pp_print_nothing
+ (pp_ghost (fun fmt () ->
+ fprintf
+ fmt
+ "@;<0 2>@[<v>%a%a@]"
+ (pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_sep:pp_print_semicolon
+ ~pp_eol:pp_print_semicolon
+ (pp_c_decl_local_var m))
+ m_c.mstep.step_outputs
+ (if stateless_c then pp_print_nothing
+ else
+ pp_machine_decl
+ ~ghost:true
+ (pp_comma_list ~pp_eol:pp_print_semicolon pp_print_string))
+ (m_c.mname.node_id, [ mem_in; mem_out ])))
+ | _ ->
+ pp_print_nothing
in
pp_print_option (pp_proof_annotation m m_c) fmt c;
pp_spec_vars fmt ();
@@ -1404,12 +1538,11 @@ module SrcMod = struct
if stateless then
fprintf
fmt
- "%a@,%a@,%a@,%a@,%a@,%a"
+ "%a@,%a@,%a@,%a@,%a"
(pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
outputs
(pp_if_outputs (pp_requires pp_separated''))
outputs
- pp_assigns_spec_vars ()
(pp_assigns pp_ptr_decl)
outputs
(pp_ensures (pp_transition_aux' m))
@@ -1419,7 +1552,24 @@ module SrcMod = struct
else
fprintf
fmt
- "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
+ "%a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a@,\
+ %a"
(pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
outputs
(pp_requires pp_mem_valid')
@@ -1436,7 +1586,6 @@ module SrcMod = struct
(name, inputs @ outputs, mem, mem)
pp_spec
c
- pp_assigns_spec_vars ()
(pp_assigns pp_ptr_decl)
outputs
(pp_assigns (pp_reg self))
@@ -1493,7 +1642,9 @@ module SrcMod = struct
(pp_print_list
~pp_open_box:pp_open_vbox0
~pp_prologue:pp_print_cut
- (pp_acsl_line' ~ghost (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
+ (pp_acsl_line'
+ ~ghost
+ (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
instr.instr_spec
let pp_ghost_parameter mem fmt inst =
@@ -1510,31 +1661,28 @@ module SrcMod = struct
let pp_vars ?pp_eol = pp_comma_list ?pp_eol (pp_c_var_read m) in
match contract_of machines m with
| Some c, Some _ ->
- pp_acsl_cut
- (pp_print_option
- (fun fmt -> function
- | Kinduction k ->
- let l = List.init k (fun n -> n + 1) in
- let pp_mem_in = pp_at_pre pp_ptr in
- let pp_mem_out = pp_ptr in
- pp_assert
- (pp_and_l
- (fun fmt n ->
- (if n = k then
- pp_k_induction_inductive_case
- else
- pp_k_induction_base_case)
- m
- pp_mem_in
- pp_mem_out
- pp_vars
- fmt
- (n, mem, mem)))
- fmt
- l))
- fmt c.mc_proof
- | _, _ -> ()
-
+ pp_print_option
+ (pp_acsl_cut (fun fmt -> function
+ | Kinduction k ->
+ let l = List.init k (fun n -> n + 1) in
+ let pp_mem_in = pp_at_pre pp_ptr in
+ let pp_mem_out = pp_ptr in
+ pp_assert
+ (pp_and_l (fun fmt n ->
+ (if n = k then pp_k_induction_inductive_case
+ else pp_k_induction_base_case)
+ m
+ pp_mem_in
+ pp_mem_out
+ pp_vars
+ fmt
+ (n, mem, mem)))
+ fmt
+ l))
+ fmt
+ c.mc_proof
+ | _, _ ->
+ ()
end
module MainMod = struct
@@ -1578,9 +1726,7 @@ module MainMod = struct
(pp_ref pp_var_decl)))
(main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
(pp_loop_invariant
- (pp_or
- (pp_valid_read pp_stdout)
- (pp_equal pp_stdout pp_null)))
+ (pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
((), ((), ())))
fmt
()
@@ -1592,9 +1738,7 @@ module MainMod = struct
fmt
"%a@,%a@,%a@,%a"
(pp_requires
- (pp_or
- (pp_valid_read pp_stdout)
- (pp_equal pp_stdout pp_null)))
+ (pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
((), ((), ()))
(pp_terminates pp_false)
()
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index ea08cefab6a93840cdec395b07f83de5a557027d..e18655d2a2501bf3de900b3d0307b57428ff332f 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -35,7 +35,8 @@ module type MODIFIERS_SRC = sig
val pp_ghost_parameter : ident -> formatter -> ident option -> unit
- val pp_contract : formatter -> machine_t list -> ident -> ident -> machine_t -> unit
+ val pp_contract :
+ formatter -> machine_t list -> ident -> ident -> machine_t -> unit
end
module EmptyMod = struct
@@ -323,12 +324,12 @@ module Main (Mod : MODIFIERS_SRC) = struct
i
(pp_print_parenthesized (pp_c_val m self (pp_c_var_read m)))
vl
- | MStep (il, i, vl) ->
- begin match List.assoc_opt i m.minstances with
- | Some (td, _) when Arrow.td_is_arrow td ->
- pp_arrow_call m self mem fmt i il
- | _ -> pp_basic_instance_call m self mem fmt i vl il
- end
+ | MStep (il, i, vl) -> (
+ match List.assoc_opt i m.minstances with
+ | Some (td, _) when Arrow.td_is_arrow td ->
+ pp_arrow_call m self mem fmt i il
+ | _ ->
+ pp_basic_instance_call m self mem fmt i vl il)
| MBranch (_, []) ->
eprintf
"internal error: C_backend_src.pp_machine_instr %a@."
@@ -544,9 +545,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
check
let pp_print_function ~pp_prototype ~prototype ?(is_contract = false)
- ?(pp_spec = pp_print_nothing)
- ?(pp_local = pp_print_nothing) ?(base_locals = [])
- ?(pp_array_mem = pp_print_nothing) ?(array_mems = [])
+ ?(pp_spec = pp_print_nothing) ?(pp_local = pp_print_nothing)
+ ?(base_locals = []) ?(pp_array_mem = pp_print_nothing) ?(array_mems = [])
?(pp_init_mpfr_local = pp_print_nothing)
?(pp_clear_mpfr_local = pp_print_nothing) ?(mpfr_locals = [])
?(pp_check = pp_print_nothing) ?(checks = [])
@@ -1004,7 +1004,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
content = [];
is_stateful = true (* assuming it is stateful *);
}
- (* Print the svn version number and the supported C standard (C90 or C99) *)
+ (* Print the svn version number and the supported C standard (C90 or
+ C99) *)
pp_print_version
()
(* Print dependencies *)
diff --git a/src/backends/C/c_backend_src.mli b/src/backends/C/c_backend_src.mli
index 0ffb3c7a3d8ea0cdbae8fae767e358aa050b0477..5128dab2f37ae460411c3c19a1451a251b6591fa 100644
--- a/src/backends/C/c_backend_src.mli
+++ b/src/backends/C/c_backend_src.mli
@@ -21,7 +21,8 @@ module type MODIFIERS_SRC = sig
val pp_ghost_parameter : ident -> formatter -> ident option -> unit
- val pp_contract : formatter -> machine_t list -> ident -> ident -> machine_t -> unit
+ val pp_contract :
+ formatter -> machine_t list -> ident -> ident -> machine_t -> unit
end
module EmptyMod : MODIFIERS_SRC
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index eb7588884a32722b161625d689852328dcbb2232..fc176afce3e3e1cdcffb107f8a77e91f2aa5671a 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -387,7 +387,8 @@ let rec pp_machine_instr machines reset_instances (m : machine_t) fmt instr :
other did. Am I clear ? *)
(* For each branch we obtain the logical encoding, and the information
whether a sub node has been reset or not. If a node has been reset in one
- of the branch, then all others have to have the mem_m = mem_c statement. *)
+ of the branch, then all others have to have the mem_m = mem_c
+ statement. *)
let self = m.mname.node_id in
let pp_branch fmt (tag, instrs) =
fprintf
diff --git a/src/backends/Horn/horn_backend_traces.ml b/src/backends/Horn/horn_backend_traces.ml
index 877c817723a2b1198a14d782e0fc95b526eec269..afbba34191a3652b9e252323842556d5678229db 100644
--- a/src/backends/Horn/horn_backend_traces.ml
+++ b/src/backends/Horn/horn_backend_traces.ml
@@ -53,7 +53,8 @@ let machines_traces machines =
let filtered =
List.filter (fun (kwds, _) -> kwds = [ "traceability" ]) all_annots
in
- (* List.iter (eprintf "Annots: %a@." Printers.pp_expr_annot) (m.mannot); *)
+ (* List.iter (eprintf "Annots: %a@." Printers.pp_expr_annot)
+ (m.mannot); *)
let content = List.map snd filtered in
(* Elements are supposed to be a pair (tuple): variable, expression *)
List.map
diff --git a/src/backends/backends.ml b/src/backends/backends.ml
index 7032edee99ac0dc17216196bff6999c390164e9a..d571863a684405d8784fc3f856fc7908a5b9d47e 100644
--- a/src/backends/backends.ml
+++ b/src/backends/backends.ml
@@ -5,7 +5,8 @@ let setup () =
if !Options.output = Options.OutEMF then (
(* Not merging branches *)
join_guards := false;
- (* In case of a default "int" type, substitute it with the legal int32 value *)
+ (* In case of a default "int" type, substitute it with the legal int32
+ value *)
if !Options.int_type = "int" then Options.int_type := "int32");
if !Options.optimization < 0 then join_guards := false
diff --git a/src/causality.ml b/src/causality.ml
index 243447ff3df7ac7c933df435cbfe0d998a85ce2d..d02e2cb0d66ab426a027802941cee193479bbc47 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -206,7 +206,8 @@ module ExprDep = struct
(* mem/mem in g' *)
(* match (lhs_is_mem, ISet.mem x mems) with | (false, true ) -> (add_edges [x]
lhs g, g') | (false, false) -> (add_edges lhs [x] g, g') | (true , false)
- -> (add_edges lhs [x] g, g') | (true , true ) -> (g, add_edges [x] lhs g') *)
+ -> (add_edges lhs [x] g, g') | (true , true ) -> (g, add_edges [x] lhs
+ g') *)
let add_eq_dependencies mems inputs node_vars eq (g, g') =
let add_var lhs_is_mem lhs x (g, g') =
if is_instance_var x || ISet.mem x node_vars then
@@ -590,7 +591,8 @@ module CycleDetection = struct
(* Breaks cycles of the dependency graph [g] of memory variables [mems]
belonging in node [node]. Returns: - a list of new auxiliary variable
- declarations - a list of new equations - a modified acyclic version of [g] *)
+ declarations - a list of new equations - a modified acyclic version of
+ [g] *)
let break_cycles node mems g =
let eqs, auts = get_node_eqs node in
assert (auts = []);
diff --git a/src/checks/algebraicLoop.ml b/src/checks/algebraicLoop.ml
index 116425968cc9844ef99a0f30442ed534acebfb20..4927fa24b5293386dd44aafb70caa6ea68e58d8c 100644
--- a/src/checks/algebraicLoop.ml
+++ b/src/checks/algebraicLoop.ml
@@ -327,7 +327,8 @@ let clean_al prog : program_t * bool * report =
| Node nd -> (
let error, max_inlines =
try
- (* without exception the node is schedulable; nothing to declare *)
+ (* without exception the node is schedulable; nothing to
+ declare *)
let _ = Scheduling.schedule_node nd in
None, max_inlines
with Causality.Error (Causality.DataCycle partitions) ->
diff --git a/src/checks/liveness.ml b/src/checks/liveness.ml
index 1eea77127d0ed06ba0e577e5f3fc426796140103..ab45bf3d4493a30cb28e2721063f489a6e69588f 100644
--- a/src/checks/liveness.ml
+++ b/src/checks/liveness.ml
@@ -48,7 +48,8 @@ let pp_fanin fmt fanin =
Hashtbl.iter (fun s t -> Format.fprintf fmt "@ %s -> %d" s t) fanin;
Format.fprintf fmt "@]@ }@]"
-(* computes the cone of influence of a given [var] wrt a dependency graph [g]. *)
+(* computes the cone of influence of a given [var] wrt a dependency graph
+ [g]. *)
let cone_of_influence g var =
(*Format.printf "DEBUG coi: %s@." var;*)
let frontier = ref (ISet.add var ISet.empty) in
diff --git a/src/checks/stateless.ml b/src/checks/stateless.ml
index 80d67e0380f683929e0d34cd55630a392d98c46e..7e52b48cbfd54715a2519d6d4ef66b87f7e68c6a 100644
--- a/src/checks/stateless.ml
+++ b/src/checks/stateless.ml
@@ -62,8 +62,7 @@ let rec check_expr expr =
i);
check_expr e' && reset_opt && stateless_node
-and check_eexpr e =
- check_expr e.eexpr_qfexpr
+and check_eexpr e = check_expr e.eexpr_qfexpr
and compute_node nd =
(* returns true iff the node is stateless.*)
@@ -76,18 +75,14 @@ and compute_contract nd =
let c = node_as_contract nd in
let eqs, aut = get_contract_eqs c in
aut = []
- && (* A node containinig an automaton will be stateful *)
- List.for_all (fun eq -> check_expr eq.eq_rhs) eqs
- &&
- List.for_all check_eexpr c.assume
- &&
- List.for_all check_eexpr c.guarantees
+ (* A node containinig an automaton will be stateful *)
+ && List.for_all (fun eq -> check_expr eq.eq_rhs) eqs
+ && List.for_all check_eexpr c.assume
+ && List.for_all check_eexpr c.guarantees
and compute_node_or_contract nd =
match nd.node_spec, nd.node_iscontract with
- | None, false
- | Some (NodeSpec _), false
- | Some (Contract _), false ->
+ | None, false | Some (NodeSpec _), false | Some (Contract _), false ->
compute_node nd
| Some (Contract _), true ->
compute_contract nd
@@ -96,23 +91,22 @@ and compute_node_or_contract nd =
and check_node td =
match td.top_decl_desc with
- | Node nd ->
- begin match nd.node_stateless with
- | None ->
- let stateless = compute_node_or_contract nd in
- nd.node_stateless <- Some stateless;
- if stateless
- then (if not nd.node_dec_stateless
- then Log.report ~level:2 (fun fmt ->
- Format.fprintf fmt "%s: node -> function@;" nd.node_id))
- else if nd.node_dec_stateless
- then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id));
- nd.node_dec_stateless <- stateless;
- stateless
- | Some stl ->
- stl
- end
-| ImportedNode nd ->
+ | Node nd -> (
+ match nd.node_stateless with
+ | None ->
+ let stateless = compute_node_or_contract nd in
+ nd.node_stateless <- Some stateless;
+ if stateless then (
+ if not nd.node_dec_stateless then
+ Log.report ~level:2 (fun fmt ->
+ Format.fprintf fmt "%s: node -> function@;" nd.node_id))
+ else if nd.node_dec_stateless then
+ raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id));
+ nd.node_dec_stateless <- stateless;
+ stateless
+ | Some stl ->
+ stl)
+ | ImportedNode nd ->
if nd.nodei_prototype = Some "C" && not nd.nodei_stateless then
raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id));
nd.nodei_stateless
diff --git a/src/clocks.ml b/src/clocks.ml
index d90a8492624e3564884aedc47d465bb3935517e0..d0d4abf44a97fcf4896423f16e96ac1070e958ac 100644
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -38,7 +38,8 @@ and carrier_expr = {
type t = { mutable cdesc : clock_desc; mutable cscoped : bool; cid : int }
-(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
+(* pck stands for periodic clock. Easier not to separate pck from other
+ clocks *)
and clock_desc =
| Carrow of t * t
| Ctuple of t list
@@ -205,8 +206,10 @@ let split_arrow ck =
(** Returns the clock corresponding to a clock list. *)
let clock_of_clock_list = function
- | [ck] -> ck
- | ckl -> new_ck (Ctuple ckl) true
+ | [ ck ] ->
+ ck
+ | ckl ->
+ new_ck (Ctuple ckl) true
let clock_list_of_clock ck =
match (repr ck).cdesc with Ctuple cl -> cl | _ -> [ ck ]
diff --git a/src/clocks.mli b/src/clocks.mli
index 9d9658a92637bd91242412a27b2b534990244973..2272fbe657af1c06ec93d8993d65eba7f411f2a9 100644
--- a/src/clocks.mli
+++ b/src/clocks.mli
@@ -17,7 +17,8 @@ and carrier_expr = {
type t = { mutable cdesc : clock_desc; mutable cscoped : bool; cid : int }
-(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
+(* pck stands for periodic clock. Easier not to separate pck from other
+ clocks *)
and clock_desc =
| Carrow of t * t
| Ctuple of t list
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index 91d5b00f3a19e6788460fa5c2b7a4507b5e11278..19d91e06c9ee3958ef8bacbb788ae532f765c2df 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -73,8 +73,9 @@ let expand_automata decls =
let check_stateless_decls decls =
Log.report ~level:1 (fun fmt ->
fprintf fmt "@ @[<v 2>.. checking stateless/stateful status@ ");
- try (Stateless.check_prog decls;
- Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ "))
+ try
+ Stateless.check_prog decls;
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ")
with Stateless.Error (loc, err) as exc ->
eprintf
"Stateless status error: %a%a@."
@@ -250,7 +251,7 @@ let resolve_contracts prog =
let in_assigns = mk_def imp_in import.inputs in
let out_assigns = mk_def imp_out import.outputs in
let stmts =
- in_assigns :: out_assigns :: imp_nd.node_stmts @ stmts
+ (in_assigns :: out_assigns :: imp_nd.node_stmts) @ stmts
in
let c = merge_contracts c imp_c in
stmts, locals, c
@@ -309,33 +310,31 @@ let resolve_contracts prog =
false)
(accu_contracts @ prog)
in
- let nd = {
- node_id = mk_new_name used (id ^ "_contract");
- node_type = Types.new_var ();
- node_clock = Clocks.new_var true;
- node_inputs = inputs @ outputs;
- node_outputs = [];
- node_locals;
- node_gencalls = [];
- node_checks = [];
- node_asserts = [];
- node_stmts;
- node_dec_stateless = false;
- node_stateless = None;
- node_spec = Some (Contract c);
- node_annot = [];
- node_iscontract = true;
- } in
+ let nd =
+ {
+ node_id = mk_new_name used (id ^ "_contract");
+ node_type = Types.new_var ();
+ node_clock = Clocks.new_var true;
+ node_inputs = inputs @ outputs;
+ node_outputs = [];
+ node_locals;
+ node_gencalls = [];
+ node_checks = [];
+ node_asserts = [];
+ node_stmts;
+ node_dec_stateless = false;
+ node_stateless = None;
+ node_spec = Some (Contract c);
+ node_annot = [];
+ node_iscontract = true;
+ }
+ in
(* let stateless = Stateless.compute_node nd in *)
- mktop_decl
- c.spec_loc
- top.top_decl_owner
- top.top_decl_itf
- (Node nd)
- (* { nd with
- * node_dec_stateless = stateless;
- * node_stateless = Some stateless;
- * }) *)
+ mktop_decl c.spec_loc top.top_decl_owner top.top_decl_itf (Node nd)
+ (* { nd with
+ * node_dec_stateless = stateless;
+ * node_stateless = Some stateless;
+ * }) *)
in
(* Processing nodes in order. Should have been sorted by now
@@ -427,4 +426,3 @@ let update_vdecl_parents_prog prog =
| _ ->
())
prog
-
diff --git a/src/compiler_common.mli b/src/compiler_common.mli
index 9aa995651395a8840a57ac8da42e58c527f3d01f..5b686c315d8033bc647e77487112253a4b4e0629 100644
--- a/src/compiler_common.mli
+++ b/src/compiler_common.mli
@@ -28,4 +28,3 @@ val clock_decls : Clocks.t Env.t -> program_t -> Clocks.t Env.t
val create_dest_dir : unit -> unit
val track_exception : unit -> unit
-
diff --git a/src/corelang.ml b/src/corelang.ml
index 4b78ff1f08a4dd6fcee9e9da7c4371df128e2940..fe2c56fb1ce84c7c3a4e74675adfd12b28952f7a 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -53,7 +53,7 @@ let mktyp loc d = { ty_dec_desc = d; ty_dec_loc = loc }
let mkclock loc d = { ck_dec_desc = d; ck_dec_loc = loc }
-let mkvar_decl loc ?(var_is_contract=false) ?(orig = false)
+let mkvar_decl loc ?(var_is_contract = false) ?(orig = false)
(id, ty_dec, ck_dec, is_const, value, parentid) =
assert (value = None || is_const);
{
@@ -67,7 +67,7 @@ let mkvar_decl loc ?(var_is_contract=false) ?(orig = false)
var_type = Types.new_var ();
var_clock = Clocks.new_var true;
var_loc = loc;
- var_is_contract
+ var_is_contract;
}
let dummy_var_decl name typ =
@@ -122,12 +122,7 @@ let mkeq loc (lhs, rhs) = { eq_lhs = lhs; eq_rhs = rhs; eq_loc = loc }
let mkassert loc expr = { assert_loc = loc; assert_expr = expr }
let mktop_decl top_decl_loc top_decl_owner top_decl_itf top_decl_desc =
- {
- top_decl_desc;
- top_decl_loc;
- top_decl_owner;
- top_decl_itf;
- }
+ { top_decl_desc; top_decl_loc; top_decl_owner; top_decl_itf }
let mkpredef_call loc funname args =
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
@@ -193,7 +188,7 @@ let empty_contract =
modes = [];
imports = [];
spec_loc = Location.dummy;
- proof = None
+ proof = None;
}
(* For const declaration we do as for regular lustre node. But for local flows
@@ -219,7 +214,7 @@ let mk_contract_guarantees name eexpr proof =
empty_contract with
guarantees = [ eexpr_add_name eexpr name ];
spec_loc = eexpr.eexpr_loc;
- proof
+ proof;
}
let mk_contract_assume name eexpr =
@@ -245,14 +240,16 @@ let mk_contract_import id ins outs loc =
}
let merge_proofs p1 p2 =
- let merge_proofs p1 p2 = match p1, p2 with
- | Kinduction k1, Kinduction k2 ->
- Kinduction (max k1 k2)
+ let merge_proofs p1 p2 =
+ match p1, p2 with Kinduction k1, Kinduction k2 -> Kinduction (max k1 k2)
in
match p1, p2 with
- | Some p1, Some p2 -> Some (merge_proofs p1 p2)
- | Some p, None | None, Some p -> Some p
- | None, None -> None
+ | Some p1, Some p2 ->
+ Some (merge_proofs p1 p2)
+ | Some p, None | None, Some p ->
+ Some p
+ | None, None ->
+ None
let merge_contracts ann1 ann2 =
(* keeping the first item loc *)
@@ -265,7 +262,7 @@ let merge_contracts ann1 ann2 =
modes = ann1.modes @ ann2.modes;
imports = ann1.imports @ ann2.imports;
spec_loc = ann1.spec_loc;
- proof = merge_proofs ann1.proof ann2.proof
+ proof = merge_proofs ann1.proof ann2.proof;
}
let mkeexpr loc expr =
@@ -541,7 +538,8 @@ let tag_table =
let field_table = Utils.create_hashtable 20 []
let get_enum_type_tags cty =
- (*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
+ (*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc
+ cty;*)
match cty with
| Tydec_bool ->
[ tag_true; tag_false ]
@@ -768,11 +766,11 @@ let get_node_var id node =
let get_eqs stmts =
List.fold_right
(fun stmt (res_eq, res_aut) ->
- match stmt with
- | Eq eq ->
- eq :: res_eq, res_aut
- | Aut aut ->
- res_eq, aut :: res_aut)
+ match stmt with
+ | Eq eq ->
+ eq :: res_eq, res_aut
+ | Aut aut ->
+ res_eq, aut :: res_aut)
stmts
([], [])
@@ -787,8 +785,7 @@ let get_node_eqs =
Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
res
-let get_contract_eqs c =
- get_eqs c.stmts
+let get_contract_eqs c = get_eqs c.stmts
let get_node_eq id node =
let eqs, _ = get_node_eqs node in
@@ -1277,7 +1274,8 @@ let mk_internal_node id =
let ck = Env.lookup_value Basic_library.clock_env id in
let tin, tout = Types.split_arrow ty in
(*eprintf "internal fun %s: %d -> %d@." id (List.length
- (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
+ (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type
+ tout));*)
let cpt = ref (-1) in
mktop
(ImportedNode
diff --git a/src/corelang.mli b/src/corelang.mli
index 3500c8e1eb762793fa12ed3d13f5ce2b7863720d..728a28501bc45cbeed0bf7fbe3bf0a55f6bba286 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -273,7 +273,8 @@ val empty_contract : contract_desc
val mk_contract_var :
ident -> bool -> type_dec option -> expr -> Location.t -> contract_desc
-val mk_contract_guarantees : string option -> eexpr -> proof_annotation option -> contract_desc
+val mk_contract_guarantees :
+ string option -> eexpr -> proof_annotation option -> contract_desc
val mk_contract_assume : string option -> eexpr -> contract_desc
diff --git a/src/inliner.ml b/src/inliner.ml
index 42dd4de524ebd12335c62c37a08940f251eb2e6e..8a15a094c2585c46d5ec0afa7b2668d61b4c712c 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -47,7 +47,8 @@ let rec add_expr_reset_cond cond expr =
| Expr_ite (c, t, e) ->
Expr_ite (aux c, aux t, aux e)
| Expr_arrow (e1, e2) ->
- (* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else e2) *)
+ (* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else
+ e2) *)
let e1 = aux e1 and e2 = aux e2 in
(* inlining is performed before typing. we can leave the fields free *)
let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in
@@ -355,7 +356,7 @@ and inline_node ?(selection_on_annotation = false) node nodes =
inline_expr eq.eq_rhs locals node nodes
in
( locals',
- Eq { eq with eq_rhs = eq_rhs' } :: new_stmts' @ stmts,
+ (Eq { eq with eq_rhs = eq_rhs' } :: new_stmts') @ stmts,
asserts' @ asserts,
annots' @ annots ))
(node.node_locals, [], node.node_asserts, node.node_annot)
diff --git a/src/lusic.ml b/src/lusic.ml
index 8772f93f573b8b44cc59b0066fedddfb4b788c66..a9d8a50e1ace729d209ec8be755b0544827ee63b 100644
--- a/src/lusic.ml
+++ b/src/lusic.ml
@@ -17,7 +17,8 @@ open Lustre_types
type t = { obsolete : bool; from_lusi : bool; contents : program_t }
-(* extracts a header from a program representing module owner = dirname/basename *)
+(* extracts a header from a program representing module owner =
+ dirname/basename *)
let extract_header dirname basename prog =
let owner = dirname ^ "/" ^ basename in
List.fold_right
diff --git a/src/lusic.mli b/src/lusic.mli
index edfe04a44b173fe8b900714b038e93f118cb5c66..bbf1a31acf850216bee870566aed72e9c76d44f4 100644
--- a/src/lusic.mli
+++ b/src/lusic.mli
@@ -2,7 +2,8 @@ open Lustre_types
type t = { obsolete : bool; from_lusi : bool; contents : program_t }
-(* extracts a header from a program representing module owner = dirname/basename *)
+(* extracts a header from a program representing module owner =
+ dirname/basename *)
val extract_header : string -> string -> program_t -> top_decl list
(* read and decode a header from a file *)
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index a9aad1407c9c28424f994c23f615fb76e00a454d..cc5d978b96e1c2819e08881df6bef56090bdcfb4 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -59,7 +59,7 @@ type var_decl = {
mutable var_type : Types.t;
mutable var_clock : Clocks.t;
var_loc : Location.t;
- var_is_contract: bool;
+ var_is_contract : bool;
}
(* The tag of an expression is a unique identifier used to distinguish different
instances of the same node *)
@@ -162,7 +162,7 @@ type contract_desc = {
modes : contract_mode list;
imports : contract_import list;
spec_loc : Location.t;
- proof : proof_annotation option
+ proof : proof_annotation option;
}
type 'a node_spec_t = Contract of 'a | NodeSpec of ident
diff --git a/src/lustre_types.mli b/src/lustre_types.mli
index 7cfdbfa3043649465b53cc8b62e540d9fb1a421f..160e25729e9bbd24e8c6af0a3011bfa0feaf0b37 100644
--- a/src/lustre_types.mli
+++ b/src/lustre_types.mli
@@ -48,7 +48,7 @@ type var_decl = {
mutable var_type : Types.t;
mutable var_clock : Clocks.t;
var_loc : Location.t;
- var_is_contract: bool;
+ var_is_contract : bool;
}
(* The tag of an expression is a unique identifier used to distinguish different
instances of the same node *)
@@ -151,7 +151,7 @@ type contract_desc = {
modes : contract_mode list;
imports : contract_import list;
spec_loc : Location.t;
- proof : proof_annotation option
+ proof : proof_annotation option;
}
type 'a node_spec_t = Contract of 'a | NodeSpec of ident
@@ -234,4 +234,4 @@ val tag_true : label
val tag_false : label
-val node_as_contract: node_desc -> contract_desc
+val node_as_contract : node_desc -> contract_desc
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 7e9f43babded77c972182a6d8393bffb7173a37c..a67084e1ef762f4828cafb5392e2d94c9a89132d 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -43,8 +43,8 @@ let build_env inputs locals outputs =
is_local = (fun id -> List.exists (fun v -> v.var_id = id) locals);
get_var =
(fun id ->
- try List.find (fun v -> v.var_id = id) all
- with Not_found ->
+ try List.find (fun v -> v.var_id = id) all
+ with Not_found ->
(* Format.eprintf "Impossible to find variable %s in set %a@.@?" * id
* VSet.pp all; *)
raise Not_found);
@@ -355,13 +355,20 @@ let translate_eq env ctx nd inputs locals outputs i eq =
let r, reset_inst = reset_instance i r call_ck in
let stateless = Stateless.check_node node_f in
let inst = if stateless then None else Some i in
- let mp = if stateless then True else mk_memory_pack ?inst (node_name node_f) in
+ let mp =
+ if stateless then True else mk_memory_pack ?inst (node_name node_f)
+ in
let ctx =
ctl
~ck:call_ck
(MStep (var_p, i, vl))
mp
- (mk_transition ?r ?inst stateless (node_name node_f) (vl @ vdecls_to_vals var_p))
+ (mk_transition
+ ?r
+ ?inst
+ stateless
+ (node_name node_f)
+ (vl @ vdecls_to_vals var_p))
{
ctx with
j = IMap.add i call_f ctx.j;
@@ -374,19 +381,16 @@ let translate_eq env ctx nd inputs locals outputs i eq =
env_cks) Clocks.print_ck call_ck;*)
{
ctx with
- si =
- (if stateless then ctx.si
- else mkinstr (MSetReset i) :: ctx.si);
+ si = (if stateless then ctx.si else mkinstr (MSetReset i) :: ctx.si);
}
- | [ x ], _ ->
- begin try
- let var_x = env.get_var x in
- let instr, spec = translate_act (var_x, eq.eq_rhs) in
- control_on_clock eq.eq_rhs.expr_clock instr True spec ctx
- with Not_found ->
- Format.eprintf "ERROR: node %s, eq %a@." id Printers.pp_node_eq eq ;
- raise Not_found
- end
+ | [ x ], _ -> (
+ try
+ let var_x = env.get_var x in
+ let instr, spec = translate_act (var_x, eq.eq_rhs) in
+ control_on_clock eq.eq_rhs.expr_clock instr True spec ctx
+ with Not_found ->
+ Format.eprintf "ERROR: node %s, eq %a@." id Printers.pp_node_eq eq;
+ raise Not_found)
| _ ->
Format.eprintf
"internal error: Machine_code.translate_eq %a@?"
@@ -495,7 +499,9 @@ let transition_0 nd =
tname = nd;
tindex = Some 0;
tvars = nd.node_inputs;
- tformula = if fst (get_stateless_status_node nd) then True else StateVarPack ResetFlag;
+ tformula =
+ (if fst (get_stateless_status_node nd) then True
+ else StateVarPack ResetFlag);
tmem_footprint = ISet.empty;
tinst_footprint = IMap.empty;
}
@@ -522,25 +528,25 @@ let transition_toplevel nd i =
let translate_eexpr env e =
try
- List.fold_right (fun (qt, xs) f -> match qt with
- | Lustre_types.Exists -> Exists (xs, f)
- | Lustre_types.Forall -> Forall (xs, f))
- e.eexpr_quantifiers
- (Value (translate_expr env e.eexpr_qfexpr))
- with
- NormalizationError ->
- Format.eprintf
- "Normalization error: %a@."
- Printers.pp_eexpr
- e;
- raise NormalizationError
-
-
-let translate_contract env c = {
- mc_pre = And (List.map (translate_eexpr env) c.Lustre_types.assume);
- mc_post = And (List.map (translate_eexpr env) c.Lustre_types.guarantees);
- mc_proof = c.proof
-}
+ List.fold_right
+ (fun (qt, xs) f ->
+ match qt with
+ | Lustre_types.Exists ->
+ Exists (xs, f)
+ | Lustre_types.Forall ->
+ Forall (xs, f))
+ e.eexpr_quantifiers
+ (Value (translate_expr env e.eexpr_qfexpr))
+ with NormalizationError ->
+ Format.eprintf "Normalization error: %a@." Printers.pp_eexpr e;
+ raise NormalizationError
+
+let translate_contract env c =
+ {
+ mc_pre = And (List.map (translate_eexpr env) c.Lustre_types.assume);
+ mc_post = And (List.map (translate_eexpr env) c.Lustre_types.guarantees);
+ mc_proof = c.proof;
+ }
let translate_spec env = function
| Contract c ->
@@ -583,7 +589,8 @@ let translate_decl nd sch =
* ; *)
let equations = assert_instrs @ sorted_eqs in
let mems = get_memories env equations in
- (* Removing computed memories from locals. We also removed unused variables. *)
+ (* Removing computed memories from locals. We also removed unused
+ variables. *)
let locals =
List.filter
(fun v -> (not (VSet.mem v mems)) && not (List.mem v.var_id unused))
@@ -603,26 +610,24 @@ let translate_decl nd sch =
let mmap = IMap.bindings ctx.j in
let mmemory_packs =
memory_pack_0 nd
- ::
- List.mapi
- (fun i f -> { mpname = nd; mpindex = Some (i + 1); mpformula = red f })
- (List.rev ctx.mp)
+ :: List.mapi
+ (fun i f -> { mpname = nd; mpindex = Some (i + 1); mpformula = red f })
+ (List.rev ctx.mp)
@ [ memory_pack_toplevel nd (List.length ctx.mp) ]
in
let mtransitions =
transition_0 nd
- ::
- List.mapi
- (fun i (tvars, tmem_footprint, tinst_footprint, f) ->
- {
- tname = nd;
- tindex = Some (i + 1);
- tvars;
- tformula = red f;
- tmem_footprint;
- tinst_footprint;
- })
- (List.rev ctx.t)
+ :: List.mapi
+ (fun i (tvars, tmem_footprint, tinst_footprint, f) ->
+ {
+ tname = nd;
+ tindex = Some (i + 1);
+ tvars;
+ tformula = red f;
+ tmem_footprint;
+ tinst_footprint;
+ })
+ (List.rev ctx.t)
@ [ transition_toplevel nd (List.length ctx.t) ]
in
let clear_reset =
@@ -630,7 +635,13 @@ let translate_decl nd sch =
~instr_spec:
((if fst (get_stateless_status_node nd) then []
else [ mk_memory_pack ~i:0 nd.node_id ])
- @ [ mk_transition ~i:0 stateless nd.node_id (vdecls_to_vals nd.node_inputs) ])
+ @ [
+ mk_transition
+ ~i:0
+ stateless
+ nd.node_id
+ (vdecls_to_vals nd.node_inputs);
+ ])
MClearReset
in
let mnode_spec = Utils.option_map (translate_spec env) nd.node_spec in
@@ -670,7 +681,7 @@ let translate_decl nd sch =
mspec = { mnode_spec; mtransitions; mmemory_packs };
mannot = nd.node_annot;
msch = Some sch;
- mis_contract = nd.node_iscontract
+ mis_contract = nd.node_iscontract;
}
(** takes the global declarations and the scheduling associated to each node *)
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 922f3b792e07a828ff41aa6e891083a3c85376ec..52b38edfc5c35bbb696f201c139ed8576022ba17 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -160,8 +160,8 @@ module PrintSpec = struct
fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [ a; b ])
| Value v ->
pp_val m fmt v
-
in
+
pp_spec
end
@@ -314,9 +314,13 @@ let pp_transitions m fmt =
fprintf fmt "@[<v 2>transitions:@ %a@]" (pp_print_list (pp_transition m))
let pp_mspec m fmt c =
- fprintf fmt "@[<v>contract: G (H (%a) => %a);]"
- (PrintSpec.pp_spec m) c.mc_pre
- (PrintSpec.pp_spec m) c.mc_post
+ fprintf
+ fmt
+ "@[<v>contract: G (H (%a) => %a);]"
+ (PrintSpec.pp_spec m)
+ c.mc_pre
+ (PrintSpec.pp_spec m)
+ c.mc_post
let pp_machine fmt m =
fprintf
@@ -452,7 +456,7 @@ let arrow_machine =
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
mannot = [];
msch = None;
- mis_contract = false
+ mis_contract = false;
}
let empty_desc =
@@ -495,7 +499,7 @@ let empty_machine =
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
mannot = [];
msch = None;
- mis_contract = false
+ mis_contract = false;
}
let new_instance =
diff --git a/src/machine_code_types.mli b/src/machine_code_types.mli
index 266c6e427f1d63b7e53c24fb63fa0054e782f876..d040eb3da50654cf1b56b7098e8d5aa73b96ef49 100644
--- a/src/machine_code_types.mli
+++ b/src/machine_code_types.mli
@@ -58,9 +58,9 @@ type mc_transition_t = value_t transition_t
type mc_memory_pack_t = value_t memory_pack_t
type mc_contract_t = {
- mc_pre: mc_formula_t;
- mc_post: mc_formula_t;
- mc_proof: proof_annotation option
+ mc_pre : mc_formula_t;
+ mc_post : mc_formula_t;
+ mc_proof : proof_annotation option;
}
type machine_spec = {
@@ -84,6 +84,7 @@ type machine_t = {
mstep : step_t;
mspec : machine_spec;
mannot : expr_annot list;
- msch : Scheduling_type.schedule_report option; (* Equations scheduling *)
- mis_contract: bool
+ msch : Scheduling_type.schedule_report option;
+ (* Equations scheduling *)
+ mis_contract : bool;
}
diff --git a/src/modules.ml b/src/modules.ml
index 7b1f4956a901e55030205c5eb499422cb7b6711c..4d852450051e59292a30cd26675384c73090eecb 100644
--- a/src/modules.ml
+++ b/src/modules.ml
@@ -32,7 +32,8 @@ let name_dependency loc (local, dep) ext =
let add_imported_node name value =
(*Format.eprintf "add_imported_node %s %a (owner=%s)@." name
- Printers.pp_imported_node (imported_node_of_top value) value.top_decl_owner;*)
+ Printers.pp_imported_node (imported_node_of_top value)
+ value.top_decl_owner;*)
try
let value' = node_from_name name in
let owner' = value'.top_decl_owner in
diff --git a/src/mutation.ml b/src/mutation.ml
index 7f6ab582d1ee30199f1a7306fb3d44c6670099ca..651cfc1adbb4c75df9056ab665242d801d869c36 100644
--- a/src/mutation.ml
+++ b/src/mutation.ml
@@ -754,7 +754,8 @@ let next_change m =
else first_boolexpr ()
in
- (* Format.eprintf "from: %a to: %a@." print_directive m print_directive res; *)
+ (* Format.eprintf "from: %a to: %a@." print_directive m print_directive
+ res; *)
res
let fold_mutate nb prog =
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index cc42e7395b81c6a4c6eca3bdc26c1e9af87301f2..602ba37489fc69e39d5e46a8e539ec6b0db0dc0b 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -501,7 +501,8 @@ let subst_instr m subst instrs instr =
(* Last case, v', the lhs of the previous similar definition is,
itself, a memory *)
- (* TODO regarder avec X. Il me semble qu'on peut faire plus simple: *)
+ (* TODO regarder avec X. Il me semble qu'on peut faire plus
+ simple: *)
(* Filtering out the list of instructions: - we copy in the same
order the list of instr in instrs (fold_right) - if the current
instr is this instr' then apply the elimination with v' -> v on
@@ -898,7 +899,8 @@ let elim_prog_variables prog removed_table =
its normalized recomputed, as well as its scheduling, before regenerating the
machines.
- The function returns both the (possibly updated) prog as well as the machines *)
+ The function returns both the (possibly updated) prog as well as the
+ machines *)
let optimize params prog node_schs machine_code =
let machine_code =
if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then (
diff --git a/src/optimize_machine.mli b/src/optimize_machine.mli
index be5dbc87e95060bc680cc06f2f25db8f83ab6475..ad98f2c6247b4462105a562dd6b852df0937901a 100644
--- a/src/optimize_machine.mli
+++ b/src/optimize_machine.mli
@@ -11,7 +11,8 @@ open Machine_code_types
its normalized recomputed, as well as its scheduling, before regenerating the
machines.
- The function returns both the (possibly updated) prog as well as the machines *)
+ The function returns both the (possibly updated) prog as well as the
+ machines *)
val optimize :
Normalization.param_t ->
program_t ->
diff --git a/src/options_management.ml b/src/options_management.ml
index 79a370004ac08e3faba353e1a306dc0880881afe..4acbc8982789dd7deb22ac2e93c5d7fb4ab05079 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -260,8 +260,7 @@ let plugin_opt (name, activate, usage, options) =
exit 0
in
("-" ^ name, Arg.Unit activate, "activate plugin " ^ name)
- ::
- ("-" ^ name ^ "-help", Arg.Unit usage, "plugin " ^ name ^ " help")
+ :: ("-" ^ name ^ "-help", Arg.Unit usage, "plugin " ^ name ^ " help")
:: List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options
let verifier_opt (name, activate, options) =
diff --git a/src/plugins/plugins.ml b/src/plugins/plugins.ml
index 26d4b0644cbde8b037b7c31946a7f977748c9046..f41253f4a5b23921e3a3087759b18f67c990a24f 100644
--- a/src/plugins/plugins.ml
+++ b/src/plugins/plugins.ml
@@ -49,7 +49,8 @@ let c_backend_main_loop_body_suffix fmt () =
M.c_backend_main_loop_body_suffix fmt ())
(plugins ())
-(* Specific treatment of annotations when inlining, specific of declared plugins *)
+(* Specific treatment of annotations when inlining, specific of declared
+ plugins *)
let inline_annots rename_var_fun annot_list =
List.map
diff --git a/src/plugins/salsa/machine_salsa_opt.ml b/src/plugins/salsa/machine_salsa_opt.ml
index c898696c3b0407316bf6aa537be2edcee06ee089..1ebd7bfef8d389512b9c8f9651e406b6ef52d30d 100644
--- a/src/plugins/salsa/machine_salsa_opt.ml
+++ b/src/plugins/salsa/machine_salsa_opt.ml
@@ -290,7 +290,8 @@ let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e :
(* if !debug then Format.eprintf "Substituted def in expr@ "; *)
let abstractEnv = RangesInt.to_abstract_env ranges in
- (* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id) abstractEnv; *)
+ (* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id)
+ abstractEnv; *)
(* The expression is partially evaluated by the available ranges
valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on
garde evalPartExpr remplace les variables e qui sont dans env par la cst
@@ -548,7 +549,7 @@ let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv
then MT.MLocalAssign (v, e)
else MT.MStateAssign (v, e)
in
- ( il @ Corelang.mkinstr instr_desc :: accu_instr,
+ ( il @ (Corelang.mkinstr instr_desc :: accu_instr),
(match r with
| None ->
ranges
@@ -820,7 +821,8 @@ let rec rewrite_instrs nodename m constEnv vars_env m instrs ranges formalEnv
(* Required variables to compute vt are introduced. Then each branch is
refactored specifically *)
- (* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; *)
+ (* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr
+ hd_instr; *)
let required_vars = get_expr_real_vars vt in
let required_vars = Vars.diff required_vars printed_vars in
(* remove already produced variables *)
@@ -896,7 +898,8 @@ let rec rewrite_instrs nodename m constEnv vars_env m instrs ranges formalEnv
ranges. We merge this data by computing the join per variable *)
formalEnv,
(* Thanks to the computation of var_to_print in each branch, no new
- definition should have been computed without being already printed *)
+ definition should have been computed without being already
+ printed *)
Vars.union written_vars printed_vars,
Vars.diff vars_to_print written_vars
(* We remove vars that have been produced within branches *),
diff --git a/src/plugins/salsa/salsaDatatypes.ml b/src/plugins/salsa/salsaDatatypes.ml
index e8e3d9c9a024178c0d2b40ee9ddc3c677cc6adf7..887b570ec9cf267743440f84786dc2e94d73ded1 100644
--- a/src/plugins/salsa/salsaDatatypes.ml
+++ b/src/plugins/salsa/salsaDatatypes.ml
@@ -69,7 +69,8 @@ functor
(* Compute a join per variable *)
let merge ranges1 ranges2 =
- (* Format.eprintf "Mergeing rangesint %a with %a@." pp ranges1 pp ranges2; *)
+ (* Format.eprintf "Mergeing rangesint %a with %a@." pp ranges1 pp
+ ranges2; *)
let ranges = Hashtbl.copy ranges1 in
Hashtbl.iter
(fun k v ->
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index 67ed0fd4c322cf491620c6eb49a2b386c690ef2e..85693b132c3762cf67b1c0bf4c25a19a80b3a333 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -302,7 +302,8 @@ let rec is_valid_path path nodename prog machines =
is_valid_path path' nodename prog machines
else false
-(* let instok = List.exists (fun (inst', node) -> inst' = inst) m.minstances in *)
+(* let instok = List.exists (fun (inst', node) -> inst' = inst) m.minstances
+ in *)
(* if not instok then Format.eprintf "inst = %s@." inst; *)
(* instok && *)
(* let instnode = fst (snd (List.find (fun (inst', node) -> inst' = inst)
diff --git a/src/printers.ml b/src/printers.ml
index 5d3a818c5189b376fc27c15f28f90d61919e4fd4..60db1b1d52b1515a8b058ece48ea17dc9cde58cf 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -495,50 +495,48 @@ let pp_spec_stmt fmt stmt =
let pp_spec fmt spec =
(* const are prefixed with const in pp_var and with nothing for regular
variables. We adapt the call to produce the appropriate output. *)
- fprintf fmt "@[<v>%a%a%a%a%a%a@]"
- (pp_print_list
- (fun fmt v ->
- fprintf fmt "%a = %t;" pp_var v (fun fmt ->
- match v.var_dec_value with
- | None ->
- assert false
- | Some e ->
- pp_expr fmt e)))
+ fprintf
+ fmt
+ "@[<v>%a%a%a%a%a%a@]"
+ (pp_print_list (fun fmt v ->
+ fprintf fmt "%a = %t;" pp_var v (fun fmt ->
+ match v.var_dec_value with
+ | None ->
+ assert false
+ | Some e ->
+ pp_expr fmt e)))
spec.consts
-
- (pp_print_list ~pp_prologue:pp_print_cut pp_spec_stmt) spec.stmts
-
- (pp_print_list ~pp_prologue:pp_print_cut (fun fmt -> fprintf fmt "assume %a;" pp_eexpr))
+ (pp_print_list ~pp_prologue:pp_print_cut pp_spec_stmt)
+ spec.stmts
+ (pp_print_list ~pp_prologue:pp_print_cut (fun fmt ->
+ fprintf fmt "assume %a;" pp_eexpr))
spec.assume
-
- (pp_print_list ~pp_prologue:pp_print_cut (fun fmt -> fprintf fmt "guarantee %a;" pp_eexpr))
+ (pp_print_list ~pp_prologue:pp_print_cut (fun fmt ->
+ fprintf fmt "guarantee %a;" pp_eexpr))
spec.guarantees
-
- (pp_print_list ~pp_prologue:pp_print_cut
- (fun fmt mode ->
- fprintf
- fmt
- "mode %s (@[<v 0>%a@ %a@]);"
- mode.mode_id
- (pp_print_list (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r))
- mode.require
- (pp_print_list (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r))
- mode.ensure))
+ (pp_print_list ~pp_prologue:pp_print_cut (fun fmt mode ->
+ fprintf
+ fmt
+ "mode %s (@[<v 0>%a@ %a@]);"
+ mode.mode_id
+ (pp_print_list (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r))
+ mode.require
+ (pp_print_list (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r))
+ mode.ensure))
spec.modes
-
- (pp_print_list ~pp_prologue:pp_print_cut
- (fun fmt import ->
- fprintf
- fmt
- "import %s (%a) returns (%a);"
- import.import_nodeid
- pp_expr
- import.inputs
- pp_expr
- import.outputs))
+ (pp_print_list ~pp_prologue:pp_print_cut (fun fmt import ->
+ fprintf
+ fmt
+ "import %s (%a) returns (%a);"
+ import.import_nodeid
+ pp_expr
+ import.inputs
+ pp_expr
+ import.outputs))
spec.imports
-(* Printing top contract as comments in regular output and as contract in kind2 *)
+(* Printing top contract as comments in regular output and as contract in
+ kind2 *)
let pp_contract fmt nd =
let c = node_as_contract nd in
fprintf
@@ -740,8 +738,7 @@ let pp_short_decl fmt decl =
| Include s ->
fprintf fmt "include \"%s\"" s
| Open (local, s) ->
- if local then fprintf fmt "#open \"%s\"" s
- else fprintf fmt "#open <%s>" s
+ if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
| TypeDef tdef ->
fprintf fmt "type %s" tdef.tydef_id
diff --git a/src/scheduling.ml b/src/scheduling.ml
index bcdbd9ae25642c2bd8186d21da0459e894a27c8b..39d53a4a36e35c4009afc4947ea5d1e78786aa80 100644
--- a/src/scheduling.ml
+++ b/src/scheduling.ml
@@ -156,7 +156,8 @@ let schedule_prog prog =
let compute_prog_reuse_table report = IMap.map compute_node_reuse_table report
-(* removes inlined local variables from schedule report, which are now useless *)
+(* removes inlined local variables from schedule report, which are now
+ useless *)
let remove_node_inlined_locals locals report =
let is_inlined v = IMap.exists (fun l _ -> v = l) locals in
let schedule' =
diff --git a/src/spec_common.ml b/src/spec_common.ml
index bdae2bcf508ad66559c104dba93a46bd8dbbb95e..a5b2cdf904e481698b6e7db65497d05553e56301 100644
--- a/src/spec_common.ml
+++ b/src/spec_common.ml
@@ -79,8 +79,8 @@ let vals vs = List.map (fun v -> Val v) vs
let mk_pred_call pred = Predicate pred
-let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst stateless id vars
- =
+let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst
+ stateless id vars =
let tr =
mk_pred_call
(Transition
diff --git a/src/spec_types.ml b/src/spec_types.ml
index 7d2324a374ec7c8aa213b8d0937ca60930b245cc..94e6a6aaee7a22ccda6053d5d7b4b719f0b33d43 100644
--- a/src/spec_types.ml
+++ b/src/spec_types.ml
@@ -24,7 +24,7 @@ let type_of_l_value : type a. (a, left_v) expression_t -> Types.t = function
type 'a predicate_t =
| Transition :
- bool (* stateless *)
+ bool (* stateless *)
* ident (* node name *)
* ident option
(* instance *)
diff --git a/src/spec_types.mli b/src/spec_types.mli
index f7ab12cbc6dc67188bacf25b7944fa974dbfa0d3..6edbe9cfc3934bf9d27655956b99dafbadc719ac 100644
--- a/src/spec_types.mli
+++ b/src/spec_types.mli
@@ -17,7 +17,7 @@ val type_of_l_value : ('a, left_v) expression_t -> Types.t
type 'a predicate_t =
| Transition :
- bool (* stateless *)
+ bool (* stateless *)
* ident (* node name *)
* ident option
(* instance *)
diff --git a/src/tools/importer/vhdl_deriving_yojson.ml b/src/tools/importer/vhdl_deriving_yojson.ml
index d7b21d0b92f6b63f6e87d9950070e7f5f8b21133..fee7119bca288a2349b1f7d9776dfa45e20a302d 100644
--- a/src/tools/importer/vhdl_deriving_yojson.ml
+++ b/src/tools/importer/vhdl_deriving_yojson.ml
@@ -33,7 +33,8 @@ type vhdl_type_t =
(* let std_logic_cst = [ "U"; "X"; "0"; "1"; "Z"; "W"; "L"; "H"; "-" ] *)
(* XXX: UNUSED *)
-(* let literal_base = [ "B"; "O"; "X"; "UB"; "UO"; "UX"; "SB"; "SO"; "SX"; "D" ] *)
+(* let literal_base = [ "B"; "O"; "X"; "UB"; "UO"; "UX"; "SB"; "SO"; "SX"; "D"
+ ] *)
(* Prefix of CstLiteral *)
(* TODO: do we need more constructors ? *)
diff --git a/src/tools/importer/vhdl_json_lib.ml b/src/tools/importer/vhdl_json_lib.ml
index f4c7c74169f2f17639a5af384457adbadeae6c45..ce97ba36b399cc655aba7d9798d1435db6180d64 100644
--- a/src/tools/importer/vhdl_json_lib.ml
+++ b/src/tools/importer/vhdl_json_lib.ml
@@ -180,7 +180,7 @@ let rec to_list_content_str str json =
if pairlist_contains_str str l then
`Assoc
((str, to_list_content_str str (`List (assoc_elem_filter_snd l str)))
- :: assoc_elem_filternot (map_snd (to_list_content_str str) l) str)
+ :: assoc_elem_filternot (map_snd (to_list_content_str str) l) str)
else `Assoc (map_snd (to_list_content_str str) l)
| `List (hd :: tl) ->
`List (to_list_content_str str hd :: List.map (to_list_content_str str) tl)
diff --git a/src/tools/seal/seal_extract.ml b/src/tools/seal/seal_extract.ml
index 16311b0251811e14f3c143bd850e4f7214493d8d..9f788b816bc9285db0d2d18df484b73fdd54968a 100644
--- a/src/tools/seal/seal_extract.ml
+++ b/src/tools/seal/seal_extract.ml
@@ -70,7 +70,8 @@ let mem_zexpr ze = Hashtbl.mem ze_hash ze
let get_zexpr e =
let _, uid = List.find (fun (e', _) -> Corelang.is_eq_expr e e') !expr_hash in
- (* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref eref.expr_tag; *)
+ (* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref
+ eref.expr_tag; *)
Hashtbl.find e_hash uid
let get_expr ze =
@@ -472,7 +473,8 @@ let clean_sys sys =
consolidated list. *)
(* combine_guards ~fresh:Some(e,b) gl1 gl2 returns ok, gl with ok=true when
- (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated version of it. *)
+ (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated version of
+ it. *)
let combine_guards ?(fresh = None) gl1 gl2 =
(* Filtering out trivial cases. More semantics ones would have to be addressed
later *)
@@ -724,7 +726,8 @@ let split_mdefs elem (mdefs : elem_guarded_expr list) =
(* select the element of guards that match the argument elem *)
let sel, others_guards = List.partition (select_elem elem) guards in
match sel with
- (* we extract the element from the list and add it to the appropriate list *)
+ (* we extract the element from the list and add it to the appropriate
+ list *)
| [ (_, sel_status) ] ->
if sel_status then (others_guards, expr) :: selected, left_out
else selected, (others_guards, expr) :: left_out
@@ -818,7 +821,8 @@ let rec build_switch_sys
true (* Regular unguarded expression *)
| [] ->
true
- (* A unbalanced definition of the memory. Here we have m_{k+1} -> m_k *)
+ (* A unbalanced definition of the memory. Here we have m_{k+1} ->
+ m_k *)
| _ ->
false)
mem_defs
@@ -859,7 +863,8 @@ let rec build_switch_sys
(* Format.eprintf "Selected item %a in@.%a@.POS=%a@.NEG=%a@."
Printers.pp_expr elem pp_all_defs mem_defs pp_all_defs pos
pp_all_defs neg ; *)
- (* Special cases to avoid useless computations: true, false conditions *)
+ (* Special cases to avoid useless computations: true, false
+ conditions *)
match elem.expr_desc with
(*| Expr_ident "true" -> build_switch_sys pos prefix *)
| Expr_const (Const_tag tag) when tag = tag_true ->
diff --git a/src/tools/seal/seal_slice.ml b/src/tools/seal/seal_slice.ml
index 4f13c2b308f8a03bbfb19fc0d9cd2558c9034773..ae03855b683e429194db3849adb254263023b3bc 100644
--- a/src/tools/seal/seal_slice.ml
+++ b/src/tools/seal/seal_slice.ml
@@ -7,12 +7,14 @@ open Seal_utils
(* their COI (cone of influence) *)
(******************************************************************************)
-(* Basic functions to search into nodes. Could be moved to corelang eventually *)
+(* Basic functions to search into nodes. Could be moved to corelang
+ eventually *)
let is_variable nd vid = List.exists (fun v -> v.var_id = vid) nd.node_locals
let find_variable nd vid = List.find (fun v -> v.var_id = vid) nd.node_locals
-(* Returns the vars required to compute v. Memories are specifically identified. *)
+(* Returns the vars required to compute v. Memories are specifically
+ identified. *)
let coi_var deps nd v =
let vname = v.var_id in
let sliced_deps = Causality.slice_graph deps vname in
diff --git a/src/tools/stateflow/json-parser/main_parse_json_file.ml b/src/tools/stateflow/json-parser/main_parse_json_file.ml
index f1930ddfdb7bad42232d47d495398394d098fa00..f5a6f06def78599e65fd6cb7a5bfbcc44cea43f0 100644
--- a/src/tools/stateflow/json-parser/main_parse_json_file.ml
+++ b/src/tools/stateflow/json-parser/main_parse_json_file.ml
@@ -69,7 +69,8 @@ module ParseExt = struct
Parser_lustre.stmt_list
(fun (stmts, asserts, annots) (in_, out_, locals_) ->
if asserts != [] || annots != [] then assert false
- (* Stateflow equations should not use asserts nor define annotations *)
+ (* Stateflow equations should not use asserts nor define
+ annotations *)
else
Action.aquote
{
diff --git a/src/tools/stateflow/semantics/cPS_lustre_generator.ml b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
index 8c9d3709a4e5f5b397f668b4f456f6359371d952..b5b9f5ec2f086fedc543494034263357c510a17d 100644
--- a/src/tools/stateflow/semantics/cPS_lustre_generator.ml
+++ b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
@@ -471,7 +471,7 @@ end) : TransformerType = struct
node_principal
let mkprincipal tr =
- event_type_decl :: mkcomponent Dcall [ "principal" ] tr
+ (event_type_decl :: mkcomponent Dcall [ "principal" ] tr)
@ [ mk_main_loop () ]
end
diff --git a/src/tools/zustre/zustre_analyze.ml b/src/tools/zustre/zustre_analyze.ml
index ebe612126a6a7a3988f2f4af54615f496c067a6f..1abe3a217ac22fb3abb087bcc933728a0aa4a604 100644
--- a/src/tools/zustre/zustre_analyze.ml
+++ b/src/tools/zustre/zustre_analyze.ml
@@ -116,16 +116,13 @@ let check machines node =
Z3.Expr.mk_app
!ctx
(get_fdecl (machine_reset_name node))
- (idx_0
- ::
- uid_0 :: List.map horn_var_to_expr (reset_vars machines machine));
+ (idx_0 :: uid_0
+ :: List.map horn_var_to_expr (reset_vars machines machine));
Z3.Expr.mk_app
!ctx
(get_fdecl (machine_step_name node))
- (idx_0
- ::
- uid_0
- :: List.map horn_var_to_expr (step_vars_m_x machines machine));
+ (idx_0 :: uid_0
+ :: List.map horn_var_to_expr (step_vars_m_x machines machine));
]
in
@@ -165,7 +162,7 @@ let check machines node =
(Z3.Arithmetic.mk_add
!ctx
[ k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1 ]
- :: List.map horn_var_to_expr main_memory_next)
+ :: List.map horn_var_to_expr main_memory_next)
in
let horn_body =
Z3.Boolean.mk_and
@@ -178,8 +175,8 @@ let check machines node =
Z3.Expr.mk_app
!ctx
(get_fdecl (step_name node))
- (k_var
- :: uid_0 :: List.map horn_var_to_expr (step_vars machines machine));
+ (k_var :: uid_0
+ :: List.map horn_var_to_expr (step_vars machines machine));
]
in
(* Vars contains all vars: in_out, current, mid, neXt memories *)
diff --git a/src/tools/zustre/zustre_common.ml b/src/tools/zustre/zustre_common.ml
index 61dd0dfcbd064f34794efe04606a7d1c3cd00f68..6e937fcbdce9eb519e21c1cfea0843472d379ca6 100644
--- a/src/tools/zustre/zustre_common.ml
+++ b/src/tools/zustre/zustre_common.ml
@@ -603,7 +603,8 @@ let rec instr_to_exprs machines reset_instances (m : machine_t) instr :
other did. Am I clear ? *)
(* For each branch we obtain the logical encoding, and the information
whether a sub node has been reset or not. If a node has been reset in one
- of the branch, then all others have to have the mem_m = mem_c statement. *)
+ of the branch, then all others have to have the mem_m = mem_c
+ statement. *)
let self = m.mname.node_id in
let branch_to_expr (tag, instrs) =
let branch_def, branch_resets =
@@ -773,14 +774,11 @@ let machine_reset machines m =
(get_fdecl (name ^ "_reset"))
(List.map
horn_var_to_expr
- (idx
- ::
- uid
- ::
- (* Additional vars: counters, uid *)
- rename_machine_list
- (concat m.mname.node_id id)
- (reset_vars machines machine_n))))
+ (idx :: uid
+ :: (* Additional vars: counters, uid *)
+ rename_machine_list
+ (concat m.mname.node_id id)
+ (reset_vars machines machine_n))))
m.minstances
in
@@ -827,7 +825,7 @@ let decl_machine machines m =
in
(* this line seems useless *)
let vars =
- idx :: uid :: vars
+ (idx :: uid :: vars)
@ rename_machine_list m.mname.node_id m.mstep.step_locals
in
(* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ "
@@ -903,7 +901,7 @@ let decl_machine machines m =
Z3.Boolean.mk_and
!ctx
(horn_step_body
- :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
+ :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
in
let vars =
step_vars_c_m_x machines m
diff --git a/src/types.ml b/src/types.ml
index 6cfb6b19c3c4d1913ab44df5c3f5a80b8d686f80..13a88a83b56a4d2a3b815952683c2593ca4d903c 100644
--- a/src/types.ml
+++ b/src/types.ml
@@ -589,9 +589,7 @@ module Make (BasicT : BASIC_TYPES) = struct
assert false
(** Returns the type corresponding to a type list. *)
- let type_of_type_list = function
- | [t] -> t
- | tyl -> new_ty (Ttuple tyl)
+ let type_of_type_list = function [ t ] -> t | tyl -> new_ty (Ttuple tyl)
let rec type_list_of_type ty =
match (repr ty).tdesc with
diff --git a/src/typing.ml b/src/typing.ml
index ba7c0877fedb5192fc0257c580d0a955db2f1a0e..ad83862f3aaff2a9b089dd46c01ba999cec15ce4 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -1048,8 +1048,8 @@ struct
let type_prog env decls =
(* try *)
- List.fold_left type_top_decl env decls
- (* with Failure _ as exc -> raise exc *)
+ List.fold_left type_top_decl env decls
+ (* with Failure _ as exc -> raise exc *)
(* Once the Lustre program is fully typed, we must get back to the original
description of dimensions, with constant parameters, instead of unifiable
diff --git a/unused/expand.ml b/unused/expand.ml
index e2ba8822bc09560bf86055089b35785d94a7e8c1..4c38b8e6027336775b370a844d92f50ed5e83076 100644
--- a/unused/expand.ml
+++ b/unused/expand.ml
@@ -248,7 +248,7 @@ and expand_expr ck_substs var_substs expr =
new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
| Expr_pre _ | Expr_arrow _ ->
assert false
- (* Not used in the Prelude part of the code *)
+(* Not used in the Prelude part of the code *)
(* Expands an equation *)
and expand_eq ck_substs var_substs eq =