[kernel] ensure inline-stmt-contracts produce a correct AST

src/kernel_services/ast_transformations/inline_stmt_contracts.ml

@@ -65,10 +65,12 @@ class inline_stmt_contract =
          | [] -> Cil.DoChildren
          | _ ->
            let nop = Cil.mkStmtOneInstr ~valid_sid:true (Skip loc) in
-           List.iter (Annotations.add_code_annot emitter nop) posts;
+           let kf = Option.get self#current_kf in
+           List.iter (Annotations.add_code_annot emitter ~kf nop) posts;
            let b = Cil.mkBlockNonScoping [s; nop] in
            let b = Cil.transient_block b in
            let res = Cil.mkStmt ~valid_sid:true (Block b) in
+           Ast.mark_as_changed ();
            File.must_recompute_cfg (Option.get self#current_func);
            ChangeTo res
         )

tests/syntax/oracle/inline_stmt_contract.res.oracle

+[kernel] Parsing inline_stmt_contract.i (no preprocessing)
+/* Generated by Frama-C */
+int X;
+int f(void)
+{
+  /*@ assert inline_stmt_contract: X ≡ 0; */
+  /*@ requires X ≡ 0;
+      ensures X ≡ 1; */
+  X ++;
+  /*@ assert inline_stmt_contract: X ≡ 1; */ ;
+  return X;
+}
+
+int g(void)
+{
+  __fc_inline_contract_label_0:
+  /*@ assert inline_stmt_contract: X ≥ 0 ⇒ X > -1; */
+  /*@ behavior b:
+        assumes X ≥ 0;
+        requires X > -1;
+        ensures X ≡ 0; */
+  if (X >= 0) X = 0; else X = -1;
+  /*@
+  assert
+  inline_stmt_contract: \at(X ≥ 0,__fc_inline_contract_label_0) ⇒ X ≡ 0;
+   */
+  ;
+  return X;
+}
+
+int h(void)
+{
+  int __retres;
+  /*@ ensures \false; */
+  {
+    __retres = 1;
+    goto return_label;
+  }
+  /*@ assert inline_stmt_contract: \false; */ ;
+  return_label: return __retres;
+}
+
+int i(void)
+{
+  __fc_inline_contract_label_0:
+  /*@ behavior b0:
+        assumes X ≡ 0;
+        ensures X ≡ 1; */
+  X ++;
+  /*@
+  assert
+  inline_stmt_contract: \at(X ≡ 0,__fc_inline_contract_label_0) ⇒ X ≡ 1;
+   */
+  ;
+  __fc_inline_contract_label_1:
+  /*@ behavior b1:
+        assumes X ≡ 1;
+        ensures X ≡ 2; */
+  X ++;
+  /*@
+  assert
+  inline_stmt_contract: \at(X ≡ 1,__fc_inline_contract_label_1) ⇒ X ≡ 2;
+   */
+  ;
+  return X;
+}
+
+