From c8556efd60a24ad7bf399efa934d8c047e2b9505 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 20 Jan 2021 15:58:09 +0100
Subject: [PATCH] [Eva] use GCC machdep to increase amount of tested features

---
 tests/value/empty_struct.c                   |  4 +--
 tests/value/oracle/empty_struct.3.res.oracle | 29 +++++++++++++----
 tests/value/oracle/empty_struct.4.res.oracle | 34 ++++++++++++++++----
 3 files changed, 51 insertions(+), 16 deletions(-)

diff --git a/tests/value/empty_struct.c b/tests/value/empty_struct.c
index 607c4df5ec6..7ee04c5c827 100644
--- a/tests/value/empty_struct.c
+++ b/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"
 */
diff --git a/tests/value/oracle/empty_struct.3.res.oracle b/tests/value/oracle/empty_struct.3.res.oracle
index 17af74f6d8a..28cf14046c6 100644
--- a/tests/value/oracle/empty_struct.3.res.oracle
+++ b/tests/value/oracle/empty_struct.3.res.oracle
@@ -1,8 +1,23 @@
 [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
diff --git a/tests/value/oracle/empty_struct.4.res.oracle b/tests/value/oracle/empty_struct.4.res.oracle
index 17af74f6d8a..62bc2e7b1de 100644
--- a/tests/value/oracle/empty_struct.4.res.oracle
+++ b/tests/value/oracle/empty_struct.4.res.oracle
@@ -1,8 +1,28 @@
 [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
-- 
GitLab