diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 310bc7e31079f520feff8cd0b14cffb6675de5d3..f26b7eb1e0ccb32af497b88cea5948ae0a0f0287 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -61,6 +61,9 @@ let mk_mem_out = mk_local "mem_out"
let mk_mem_in_c = mk_local "mem_in_c"
let mk_mem_out_c = mk_local "mem_out_c"
let mk_mem_reset = mk_local "mem_reset"
+let mk_main_mem_ghost = mk_local "main_mem_ghost"
+let mk_main_mem_ghost_c = mk_local "main_mem_ghost_c"
+let mk_k = mk_local "k"
(* Generation of a non-clashing name for the instance variable of static
allocation macro *)
diff --git a/src/backends/C/c_backend_common.mli b/src/backends/C/c_backend_common.mli
index a9fc7f8e261f977e982106e2be7a50f1cd2e775f..7ebacfec68623b699bf0a237a7e85ec14b926b93 100644
--- a/src/backends/C/c_backend_common.mli
+++ b/src/backends/C/c_backend_common.mli
@@ -186,6 +186,9 @@ val mk_mem_out : machine_t -> ident
val mk_mem_in_c : machine_t -> ident
val mk_mem_out_c : machine_t -> ident
val mk_mem_reset : machine_t -> ident
+val mk_main_mem_ghost : machine_t -> ident
+val mk_main_mem_ghost_c : machine_t -> ident
+val mk_k : machine_t -> ident
(* Generation of a non-clashing name for the attribute variable of static
allocation macro *)
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 88271a178619f9520f2cef78bce0f9422f4d937b..5228ef9416fbfd90a09a859cc4ab90d4f1982ba0 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -19,8 +19,13 @@ module Mpfr = Lustrec_mpfr
module type MODIFIERS_MAINSRC = sig
val pp_import_spec_prototype : formatter -> dep_t -> unit
- val pp_declare_ghost_state : machine_t option -> formatter -> ident -> unit
- val pp_ghost_state_parameter : formatter -> machine_t option -> unit
+
+ val pp_declare_ghost_state :
+ machine_t -> machine_t option -> formatter -> ident -> unit
+
+ val pp_ghost_state_parameter :
+ machine_t -> formatter -> machine_t option -> unit
+
val pp_main_spec : formatter -> unit
val pp_main_loop_invariants :
@@ -29,17 +34,17 @@ module type MODIFIERS_MAINSRC = sig
val pp_main_loop_end :
ident -> machine_t list -> formatter -> machine_t -> unit
- val pp_reset_contract : formatter -> machine_t -> unit
+ val pp_reset_contract : machine_t -> formatter -> machine_t -> unit
end
module EmptyMod = struct
let pp_import_spec_prototype _ _ = ()
- let pp_declare_ghost_state _ _ _ = ()
- let pp_ghost_state_parameter _ _ = ()
+ let pp_declare_ghost_state _ _ _ _ = ()
+ let pp_ghost_state_parameter _ _ _ = ()
let pp_main_spec _ = ()
let pp_main_loop_invariants _ _ _ _ = ()
let pp_main_loop_end _ _ _ _ = ()
- let pp_reset_contract _ _ = ()
+ let pp_reset_contract _ _ _ = ()
end
module Main (Mod : MODIFIERS_MAINSRC) = struct
@@ -122,14 +127,14 @@ module Main (Mod : MODIFIERS_MAINSRC) = struct
pp_machine_alloc_name
mname)
()
- (Mod.pp_declare_ghost_state m_c)
+ (Mod.pp_declare_ghost_state m m_c)
mname
pp_machine_set_reset_name
mname
main_mem
- Mod.pp_ghost_state_parameter
+ (Mod.pp_ghost_state_parameter m)
None
- (pp_print_option Mod.pp_reset_contract)
+ (pp_print_option (Mod.pp_reset_contract m))
m_c
let pp_global_initialize fmt basename =
@@ -302,7 +307,7 @@ module Main (Mod : MODIFIERS_MAINSRC) = struct
(pp_outputs ~pp_eol:pp_print_comma)
outputs
self
- Mod.pp_ghost_state_parameter
+ (Mod.pp_ghost_state_parameter m)
m_c
let pp_main_loop mname main_mem machines m_c fmt m =
diff --git a/src/backends/C/c_backend_main.mli b/src/backends/C/c_backend_main.mli
index 3fa1d45ab0508edd29a200e143a80c77a9f3b9f4..c8a7cbe44c0245c94c86222d12f8579e8eaeb622 100644
--- a/src/backends/C/c_backend_main.mli
+++ b/src/backends/C/c_backend_main.mli
@@ -5,8 +5,13 @@ open Machine_code_types
module type MODIFIERS_MAINSRC = sig
val pp_import_spec_prototype : formatter -> dep_t -> unit
- val pp_declare_ghost_state : machine_t option -> formatter -> ident -> unit
- val pp_ghost_state_parameter : formatter -> machine_t option -> unit
+
+ val pp_declare_ghost_state :
+ machine_t -> machine_t option -> formatter -> ident -> unit
+
+ val pp_ghost_state_parameter :
+ machine_t -> formatter -> machine_t option -> unit
+
val pp_main_spec : formatter -> unit
val pp_main_loop_invariants :
@@ -15,7 +20,7 @@ module type MODIFIERS_MAINSRC = sig
val pp_main_loop_end :
ident -> machine_t list -> formatter -> machine_t -> unit
- val pp_reset_contract : formatter -> machine_t -> unit
+ val pp_reset_contract : machine_t -> formatter -> machine_t -> unit
end
module EmptyMod : MODIFIERS_MAINSRC
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 70dc1070856f4de9ab3bae11b635b4fe16891ac3..28d7ef8c8db4881626dd79fb98a9c23cda6a8ae6 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -1605,10 +1605,10 @@ end
module MainMod = struct
let pp_import_spec_prototype = SrcMod.pp_import_spec_prototype
- let main_mem_ghost = "main_mem_ghost"
- let main_mem_ghost_c = "main_mem_ghost_c"
+ (* let main_mem_ghost = "main_mem_ghost" *)
+ (* let main_mem_ghost_c = "main_mem_ghost_c" *)
- let pp_reset_contract fmt m_c =
+ let pp_reset_contract m fmt m_c =
let stateless_c = fst (get_stateless_status m_c) in
let name_c = m_c.mname.node_id in
pp_print_only_if
@@ -1625,11 +1625,11 @@ module MainMod = struct
pp_machine_set_reset_name
name_c
pp_ref'
- main_mem_ghost_c))))
+ (mk_main_mem_ghost_c m)))))
fmt
()
- let pp_declare_ghost_state m_c fmt name =
+ let pp_declare_ghost_state m m_c fmt name =
fprintf
fmt
"%a%a@;"
@@ -1640,7 +1640,7 @@ module MainMod = struct
"%a(,%s);"
(pp_machine_static_alloc_name ~ghost:true)
name
- main_mem_ghost)))
+ (mk_main_mem_ghost m))))
()
(pp_print_option (fun fmt m_c ->
let stateless_c = fst (get_stateless_status m_c) in
@@ -1655,7 +1655,7 @@ module MainMod = struct
(pp_acsl_line'_cut
(pp_ghost (fun fmt ->
fprintf fmt "%a;" (pp_machine_decl' ~ghost:true))))))
- (name_c, main_mem_ghost_c)
+ (name_c, mk_main_mem_ghost_c m)
(pp_acsl
(pp_ghost
(pp_print_list
@@ -1666,11 +1666,11 @@ module MainMod = struct
m_c.mstep.step_outputs))
m_c
- let pp_ghost_state_parameter fmt m_c =
+ let pp_ghost_state_parameter m fmt m_c =
GhostProto.pp_ghost_parameters
~cut:false
fmt
- ((main_mem_ghost, pp_ref pp_print_string)
+ ((mk_main_mem_ghost m, pp_ref pp_print_string)
::
(match m_c with
| None ->
@@ -1683,7 +1683,7 @@ module MainMod = struct
m_c.mstep.step_outputs
in
if stateless_c then l
- else (main_mem_ghost_c, pp_ref pp_print_string) :: l))
+ else (mk_main_mem_ghost_c m, pp_ref pp_print_string) :: l))
let k_induction_of machines m =
match contract_of machines m with
@@ -1696,6 +1696,7 @@ module MainMod = struct
let name = m.mname.node_id in
let insts = instances machines m in
let m_c_k = k_induction_of machines m in
+ let var_k = mk_k m in
fprintf
fmt
"%a%a"
@@ -1703,8 +1704,8 @@ module MainMod = struct
fprintf
fmt
"%a@,"
- (pp_acsl_line (pp_ghost pp_print_string))
- "int __k = 0;"))
+ (pp_acsl_line (pp_ghost (fun fmt -> fprintf fmt "int %s = 0;")))
+ var_k))
m_c_k
(pp_acsl_cut (fun fmt () ->
fprintf
@@ -1714,13 +1715,13 @@ module MainMod = struct
(name, main_mem)
(pp_loop_invariant
(pp_memory_pack_aux pp_print_string pp_print_string))
- (name, main_mem_ghost, main_mem)
+ (name, mk_main_mem_ghost m, main_mem)
(pp_loop_invariant
(pp_separated
(pp_paren pp_print_string)
pp_ref'
(pp_ref pp_var_decl)))
- (main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
+ (main_mem, mk_main_mem_ghost m, insts, m.mstep.step_outputs)
(pp_loop_invariant
(pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
((), ((), ()))
@@ -1731,7 +1732,7 @@ module MainMod = struct
fmt
"@,%a@,%a"
(pp_loop_invariant (pp_gequal pp_print_string pp_print_int))
- ("__k", 0)
+ (var_k, 0)
(pp_loop_invariant
(pp_and_l (fun fmt k' ->
pp_paren
@@ -1749,7 +1750,7 @@ module MainMod = struct
pp_reset_set'
fmt
( (name, mem),
- (name_c, main_mem_ghost_c) )
+ (name_c, mk_main_mem_ghost_c m) )
else
pp_k_induction_case
(k' < k)
@@ -1762,9 +1763,9 @@ module MainMod = struct
pp_open_hovbox fmt 0)
(fun fmt _ -> pp_true_c_bool fmt ()))
fmt
- (k', mem, main_mem_ghost_c)))
+ (k', mem, mk_main_mem_ghost_c m)))
fmt
- (("__k", k'), main_mem_ghost))))
+ ((var_k, k'), mk_main_mem_ghost m))))
(List.init (k + 1) Fun.id)))
m_c_k))
()
@@ -1777,8 +1778,8 @@ module MainMod = struct
fprintf
fmt
"%a@,%a"
- (pp_acsl_line (pp_ghost pp_print_string))
- "__k++;"
+ (pp_acsl_line (pp_ghost (fun fmt -> fprintf fmt "%s++;")))
+ (mk_k m)
(pp_acsl_line
(pp_assert
(pp_and_l (fun fmt v ->