[kernel] first steps for refining asm contracts

src/kernel_internals/typing/asm_contracts.ml

@@ -168,6 +168,24 @@ class visit_assembly =
                (fun x -> (to_id_term x, From (List.map to_id_from lv_from)))
                lv_out)
         in
+        let mk_initialized x =
+          let typ = Cil.typeOfTermLval x in
+          if Logic_utils.isLogicVoidType typ then None
+          else begin
+            let t = Logic_utils.mk_logic_AddrOf ~loc x typ in
+            let pred =
+              Logic_const.(
+                new_predicate
+                  (pinitialized ~loc (here_label,t)))
+            in
+            Some (Normal, pred)
+          end
+        in
+        let initialized () =
+          if Kernel.AsmContractsInitialized.get() then begin
+            List.filter_map mk_initialized lv_out
+          end else []
+        in
         let filter ca =
           match ca.annot_content with
           (* search for a statement contract that applies to all cases. *)
@@ -178,7 +196,8 @@ class visit_assembly =
         (match contracts with
          | [] ->
            let assigns = assigns () in
-           let bhv = Cil.mk_behavior ~assigns () in
+           let post_cond = initialized () in
+           let bhv = Cil.mk_behavior ~assigns ~post_cond () in
            let spec = Cil.empty_funspec () in
            spec.spec_behavior <- [ bhv ];
            let ca =
@@ -236,6 +255,7 @@ let transform file =
 let () =
   File.add_code_transformation_after_cleanup
     ~deps:[(module Kernel.AsmContractsGenerate);
+           (module Kernel.AsmContractsInitialized);
            (module Kernel.AsmContractsAutoValidate) ]
     category
     transform

src/kernel_services/plugin_entry_points/kernel.ml

@@ -1358,6 +1358,17 @@ module AsmContractsGenerate =
                   to gcc's extended syntax"
     end)
 
+let () = Parameter_customize.set_group normalisation
+module AsmContractsInitialized =
+  False
+    (struct
+      let option_name = "-asm-contracts-ensure-init"
+      let module_name = "AsmContractsInitialized"
+      let help = "when contracts for assembly code are generated, add \
+                  postconditions stating that the output are initialized."
+    end)
+
+
 let () = Parameter_customize.set_group normalisation
 module AsmContractsAutoValidate =
   False

src/kernel_services/plugin_entry_points/kernel.mli

@@ -537,6 +537,9 @@ module AggressiveMerging: Parameter_sig.Bool
 module AsmContractsGenerate: Parameter_sig.Bool
 (** Behavior of option "-asm-contracts" *)
 
+module AsmContractsInitialized: Parameter_sig.Bool
+(** Behavior of option "-asm-contracts-ensure-init" *)
+
 module AsmContractsAutoValidate: Parameter_sig.Bool
 (** Behavior of option "-asm-contracts-auto-validate." *)