[inline-contracts] AST is growing, not completely changing

src/kernel_services/ast_transformations/inline_stmt_contracts.ml

@@ -125,7 +125,7 @@ class inline_stmt_contract =
            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 ();
+           Ast.mark_as_grown ();
            File.must_recompute_cfg (Option.get self#current_func);
            ChangeTo res
         )

tests/misc/oracle/asm_initialized.res.oracle

@@ -52,20 +52,29 @@ int main(void)
 --- Properties of Function 'main'
 --------------------------------------------------------------------------------
 
-[    -    ] Assertion 'inline_stmt_contract' (file asm_initialized.i, line 9)
-            tried with Eva.
+[  Valid  ] Post-condition (file asm_initialized.i, line 9) at assembly (file asm_initialized.i, line 9)
+            by asm_contracts.
+[  Valid  ] Assigns (file asm_initialized.i, line 9) at assembly (file asm_initialized.i, line 9)
+            by asm_contracts.
+[  Valid  ] Assertion 'inline_stmt_contract' (file asm_initialized.i, line 9)
+            by inline_stmt_contract.
 [    -    ] Assertion 'Eva,mem_access' (file asm_initialized.i, line 10)
             tried with Eva.
 [  Alarm  ] Assertion 'Eva,initialization' (file asm_initialized.i, line 11)
             By Eva, with pending:
              - Unreachable return (file asm_initialized.i, line 11)
+[  Valid  ] Froms (file asm_initialized.i, line 9) at assembly (file asm_initialized.i, line 9)
+            by asm_contracts.
+[  Valid  ] Default behavior at assembly (file asm_initialized.i, line 9)
+            by Frama-C kernel.
 
 --------------------------------------------------------------------------------
 --- Status Report Summary
 --------------------------------------------------------------------------------
-     2 To be validated
+     5 Completely validated
+     1 To be validated
      1 Alarm emitted
-     3 Total
+     7 Total
 --------------------------------------------------------------------------------
 /* Generated by Frama-C */
 int main(void)