From d800b9c37c6acf69c5476e240a9f456282d8220b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Thu, 26 Jan 2023 09:28:57 +0900
Subject: [PATCH] do not generate ghost reset functions for stateless machines
---
src/backends/C/c_backend_header.ml | 15 +++++++++++----
src/backends/C/c_backend_spec.ml | 13 ++++++++-----
2 files changed, 19 insertions(+), 9 deletions(-)
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 002c58a2..92134e63 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -307,7 +307,9 @@ struct
let pp_alloc_header header_fmt basename machines dependencies =
(* Include once: start *)
- let machines' = List.filter (fun m -> not m.mis_contract) machines in
+ let machines' = List.filter (fun m ->
+ not m.mis_contract && not (fst (get_stateless_status m)) ) machines
+ in
let baseNAME = file_to_module_name basename in
let self_dep =
{
@@ -452,7 +454,7 @@ struct
~pp_prologue:(pp_print_endcut "/* Struct declarations */")
pp_machine_struct_top_decl_from_header
~pp_epilogue:pp_print_cutcut)
- nodes
+ (List.filter (fun td -> not (fst (get_stateless_status_top_decl td))) nodes)
(* Print the prototypes of all machines *)
(pp_print_list
~pp_open_box:pp_open_vbox0
@@ -464,7 +466,9 @@ struct
let pp_memory_header header_fmt basename machines dependencies =
(* Include once: start *)
- let machines' = List.filter (fun m -> not m.mis_contract) machines in
+ let machines' = List.filter (fun m ->
+ not m.mis_contract && not (fst (get_stateless_status m)) ) machines
+ in
let baseNAME = file_to_module_name basename in
fprintf
header_fmt
@@ -501,6 +505,9 @@ struct
pp
~pp_epilogue:pp_print_cutcut
in
+ let machines' = List.filter (fun m -> not (fst (get_stateless_status m)))
+ machines
+ in
fprintf
header_fmt
"@[<v>%a@,#ifndef _%s_SPEC@,#define _%s_SPEC@,@,%a@,%a#endif@]@."
@@ -515,7 +522,7 @@ struct
(pp_preds "/* Monolithic ghost `reset` functions */" (fun fmt m ->
let mem = mk_mem m in
Src.pp_ghost_reset_spec_code machines mem fmt m))
- machines
+ machines'
end
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 534426bc..d7f96b3e 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -1075,23 +1075,26 @@ module HdrMod = struct
pp
~pp_epilogue:pp_print_cutcut
in
+ let machines' = List.filter (fun m -> not (fst (get_stateless_status m)))
+ machines
+ in
fprintf
fmt
"%a%a%a%a%a%a%a"
(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
- machines
+ machines'
(pp_preds "/* ACSL ghost structures */" pp_machine_ghost_struct)
- machines
+ machines'
(pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
- machines
+ machines'
(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
- machines
+ machines'
(pp_preds "/* ACSL transition annotations */" pp_transition_defs)
machines
(pp_preds
"/* ACSL transition memory footprints lemmas */"
pp_transition_footprint_lemmas)
- machines
+ 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))
--
GitLab