Merge branch 'fix/eva/empty-struct-tests' into 'master'

[Eva] use GCC machdep to increase amount of tested features

See merge request frama-c/frama-c!3033

tests/value/empty_struct.c

@@ -2,8 +2,8 @@
    STDOPT: +" -machdep gcc_x86_32 -cpp-extra-args=-DP1 -then -lib-entry"
    STDOPT: +" -machdep gcc_x86_32 -cpp-extra-args=-DP2 -lib-entry"
    STDOPT: +" -machdep gcc_x86_32 -cpp-extra-args=-DP3 -lib-entry"
-   STDOPT: +" -cpp-extra-args=-DP1 -lib-entry"
-   STDOPT: +" -cpp-extra-args=-DP1 -absolute-valid-range 0-1 -main main2"
+   STDOPT: +" -machdep gcc_x86_32 -cpp-extra-args=-DP1 -lib-entry"
+   STDOPT: +" -machdep gcc_x86_32 -cpp-extra-args=-DP1 -absolute-valid-range 0-1 -main main2"
    STDOPT: +"  -cpp-extra-args=\"-DP1 -DP5\" -machdep gcc_x86_32 -absolute-valid-range 0-1 -main main3"
    STDOPT: +" -machdep gcc_x86_32 -cpp-extra-args=-DP1 -main main4"
 */

tests/value/oracle/empty_struct.3.res.oracle

 [kernel] Parsing tests/value/empty_struct.c (with preprocessing)
-[kernel] tests/value/empty_struct.c:13: User Error: 
-  empty structs only allowed for GCC/MSVC
-[kernel] tests/value/empty_struct.c:67: User Error: 
-  empty structs only allowed for GCC/MSVC
-[kernel] User Error: stopping on file "tests/value/empty_struct.c" that has errors. Add
-  '-kernel-msg-key pp' for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[eva] Analyzing an incomplete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  s2 ∈ [--..--]
+  pgs ∈ {{ NULL ; &S_pgs[-1] }}
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  p ∈ {{ (void *)&s }}
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function main:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+    p
+[inout] Inputs for function main:
+    \nothing

tests/value/oracle/empty_struct.4.res.oracle

 [kernel] Parsing tests/value/empty_struct.c (with preprocessing)
-[kernel] tests/value/empty_struct.c:13: User Error: 
-  empty structs only allowed for GCC/MSVC
-[kernel] tests/value/empty_struct.c:67: User Error: 
-  empty structs only allowed for GCC/MSVC
-[kernel] User Error: stopping on file "tests/value/empty_struct.c" that has errors. Add
-  '-kernel-msg-key pp' for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[eva] Analyzing a complete application starting at main2
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  NULL[rbits 0 to 15] ∈ [--..--]
+  s2 ∈ {0}
+  pgs ∈ {{ &gs }}
+[eva:alarm] tests/value/empty_struct.c:70: Warning: 
+  out of bounds read. assert \valid_read(ptr_ret);
+[eva] Recording results for main2
+[eva] done for function main2
+[eva] tests/value/empty_struct.c:70: 
+  assertion 'Eva,mem_access' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main2:
+  ptr_ret ∈ {2}
+[from] Computing for function main2
+[from] Done for function main2
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function main2:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main2:
+    ptr_ret
+[inout] Inputs for function main2:
+    \nothing