[kernel] asm contracts generation before inline-stmt-contracts, update tests

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

tests/misc/asm_initialized.i

 /* 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() {

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;
 }