diff --git a/tests/value/absolute_pointer.c b/tests/value/absolute_pointer.c
new file mode 100644
index 0000000000000000000000000000000000000000..4aa427600610f84b79e81468758ab0ec945e69b7
--- /dev/null
+++ b/tests/value/absolute_pointer.c
@@ -0,0 +1,58 @@
+/* run.config*
+
+ STDOPT: #"-absolute-valid-range 0-0x3"
+ STDOPT: #"-main negative_absolute_address -absolute-valid-range 0-0x10000000000000000"
+ STDOPT: #"-main negative_absolute_address -warn-invalid-pointer -absolute-valid-range 0-0x10000000000000000"
+*/
+
+int * f() {
+ return 100;
+}
+
+void crash () {
+ unsigned int v = 1;
+ *((f()))=v;
+}
+
+
+char R;
+void main(int c) {
+ if(c) crash();
+
+ *((char*)0)=2;
+ R = *((char*)1);
+ *((char*)2)=2;
+ R = *((char*)3);
+}
+
+#include <stdint.h>
+
+volatile char nondet;
+
+/* Tests negative absolute addresses. Currently, Eva interprets absolute
+ addresses as unsigned integers of the size of pointers, and wrap negative
+ addresses accordingly. It would be better to not wrap such negative addresses
+ and to warn when they are dereferenced.
+ With -warn-invalid-pointers, such negative absolute addresses raise a
+ proper alarm. However, the same computation in uintptr_t type are always
+ valid. */
+void negative_absolute_address(void) {
+ uintptr_t uptr = 0;
+ char *p = 0;
+ if (nondet) {
+ *(p - 100) = 25; // invalid pointer
+ Frama_C_show_each(p - 100);
+ } else {
+ *((char *)(uptr - 100)) = 1; // valid
+ Frama_C_show_each((char *)(uptr - 100));
+ }
+ if (nondet) {
+ char *q = p - 99; // invalid pointer
+ *q = 42;
+ Frama_C_show_each(q);
+ } else {
+ char *q = (char *)(uptr - 99); // valid
+ *q = 2;
+ Frama_C_show_each(q);
+ }
+}
diff --git a/tests/value/absolute_pointer.i b/tests/value/absolute_pointer.i
deleted file mode 100644
index e0fef35ae0d0ed1b81b50540154cfc020271447e..0000000000000000000000000000000000000000
--- a/tests/value/absolute_pointer.i
+++ /dev/null
@@ -1,24 +0,0 @@
-/* run.config*
-
- STDOPT: #"-absolute-valid-range 0-0x3"
-*/
-
-int * f() {
- return 100;
-}
-
-void crash () {
- unsigned int v = 1;
- *((f()))=v;
-}
-
-
-char R;
-void main(int c) {
- if(c) crash();
-
- *((char*)0)=2;
- R = *((char*)1);
- *((char*)2)=2;
- R = *((char*)3);
-}
diff --git a/tests/value/oracle/absolute_pointer.res.oracle b/tests/value/oracle/absolute_pointer.0.res.oracle
similarity index 87%
rename from tests/value/oracle/absolute_pointer.res.oracle
rename to tests/value/oracle/absolute_pointer.0.res.oracle
index 19d88e55f2038e52629152eeb12c202a29e3ea45..6553c1d79c44c33325e89102b7060e012296ff33 100644
--- a/tests/value/oracle/absolute_pointer.res.oracle
+++ b/tests/value/oracle/absolute_pointer.0.res.oracle
@@ -1,26 +1,27 @@
-[kernel] Parsing absolute_pointer.i (no preprocessing)
+[kernel] Parsing absolute_pointer.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
NULL[rbits 0 to 31] ∈ [--..--]
R ∈ {0}
+ nondet ∈ [--..--]
[eva] computing for function crash <- main.
- Called from absolute_pointer.i:18.
+ Called from absolute_pointer.c:20.
[eva] computing for function f <- crash <- main.
- Called from absolute_pointer.i:12.
+ Called from absolute_pointer.c:14.
[eva] Recording results for f
[eva] Done for function f
-[eva:alarm] absolute_pointer.i:12: Warning:
+[eva:alarm] absolute_pointer.c:14: Warning:
out of bounds write. assert \valid(tmp);
(tmp from f())
-[kernel] absolute_pointer.i:12: Warning:
+[kernel] absolute_pointer.c:14: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for crash
[eva] Done for function crash
[eva] Recording results for main
[eva] Done for function main
-[eva] absolute_pointer.i:12:
+[eva] absolute_pointer.c:14:
assertion 'Eva,mem_access' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
diff --git a/tests/value/oracle/absolute_pointer.1.res.oracle b/tests/value/oracle/absolute_pointer.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1a7896cbbe0d439eeb0da5169506f653cec2cdf4
--- /dev/null
+++ b/tests/value/oracle/absolute_pointer.1.res.oracle
@@ -0,0 +1,38 @@
+[kernel] Parsing absolute_pointer.c (with preprocessing)
+[eva] Analyzing a complete application starting at negative_absolute_address
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ NULL[rbits 0 to 147573952589676412935] ∈ [--..--]
+ R ∈ {0}
+ nondet ∈ [--..--]
+[eva:alarm] absolute_pointer.c:43: Warning:
+ out of bounds write. assert \valid(p - 100);
+[kernel] absolute_pointer.c:43: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva] absolute_pointer.c:47: Frama_C_show_each: {4294967196}
+[eva] absolute_pointer.c:52: Frama_C_show_each: {4294967197}
+[eva] absolute_pointer.c:56: Frama_C_show_each: {4294967197}
+[eva] Recording results for negative_absolute_address
+[eva] Done for function negative_absolute_address
+[eva] absolute_pointer.c:43:
+ assertion 'Eva,mem_access' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function negative_absolute_address:
+ NULL[rbits 0 to 34359737567] ∈ [--..--]
+ [rbits 34359737568 to 34359737575] ∈ {1}
+ [rbits 34359737576 to 34359737583] ∈ {2; 42}
+ [rbits 34359737584 to 147573952589676412935] ∈ [--..--]
+ uptr ∈ {0}
+ p ∈ {0}
+[from] Computing for function negative_absolute_address
+[from] Done for function negative_absolute_address
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function negative_absolute_address:
+ NULL[4294967196..4294967197] FROM nondet
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function negative_absolute_address:
+ NULL[4294967196..4294967197]; uptr; p; q; q_0
+[inout] Inputs for function negative_absolute_address:
+ nondet
diff --git a/tests/value/oracle/absolute_pointer.2.res.oracle b/tests/value/oracle/absolute_pointer.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e05ee987da429137a909068aeff131c948328c3b
--- /dev/null
+++ b/tests/value/oracle/absolute_pointer.2.res.oracle
@@ -0,0 +1,41 @@
+[kernel] Parsing absolute_pointer.c (with preprocessing)
+[eva] Analyzing a complete application starting at negative_absolute_address
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ NULL[rbits 0 to 147573952589676412935] ∈ [--..--]
+ R ∈ {0}
+ nondet ∈ [--..--]
+[eva:alarm] absolute_pointer.c:43: Warning:
+ invalid pointer creation. assert \object_pointer(p - 100);
+[kernel] absolute_pointer.c:43: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva] absolute_pointer.c:47: Frama_C_show_each: {4294967196}
+[eva:alarm] absolute_pointer.c:50: Warning:
+ invalid pointer creation. assert \object_pointer(p - 99);
+[eva] absolute_pointer.c:56: Frama_C_show_each: {4294967197}
+[eva] Recording results for negative_absolute_address
+[eva] Done for function negative_absolute_address
+[eva] absolute_pointer.c:43:
+ assertion 'Eva,pointer_value' got final status invalid.
+[eva] absolute_pointer.c:50:
+ assertion 'Eva,pointer_value' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function negative_absolute_address:
+ NULL[rbits 0 to 34359737567] ∈ [--..--]
+ [rbits 34359737568 to 34359737575] ∈ {1}
+ [rbits 34359737576 to 34359737583] ∈ {2}
+ [rbits 34359737584 to 147573952589676412935] ∈ [--..--]
+ uptr ∈ {0}
+ p ∈ {0}
+[from] Computing for function negative_absolute_address
+[from] Done for function negative_absolute_address
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function negative_absolute_address:
+ NULL[4294967196..4294967197] FROM nondet
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function negative_absolute_address:
+ NULL[4294967196..4294967197]; uptr; p; q; q_0
+[inout] Inputs for function negative_absolute_address:
+ nondet