From 65622cdc0f30b4b002033d72945581492dad43b2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Thu, 26 Sep 2024 18:21:54 +0200
Subject: [PATCH] [inline-contracts] AST is growing, not completely changing
---
.../inline_stmt_contracts.ml | 2 +-
tests/misc/oracle/asm_initialized.res.oracle | 17 +++++++++++++----
2 files changed, 14 insertions(+), 5 deletions(-)
diff --git a/src/kernel_services/ast_transformations/inline_stmt_contracts.ml b/src/kernel_services/ast_transformations/inline_stmt_contracts.ml
index aa0b2711ac..710fe10513 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 2c96f18db6..8a5b5eb3b7 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)
--
GitLab