diff --git a/src/kernel_services/ast_transformations/inline_stmt_contracts.ml b/src/kernel_services/ast_transformations/inline_stmt_contracts.ml index aa0b2711ac1d011e2ad56164551c846af4657b61..710fe1051385b63769a000dea1fac068a0ffa118 100644 --- a/src/kernel_services/ast_transformations/inline_stmt_contracts.ml +++ b/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 ) diff --git a/tests/misc/oracle/asm_initialized.res.oracle b/tests/misc/oracle/asm_initialized.res.oracle index 2c96f18db694be22424ec617dc98795b27e215c1..8a5b5eb3b7df56ab2017ba24da1880114d60ee6a 100644 --- a/tests/misc/oracle/asm_initialized.res.oracle +++ b/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)