[Eva] Adds test for negative absolute addresses.

tests/value/absolute_pointer.c

+/* 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);
+  }
+}

tests/value/absolute_pointer.i

-/* 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);
-}

tests/value/oracle/absolute_pointer.res.oracle → tests/value/oracle/absolute_pointer.0.res.oracle

-[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:

tests/value/oracle/absolute_pointer.1.res.oracle

+[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

tests/value/oracle/absolute_pointer.2.res.oracle

+[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