diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml index 91525dded13933c553725628b64f019f50c90bf1..29123aa01754a62fc6b66ad78f01d71a405a3f68 100644 --- a/src/kernel_internals/typing/asm_contracts.ml +++ b/src/kernel_internals/typing/asm_contracts.ml @@ -257,5 +257,6 @@ let () = ~deps:[(module Kernel.AsmContractsGenerate); (module Kernel.AsmContractsInitialized); (module Kernel.AsmContractsAutoValidate) ] + ~before:[Inline_stmt_contracts.category] category transform diff --git a/tests/misc/asm_initialized.i b/tests/misc/asm_initialized.i index 2932eef91d330df13b5a880c8687a4bff476c1c3..fdf22cba972438f0cb85f008e15228954f8970da 100644 --- a/tests/misc/asm_initialized.i +++ b/tests/misc/asm_initialized.i @@ -1,6 +1,6 @@ /* run.config* PLUGIN: @EVA_PLUGINS@ -STDOPT: #"-asm-contracts-ensure-init -print" +STDOPT: #"-asm-contracts-ensure-init -inline-stmt-contracts -absolute-valid-range 0x10000000-0xf00000000 -print" */ int main() { diff --git a/tests/misc/oracle/asm_initialized.res.oracle b/tests/misc/oracle/asm_initialized.res.oracle index dd13230b7df0c57d2ece51de371ff102b989112b..1cdc82f26bd80d4c7da9e140e2709eedb35c2a36 100644 --- a/tests/misc/oracle/asm_initialized.res.oracle +++ b/tests/misc/oracle/asm_initialized.res.oracle @@ -3,28 +3,30 @@ [eva] Computing initial state [eva] Initial state computed [eva:initial-state] Values of globals at initialization - -[eva:alarm] asm_initialized.i:10: Warning: - accessing uninitialized left-value. assert \initialized(&sp); + NULL[rbits 2147483648 to 515396075527] ∈ [--..--] +[eva:alarm] asm_initialized.i:9: Warning: + assertion 'inline_stmt_contract' got status unknown. [eva:alarm] asm_initialized.i:10: Warning: out of bounds write. assert \valid(sp - 2); -[kernel] asm_initialized.i:10: Warning: - all target addresses were invalid. This path is assumed to be dead. +[eva:alarm] asm_initialized.i:11: Warning: + accessing uninitialized left-value. assert \initialized(&x); [eva] Recording results for main [eva] Done for function main +[eva] asm_initialized.i:11: + assertion 'Eva,initialization' got final status invalid. [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function main: - NON TERMINATING FUNCTION + NULL[rbits 2147483648 to 515396075527] ∈ [--..--] [from] Computing for function main -[from] Non-terminating function main (no dependencies) [from] Done for function main [from] ====== DEPENDENCIES COMPUTED ====== These dependencies hold at termination for the executions that terminate: [from] Function main: - NON TERMINATING - NO EFFECTS + NULL[268435456..4294967298] FROM \nothing (and SELF) + \result FROM \nothing [from] ====== END OF DEPENDENCIES ====== [inout] Out (internal) for function main: - \nothing + NULL[268435456..4294967298] [inout] Inputs for function main: \nothing /* Generated by Frama-C */ @@ -36,9 +38,10 @@ int main(void) assigns sp; assigns sp \from \nothing; */ __asm__ volatile ("mov %%rsp, %0;" : "=r" (sp)); - /*@ assert Eva: initialization: \initialized(&sp); */ + /*@ assert inline_stmt_contract: \initialized(&sp); */ ; /*@ assert Eva: mem_access: \valid(sp - 2); */ *(sp - 2) = 3; + /*@ assert Eva: initialization: \initialized(&x); */ return x; }