diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index 62c7014f781da16be176be435e72d8dee57c8266..3c46ad1a4d5601ce735c8723ddc6f4ecbe5c6e6b 100644
--- a/src/backends/C/c_backend.ml
+++ b/src/backends/C/c_backend.ml
@@ -37,8 +37,7 @@ let with_main_node machines node f =
| Some m ->
f m
-let gen_files
- generate_spec_header
+let gen_files generate_spec_header
( print_memory_header,
print_alloc_header,
print_spec_header,
@@ -48,59 +47,59 @@ let gen_files
let destname = !Options.dest_dir ^ "/" ^ basename in
(* Generating H spec file *)
- if generate_spec_header then
+ if generate_spec_header then (
let spec_header_file = destname ^ "_spec.h" in
with_out_file spec_header_file (fun header_fmt ->
print_spec_header header_fmt basename machines dependencies);
- (* Generating H memory file *)
- let memory_header_file = destname ^ "_memory.h" in
- with_out_file memory_header_file (fun header_fmt ->
- print_memory_header header_fmt basename machines dependencies);
-
- (* Generating H alloc file *)
- let alloc_header_file = destname ^ "_alloc.h" in
- (* Could be changed *)
- with_out_file alloc_header_file (fun header_fmt ->
- print_alloc_header header_fmt basename machines dependencies);
-
- (* Generating Lib C file *)
- let source_lib_file = c_or_cpp destname in
- with_out_file source_lib_file (fun source_lib_fmt ->
- print_lib_c source_lib_fmt basename prog machines dependencies);
-
- (* Generating Main C file *)
- let main_node = !Options.main_node in
- with_main_node machines main_node (fun m ->
- let source_main_file = c_or_cpp (destname ^ "_main") in
- with_out_file source_main_file (fun source_main_fmt ->
- print_main_c source_main_fmt m basename prog machines dependencies));
-
- (* Generating Mauve files *)
- with_main_node machines !Options.mauve (fun m ->
- let source_mauve_file = destname ^ "_mauve.hpp" in
- with_out_file source_mauve_file (fun source_mauve_fmt ->
- (* Header *)
- print_mauve_header source_mauve_fmt basename;
- (* Shell *)
- print_mauve_shell source_mauve_fmt m;
- (* Core *)
- print_mauve_core source_mauve_fmt m;
- (* FSM *)
- print_mauve_fsm source_mauve_fmt m));
-
- (* Generating Makefile *)
- (* Makefiles: - for the moment two cases 1. Classical Makefile, only when
- provided with a main node May contain additional framac eacsl targets 2.
- Cmake : 2 files - lustrec-basename.cmake describing all variables - the
- main CMakeLists.txt activating the first file - Later option 1 should be
- removed *)
- (* Case 1 *)
- if main_node <> "" then
- let makefile_file = destname ^ ".makefile" in
+ (* Generating H memory file *)
+ let memory_header_file = destname ^ "_memory.h" in
+ with_out_file memory_header_file (fun header_fmt ->
+ print_memory_header header_fmt basename machines dependencies);
+
+ (* Generating H alloc file *)
+ let alloc_header_file = destname ^ "_alloc.h" in
(* Could be changed *)
- with_out_file makefile_file (fun makefile_fmt ->
- print_makefile basename main_node dependencies makefile_fmt)
+ with_out_file alloc_header_file (fun header_fmt ->
+ print_alloc_header header_fmt basename machines dependencies);
+
+ (* Generating Lib C file *)
+ let source_lib_file = c_or_cpp destname in
+ with_out_file source_lib_file (fun source_lib_fmt ->
+ print_lib_c source_lib_fmt basename prog machines dependencies);
+
+ (* Generating Main C file *)
+ let main_node = !Options.main_node in
+ with_main_node machines main_node (fun m ->
+ let source_main_file = c_or_cpp (destname ^ "_main") in
+ with_out_file source_main_file (fun source_main_fmt ->
+ print_main_c source_main_fmt m basename prog machines dependencies));
+
+ (* Generating Mauve files *)
+ with_main_node machines !Options.mauve (fun m ->
+ let source_mauve_file = destname ^ "_mauve.hpp" in
+ with_out_file source_mauve_file (fun source_mauve_fmt ->
+ (* Header *)
+ print_mauve_header source_mauve_fmt basename;
+ (* Shell *)
+ print_mauve_shell source_mauve_fmt m;
+ (* Core *)
+ print_mauve_core source_mauve_fmt m;
+ (* FSM *)
+ print_mauve_fsm source_mauve_fmt m));
+
+ (* Generating Makefile *)
+ (* Makefiles: - for the moment two cases 1. Classical Makefile, only when
+ provided with a main node May contain additional framac eacsl targets 2.
+ Cmake : 2 files - lustrec-basename.cmake describing all variables - the
+ main CMakeLists.txt activating the first file - Later option 1 should be
+ removed *)
+ (* Case 1 *)
+ if main_node <> "" then
+ let makefile_file = destname ^ ".makefile" in
+ (* Could be changed *)
+ with_out_file makefile_file (fun makefile_fmt ->
+ print_makefile basename main_node dependencies makefile_fmt))
(* (\* Case 2 *\) *)
(* let cmake_file = "lustrec-" ^ basename ^ ".cmake" in *)
@@ -134,7 +133,12 @@ let print_c_header basename =
Header.pp_header_from_header header_fmt basename lusic.contents
let translate_to_c generate_c_header basename prog machines dependencies =
- let generate_spec_header, header_m, source_m, source_main_m, makefile_m, machines =
+ let ( generate_spec_header,
+ header_m,
+ source_m,
+ source_main_m,
+ makefile_m,
+ machines ) =
let open Options in
match !spec with
| SpecNo ->
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 7e08852b6dd2b295937ee4dca835025689354d8c..d5361f85f4dd4a7d81252b416987015ff3d41598 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -34,7 +34,6 @@ module EmptyMod = struct
module GhostProto = EmptyGhostProto
let pp_predicates _ _ = ()
-
let pp_machine_decl_prefix _ _ = ()
let pp_import_arrow fmt () =
@@ -245,12 +244,13 @@ functor
(* Include once: start *)
let machines' = List.filter (fun m -> not m.mis_contract) machines in
let baseNAME = file_to_module_name basename in
- let self_dep = {
- local = true;
- name = basename;
- content = [];
- is_stateful = true (* assuming it is stateful *);
- }
+ let self_dep =
+ {
+ local = true;
+ name = basename;
+ content = [];
+ is_stateful = true (* assuming it is stateful *);
+ }
in
fprintf
header_fmt
@@ -259,11 +259,9 @@ functor
#define _%s_ALLOC@,\
@,\
/* Import header from %s */@,\
- %a\
- @,\
+ %a@,\
/* Import memory header from %s */@,\
- %a\
- @,\
+ %a@,\
%a%a%a#endif@]@."
(* Print the svn version number and the supported C standard (C90 or
C99) *)
@@ -275,11 +273,11 @@ functor
basename
pp_import_prototype
self_dep
- (* Import the memory header *)
+ (* Import the memory header *)
basename
pp_import_memory_prototype
self_dep
- (* Print dependencies *)
+ (* Print dependencies *)
(pp_print_list
~pp_open_box:pp_open_vbox0
~pp_prologue:(pp_print_endcut "/* Import dependencies */")
@@ -406,11 +404,7 @@ functor
let baseNAME = file_to_module_name basename in
fprintf
header_fmt
- "@[<v>%a@,\
- #ifndef _%s_MEMORY@,\
- #define _%s_MEMORY@,\
- @,\
- %a%a#endif@]@."
+ "@[<v>%a@,#ifndef _%s_MEMORY@,#define _%s_MEMORY@,@,%a%a#endif@]@."
(* Print the svn version number and the supported C standard (C90 or
C99) *)
pp_print_version
@@ -438,11 +432,7 @@ functor
let baseNAME = file_to_module_name basename in
fprintf
header_fmt
- "@[<v>%a@,\
- #ifndef _%s_SPEC@,\
- #define _%s_SPEC@,\
- @,\
- %a#endif@]@."
+ "@[<v>%a@,#ifndef _%s_SPEC@,#define _%s_SPEC@,@,%a#endif@]@."
(* Print the svn version number and the supported C standard (C90 or
C99) *)
pp_print_version
@@ -451,7 +441,6 @@ functor
baseNAME
Mod.pp_predicates
machines
-
end
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 3f78e6aa166529b702c89a01d9ca69baa6d7f5dd..a8eb84f3048ddfb0c3701f1d481c39a5fd996c49 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -18,7 +18,6 @@ open C_backend_common
module Mpfr = Lustrec_mpfr
module type MODIFIERS_MAINSRC = sig
-
val pp_import_spec_prototype : formatter -> dep_t -> unit
val pp_declare_ghost_state : formatter -> ident -> unit
val pp_ghost_state_parameter : formatter -> unit -> unit
@@ -26,6 +25,7 @@ module type MODIFIERS_MAINSRC = sig
val pp_main_loop_invariants :
ident -> machine_t list -> formatter -> machine_t -> unit
+
val pp_main_loop_end :
ident -> machine_t list -> formatter -> machine_t -> unit
end
@@ -465,21 +465,20 @@ module Main (Mod : MODIFIERS_MAINSRC) = struct
()
let pp_main_c main_fmt main_machine basename _prog machines _dependencies =
- let self_dep = {
- local = true;
- name = basename;
- content = [];
- is_stateful = true (* assuming it is stateful*);
- }
+ let self_dep =
+ {
+ local = true;
+ name = basename;
+ content = [];
+ is_stateful = true (* assuming it is stateful*);
+ }
in
fprintf
main_fmt
"@[<v>%a@,\
#include <stdlib.h>@,\
#include <assert.h>@,\
- %a\
- %a\
- @,\
+ %a%a@,\
%a@,\
%a\n\
\ @]@."
diff --git a/src/backends/C/c_backend_main.mli b/src/backends/C/c_backend_main.mli
index 3dc18e6be8d79b01c8a694cf598b859009c02ba1..b2de757237c9648806c0354774138c75ce53200e 100644
--- a/src/backends/C/c_backend_main.mli
+++ b/src/backends/C/c_backend_main.mli
@@ -11,6 +11,7 @@ module type MODIFIERS_MAINSRC = sig
val pp_main_loop_invariants :
ident -> machine_t list -> formatter -> machine_t -> unit
+
val pp_main_loop_end :
ident -> machine_t list -> formatter -> machine_t -> unit
end
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 3c02b2bd0e419d539cfcb099688728999f304425..c5c62381611e1a7a9b4b52ad6621834f68f7b7ea 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -903,24 +903,23 @@ let pp_arrow_reset_ghost mem fmt inst =
let contract_of machines m =
match m.mspec.mnode_spec with
| 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))
+ 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
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 pp_k_induction_case base m m_c pp_mem_out pp_vars fmt
- (n, mem_out) =
+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
fprintf
fmt
@@ -943,52 +942,55 @@ let pp_k_induction_case_def base m (_, m_c, _) fmt n =
let stateless = fst (get_stateless_status m) in
let stateless_c = fst (get_stateless_status m_c) in
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
- 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
+ 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
+ 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 () =
@@ -998,8 +1000,7 @@ let pp_k_induction_case_def base m (_, m_c, _) fmt n =
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
((name_c, l), ())
@@ -1013,24 +1014,23 @@ let pp_k_induction_case_def base m (_, m_c, _) fmt n =
(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))
+ 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
- ( (n, (name, rename n mem)),
- ( List.tl l, () ) )
+ ((n, (name, rename n mem)), (List.tl l, ()))
-let pp_base_case_defs m fmt (_, _, k as c_m_k) =
+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
@@ -1039,7 +1039,7 @@ let pp_base_case_defs m fmt (_, _, k as c_m_k) =
fmt
l
-let pp_inductive_case_def m fmt (_, _, k as c_m_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) =
@@ -1050,45 +1050,44 @@ let pp_k_induction_lemmas m fmt (_, m_c, k) =
~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_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))))
+ 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_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
let pp_k_induction m fmt c_m_k =
pp_acsl_cut
(fun fmt () ->
- fprintf
- fmt
- "%a@,@,%a@,@,%a"
- (pp_base_case_defs m)
- c_m_k
- (pp_inductive_case_def m)
- c_m_k
- (pp_k_induction_lemmas m)
- c_m_k)
+ fprintf
+ fmt
+ "%a@,@,%a@,@,%a"
+ (pp_base_case_defs m)
+ c_m_k
+ (pp_inductive_case_def m)
+ c_m_k
+ (pp_k_induction_lemmas m)
+ c_m_k)
fmt
()
@@ -1145,11 +1144,9 @@ module HdrMod = struct
"/* ACSL transition memory footprints lemmas */"
pp_transition_footprint_lemmas)
machines
- (pp_preds
- "/* k-induction predicates and lemmas */"
- (fun fmt m ->
- let c, m_c = contract_of machines m in
- pp_print_option (pp_proof_annotation m m_c) fmt c))
+ (pp_preds "/* k-induction predicates and lemmas */" (fun fmt m ->
+ let c, m_c = contract_of machines m in
+ pp_print_option (pp_proof_annotation m m_c) fmt c))
machines
let pp_machine_decl_prefix _ _ = ()
@@ -1285,7 +1282,8 @@ module SrcMod = struct
(* 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) *)
+ (* Transition (s, f, inst, i, List.map (rename_expression n) es, r, mf,
+ mif) *)
(* | p -> *)
(* p *)
@@ -1374,15 +1372,15 @@ module SrcMod = struct
pp_print_string
pp_print_string
(fun fmt v ->
- (if is_output m v then pp_ptr_decl else pp_var_decl)
- 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.mstep.step_inputs @ m_c.mstep.step_outputs,
- mem_in,
- mem_out )))
+ m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
+ mem_in,
+ mem_out ) ))
fmt
m_c)
in
@@ -1562,9 +1560,7 @@ module SrcMod = struct
end
module MainMod = struct
-
let pp_import_spec_prototype = SrcMod.pp_import_spec_prototype
-
let main_mem_ghost = "main_mem_ghost"
let pp_declare_ghost_state fmt name =
@@ -1587,94 +1583,114 @@ module MainMod = struct
let k_induction_of machines m =
match contract_of machines m with
- | Some c, Some m_c ->
- begin match c.mc_proof with
- | Some (Kinduction k) ->
- Some (m_c, k)
- | _ -> None
- end
- | _ -> None
+ | Some c, Some m_c -> (
+ match c.mc_proof with Some (Kinduction k) -> Some (m_c, k) | _ -> None)
+ | _ ->
+ None
let pp_main_loop_invariants main_mem machines fmt m =
let name = m.mname.node_id in
let insts = instances machines m in
let m_c_k = k_induction_of machines m in
- fprintf fmt "%a%a"
- (pp_print_option
- (fun fmt _ ->
- fprintf fmt "%a@,"
- (pp_acsl_line (pp_ghost pp_print_string)) "int __k = 0;"))
+ fprintf
+ fmt
+ "%a%a"
+ (pp_print_option (fun fmt _ ->
+ fprintf
+ fmt
+ "%a@,"
+ (pp_acsl_line (pp_ghost pp_print_string))
+ "int __k = 0;"))
m_c_k
- (pp_acsl_cut
- (fun fmt () ->
- fprintf
- fmt
- "%a@,%a@,%a@,%a%a"
- (pp_loop_invariant pp_mem_valid')
- (name, main_mem)
- (pp_loop_invariant
- (pp_memory_pack_aux pp_print_string pp_print_string))
- (name, main_mem_ghost, 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)
- (pp_loop_invariant
- (pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
- ((), ((), ()))
- (pp_print_option
- (fun fmt (m_c, k) ->
- fprintf fmt "@,%a@,%a"
- (pp_loop_invariant (pp_gequal pp_print_string pp_print_int))
- ("__k", 0)
- (pp_loop_invariant
- (pp_and_l (fun fmt k' ->
- pp_paren
- (pp_implies
- ((if k' = k then pp_gequal else pp_equal) pp_print_string pp_print_int)
- (fun fmt mem ->
- if k' = 0 then pp_reset_set' fmt (name, mem)
- else pp_k_induction_case
- (k' < k)
- m
- m_c
- pp_print_string
- (pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (fun fmt _ -> pp_true_c_bool fmt ()))
- fmt (k', mem)))
- fmt
- (("__k", k'),
- main_mem_ghost))))
- (List.init (k + 1) Fun.id)))
- m_c_k))
+ (pp_acsl_cut (fun fmt () ->
+ fprintf
+ fmt
+ "%a@,%a@,%a@,%a%a"
+ (pp_loop_invariant pp_mem_valid')
+ (name, main_mem)
+ (pp_loop_invariant
+ (pp_memory_pack_aux pp_print_string pp_print_string))
+ (name, main_mem_ghost, 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)
+ (pp_loop_invariant
+ (pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
+ ((), ((), ()))
+ (pp_print_option (fun fmt (m_c, k) ->
+ fprintf
+ fmt
+ "@,%a@,%a"
+ (pp_loop_invariant (pp_gequal pp_print_string pp_print_int))
+ ("__k", 0)
+ (pp_loop_invariant
+ (pp_and_l (fun fmt k' ->
+ pp_paren
+ (pp_implies
+ ((if k' = k then pp_gequal else pp_equal)
+ pp_print_string
+ pp_print_int)
+ (fun fmt mem ->
+ if k' = 0 then pp_reset_set' fmt (name, mem)
+ else
+ pp_k_induction_case
+ (k' < k)
+ m
+ m_c
+ pp_print_string
+ (pp_comma_list
+ ~pp_open_box:(fun fmt () ->
+ pp_open_hovbox fmt 0)
+ (fun fmt _ -> pp_true_c_bool fmt ()))
+ fmt
+ (k', mem)))
+ fmt
+ (("__k", k'), main_mem_ghost))))
+ (List.init (k + 1) Fun.id)))
+ m_c_k))
()
let pp_main_loop_end _main_mem machines fmt m =
- fprintf fmt "@,%a"
- (pp_print_option
- (fun fmt (m_c, _) ->
- let stateless_c = fst (get_stateless_status m_c) in
- let name_c = m_c.mname.node_id in
- let mem_in_c = mk_mem_in_c m in
- let mem_out_c = mk_mem_out_c m in
- let pp_var_c fmt (out, vd) =
- if out then pp_true_c_bool fmt ()
- else pp_var_decl fmt vd
- in
- let c_inputs = List.map (fun v -> false, v) m_c.mstep.step_inputs in
- let c_outputs = List.map (fun v -> true, v) m_c.mstep.step_outputs in
- fprintf fmt "%a@,%a"
- (pp_acsl_line (pp_ghost pp_print_string))
- "__k++;"
- (pp_acsl_line'
- (pp_assert
- (pp_transition_aux
- stateless_c
- pp_print_string
- pp_print_string
- pp_var_c)))
- (name_c, c_inputs @ c_outputs, mem_in_c, mem_out_c)))
+ fprintf
+ fmt
+ "@,%a"
+ (pp_print_option (fun fmt (m_c, _) ->
+ let stateless_c = fst (get_stateless_status m_c) in
+ let name_c = m_c.mname.node_id in
+ let mem_in_c = mk_mem_in_c m in
+ let mem_out_c = mk_mem_out_c m in
+ let pp_var_c fmt (out, vd) =
+ if out then pp_true_c_bool fmt () else pp_var_decl fmt vd
+ in
+ let c_inputs = List.map (fun v -> false, v) m_c.mstep.step_inputs in
+ let c_outputs = List.map (fun v -> true, v) m_c.mstep.step_outputs in
+ let pp =
+ pp_transition_aux
+ stateless_c
+ pp_print_string
+ pp_print_string
+ pp_var_c
+ in
+ fprintf
+ fmt
+ "%a@,%a"
+ (pp_acsl_line (pp_ghost pp_print_string))
+ "__k++;"
+ (pp_acsl_line'
+ (pp_assert (fun fmt x ->
+ if stateless_c then pp fmt x
+ else
+ pp_exists
+ (pp_machine_decl
+ ~ghost:true
+ (pp_comma_list pp_print_string))
+ pp
+ fmt
+ ((name_c, [ mem_in_c; mem_out_c ]), x))))
+ (name_c, c_inputs @ c_outputs, mem_in_c, mem_out_c)))
(k_induction_of machines m)
let pp_main_spec fmt =
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 06da4eacd3af29ff32765d11a8fb5dcc19ebaef2..b6f4c43733cb92b9c7d1d2c978cdd3556457e473 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -22,7 +22,6 @@ module type MODIFIERS_SRC = sig
module GhostProto : MODIFIERS_GHOST_PROTO
val pp_import_spec_prototype : formatter -> dep_t -> unit
-
val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
@@ -33,7 +32,6 @@ module type MODIFIERS_SRC = sig
machine_t -> ident -> ident -> formatter -> instr_t -> unit
val pp_ghost_parameter : ident -> formatter -> ident option -> 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
@@ -1001,12 +999,13 @@ module Main (Mod : MODIFIERS_SRC) = struct
ind.nodei_id
let pp_lib_c source_fmt basename prog machines dependencies =
- let self_dep = {
- local = true;
- name = basename;
- content = [];
- is_stateful = true (* assuming it is stateful *);
- }
+ let self_dep =
+ {
+ local = true;
+ name = basename;
+ content = [];
+ is_stateful = true (* assuming it is stateful *);
+ }
in
fprintf
source_fmt
diff --git a/src/backends/C/c_backend_src.mli b/src/backends/C/c_backend_src.mli
index 12d9fb78fd072a825a312b47bbd6a862788a3c93..8a3d136de41f1baaeaf371a084475e0ff883568e 100644
--- a/src/backends/C/c_backend_src.mli
+++ b/src/backends/C/c_backend_src.mli
@@ -8,7 +8,6 @@ module type MODIFIERS_SRC = sig
module GhostProto : MODIFIERS_GHOST_PROTO
val pp_import_spec_prototype : formatter -> dep_t -> unit
-
val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
@@ -19,7 +18,6 @@ module type MODIFIERS_SRC = sig
machine_t -> ident -> ident -> formatter -> instr_t -> unit
val pp_ghost_parameter : ident -> formatter -> ident option -> 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