do not generate ghost reset functions for stateless machines

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 ../../.." *)

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))