diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 0dd2bfab9ba112eddb4295db90cf71fe7d0eeaf9..bcead9c22d25b7e3222a820e48c21915eb3a19e2 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -87,7 +87,6 @@ let pp_nothing fmt () = pp_print_string fmt "\\nothing"
let pp_null fmt () = pp_print_string fmt "\\null"
let pp_stdout fmt () = pp_print_string fmt "stdout"
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 instances machines m =
@@ -198,7 +197,6 @@ 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_initialization' = pp_initialization pp_print_string
let pp_local m =
@@ -324,6 +322,11 @@ let pp_transition_aux' ?i m =
pp_transition_aux ?i stateless pp_print_string pp_print_string (fun fmt v ->
(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
+let pp_reset_set pp_mem fmt (name, mem) =
+ fprintf fmt "%s_reset_set(%a)" name pp_mem mem
+
+let pp_reset_set' = pp_reset_set pp_print_string
+
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
fprintf
fmt
@@ -656,12 +659,6 @@ let pp_predicate pp_l pp_r fmt (l, r) =
let pp_lemma pp_l pp_r fmt (l, r) =
fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r
-let pp_axiomatic pp_l pp_r fmt (l, r) =
- fprintf fmt "@[<v 2>axiomatic %a {@,%a@]@;}" pp_l l pp_r r
-
-let pp_axiom pp_l pp_r fmt (l, r) =
- fprintf fmt "@[<v 2>axiom %a:@,%a;@]" pp_l l pp_r r
-
let pp_mem_valid_def fmt m =
if not (fst (get_stateless_status m) || m.mis_contract) then
let name = m.mname.node_id in
@@ -853,6 +850,17 @@ let pp_initialization_def fmt m =
fmt
((name, (name, mem_in)), m.minstances)
+let pp_reset_set_def fmt m =
+ if not (fst (get_stateless_status m)) then
+ let name = m.mname.node_id in
+ let mem = mk_mem m in
+ pp_acsl
+ (pp_predicate
+ (pp_reset_set (pp_machine_decl' ~ghost:true))
+ (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int))
+ fmt
+ ((name, (name, mem)), (mem, 1))
+
let pp_reset_cleared_def fmt m =
if not (fst (get_stateless_status m)) then
let name = m.mname.node_id in
@@ -970,7 +978,7 @@ module SrcMod = struct
in
fprintf
fmt
- "%a%a%a%a%a%a"
+ "%a%a%a%a%a%a%a"
(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
machines
(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
@@ -979,6 +987,8 @@ module SrcMod = struct
machines
(pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
machines
+ (pp_preds "/* ACSL reset set annotations */" pp_reset_set_def)
+ machines
(pp_preds "/* ACSL transition annotations */" pp_transition_defs)
machines
(pp_preds
@@ -1036,17 +1046,19 @@ module SrcMod = struct
"%a@,%a@,%a"
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
(name, mem, self)
- (pp_ensures (pp_equal pp_reset_flag' pp_print_int))
- (mem, 1)
+ (pp_ensures (pp_reset_set pp_ptr))
+ (name, mem)
(pp_assigns pp_reset_flag')
[ self; mem ])
fmt
()
- let spec_from_contract c = Spec_common.red (Imply (c.mc_pre, c.mc_post))
+ (** UNUSED *)
+ (* 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)
+ (** UNUSED *)
+ (* 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
@@ -1064,106 +1076,89 @@ module SrcMod = struct
| None ->
None, None
- let pp_init_def fmt m =
- let name = m.mname.node_id in
- let mem = mk_mem m in
- pp_predicate
- (pp_init (pp_machine_decl' ~ghost:true))
- (pp_and pp_initialization' (pp_reset_flag' ~indirect:false))
- fmt
- ((name, (name, mem)), ((name, mem), mem))
-
let rename n x = sprintf "%s_%d" x n
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);
- }
-
- let rename_expression 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
-
- 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
-
- let rename_contract n c =
- {
- c with
- mc_pre = rename_formula n c.mc_pre;
- mc_post = rename_formula n c.mc_post;
- }
-
- 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) =
+ (** UNUSED *)
+ (* 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); *)
+ (* } *)
+
+ (* let rename_expression 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 *)
+
+ (* 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 *)
+
+ (* let rename_contract n c = *)
+ (* { *)
+ (* c with *)
+ (* mc_pre = rename_formula n c.mc_pre; *)
+ (* mc_post = rename_formula n c.mc_post; *)
+ (* } *)
+
+ let pp_k_induction_case base m m_c pp_mem_out pp_vars fmt
+ (n, 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@])"
+ "%s_%s_%d(@[<hov>%a,@;%a@])"
name
- case
+ (if base then "base" else "inductive")
n
- pp_mem_in
- mem_in
- pp_vars
- (inputs @ outputs)
pp_mem_out
mem_out
+ pp_vars
+ (List.map (rename_var_decl n) m_c.mstep.step_outputs)
- 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_base_cases m fmt (c, m_c, k) =
+ let pp_k_induction_case_def base m (_, m_c, _) fmt n =
let name = m.mname.node_id in
let name_c = m_c.mname.node_id in
let mem = mk_mem m in
@@ -1172,317 +1167,152 @@ module SrcMod = struct
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
- (fun fmt n ->
- 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)
+ let l = List.init (n + 1) Fun.id in
+ let l_pp = List.concat_map (function
+ | 0 ->
+ let pp = pp_reset_set' in
+ [
+ fun fmt ->
+ (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
- 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
- let mem = mk_mem m in
- let mem_c = mk_mem_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 l' = 0 :: l in
- let pp fmt =
- let pp =
- pp_implies
- (pp_and_l (fun fmt n ->
- 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
- 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_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 ) )))
- (pp_contract m)
- in
- if stateless_c then pp fmt
- else fun x ->
- pp_forall
+ 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
+ [
+ (fun fmt ->
+ pp stateless pp_var_decl fmt
+ ( name,
+ List.map (rename_var_decl n') (inputs @ outputs),
+ rename (n' - 1) mem,
+ rename n' mem ));
+ (fun fmt ->
+ pp stateless_c pp_var_c fmt
+ ( name_c,
+ c_inputs @ c_outputs,
+ rename (n' - 1) mem_c,
+ rename n' mem_c ))
+ ]) l
+ in
+ let l_pp = if base then l_pp else List.tl l_pp in
+ let pp fmt () =
+ let pp fmt () = pp_and_l (fun fmt f -> f fmt) fmt l_pp in
+ if stateless_c then pp fmt ()
+ else
+ pp_exists
(pp_machine_decl
~ghost:true
- (pp_comma_list (fun fmt n -> pp_print_string fmt (rename n mem_c))))
+ (pp_comma_list (fun fmt n ->
+ pp_print_string fmt (rename n mem_c))))
pp
fmt
- ((m_c.mname.node_id, l'), x)
+ ((name_c, l), ())
in
pp_predicate
- (pp_k_induction_inductive_case
+ (pp_k_induction_case
+ base
m
+ m_c
(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)
- (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_locals m_c))
+ (pp_exists
+ (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, l)
+ (pp_locals m)
+ (List.concat_map (fun n ->
+ List.map (rename_var_decl n) (inputs @ outputs))
+ l))
+ pp)
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)) ) )
+ ( (n, (name, rename n mem)),
+ ( List.tl l, () ) )
- let pp_k_induction_lemmas m fmt k =
- let name = m.mname.node_id in
- let mem_in = mk_mem_in m in
- let mem_out = mk_mem_out m in
- let inputs = m.mstep.step_inputs in
- let outputs = m.mstep.step_outputs in
- let l = List.init k (fun n -> n + 1) in
+ let pp_base_case_defs m fmt (_, _, k as c_m_k) =
+ let l = List.init (k - 1) succ in
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_k_induction_case_def true m c_m_k)
fmt
l
- let pp_k_induction_axiom m fmt (c, m_c, k) =
+ let pp_inductive_case_def m fmt (_, _, k as c_m_k) =
+ pp_k_induction_case_def false m c_m_k fmt k
+
+ let pp_k_induction_lemmas m fmt (_, m_c, k) =
let name = m.mname.node_id in
- let mem_in = mk_mem_in m in
- let mem_out = mk_mem_out m in
- let mem_in_c = mk_mem_in_c m_c in
- 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 mem = mk_mem m in
let l = List.init k (fun n -> n + 1) in
- let pp =
- pp_implies
- (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_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_sep:pp_print_cutcut
+ (fun fmt n ->
+ let outputs = List.map (rename_var_decl n) m_c.mstep.step_outputs in
+ 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)
+ (name, mem)
+ (pp_locals m_c)
+ outputs)
+ (pp_implies
+ (pp_k_induction_case
+ (n <> k)
+ m
+ m_c
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
- (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))))
+ (pp_comma_list pp_var_decl))
+ (pp_and_l
+ (fun fmt x ->
+ pp_equal pp_var_decl pp_print_int fmt (x, 1)))))
+ fmt
+ (n, ((), ((n, mem), outputs))))
fmt
- ( (),
- ( (),
- ( (),
- ( 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 ) ) ) ) ) )
+ l
- let pp_k_induction m fmt ((_, m_c, k) as c_m_k) =
- let stateless_c = fst (get_stateless_status m_c) in
+ let pp_k_induction m fmt c_m_k =
pp_acsl_cut
(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)
+ "%a@,@,%a@,@,%a"
+ (pp_base_case_defs m)
c_m_k
- (pp_inductive_case m)
+ (pp_inductive_case_def m)
c_m_k
(pp_k_induction_lemmas m)
- k
- (pp_k_induction_axiom m)
c_m_k)
fmt
()
@@ -1525,14 +1355,14 @@ module SrcMod = struct
let pp_spec =
pp_print_option
(if m.mis_contract then pp_print_nothing
- else fun fmt c ->
+ 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_forall
+ (pp_exists
(fun fmt vs ->
fprintf
fmt
@@ -1547,23 +1377,20 @@ module SrcMod = struct
(m_c.mname.node_id, [ mem_in; mem_out ])
(pp_locals m)
vs)
- (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)))
+ (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)))
fmt
( m_c.mstep.step_outputs,
- ( ( m_c.mname.node_id,
+ ( m_c.mname.node_id,
m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
mem_in,
- mem_out ),
- c ) ))
+ mem_out )))
fmt
m_c)
in
@@ -1700,33 +1527,6 @@ module SrcMod = struct
| None ->
[ mem, pp_print_string ])
- let pp_contract fmt machines _self mem m =
- 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_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
- | _, _ ->
- ()
-
let pp_c_decl_local_spec_var m fmt v =
pp_acsl_line'
(fun fmt v -> fprintf fmt "%a;" (pp_ghost (pp_c_decl_local_var m)) v)
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 15f7da4c87de31012468d51f82c154a6771a01d6..4fa2b900c2e0b1081e267d1a047cf8343c5acfc2 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -33,9 +33,6 @@ 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_c_decl_local_spec_var : machine_t -> formatter -> var_decl -> unit
val get_spec_locals : machine_t -> var_decl list
val pp_ghost_reset_memory : machine_t -> formatter -> ident -> unit
@@ -50,7 +47,6 @@ module EmptyMod = struct
let pp_step_spec _ _ _ _ _ = ()
let pp_step_instr_spec _ _ _ _ _ = ()
let pp_ghost_parameter _ _ _ = ()
- let pp_contract _ _ _ _ _ = ()
let pp_c_decl_local_spec_var _ _ _ = ()
let get_spec_locals _ = []
let pp_ghost_reset_memory _ _ _ = ()
@@ -631,7 +627,6 @@ module Main (Mod : MODIFIERS_SRC) = struct
~checks:m.mstep.step_checks
~pp_instr:(pp_machine_instr dependencies m self self)
~instrs:m.mstep.step_instrs
- ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self self m)
fmt
else
(* C90 code *)
@@ -663,7 +658,6 @@ module Main (Mod : MODIFIERS_SRC) = struct
~checks:m.mstep.step_checks
~pp_instr:(pp_machine_instr dependencies m self self)
~instrs:m.mstep.step_instrs
- ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self self m)
fmt
let pp_clear_reset_code dependencies self mem fmt m =
@@ -763,7 +757,6 @@ module Main (Mod : MODIFIERS_SRC) = struct
~checks:m.mstep.step_checks
~pp_instr:(pp_machine_instr dependencies m self mem)
~instrs:m.mstep.step_instrs
- ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self mem m)
fmt
else
(* C90 code *)
@@ -798,7 +791,6 @@ module Main (Mod : MODIFIERS_SRC) = struct
~checks:m.mstep.step_checks
~pp_instr:(pp_machine_instr dependencies m self mem)
~instrs:m.mstep.step_instrs
- ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self mem m)
fmt
(********************************************************************************************)
diff --git a/src/backends/C/c_backend_src.mli b/src/backends/C/c_backend_src.mli
index 47a5665099636ed26da3f35e8e4e47b2d00bf11c..1f0f9bcfdc415b3eb512364c77fea2098df0016d 100644
--- a/src/backends/C/c_backend_src.mli
+++ b/src/backends/C/c_backend_src.mli
@@ -19,9 +19,6 @@ 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_c_decl_local_spec_var : machine_t -> formatter -> var_decl -> unit
val get_spec_locals : machine_t -> var_decl list
val pp_ghost_reset_memory : machine_t -> formatter -> ident -> unit