[Eva] Tests the absence of overflow alarms on modulo operations on addresses.

tests/value/modulo.i

@@ -9,13 +9,13 @@ void main2 ()
   A = (4 * i) % 4;
   B = (4 * i + 1) % 4;
   i = v; //@ assert ((i>=-100) && (i<=100)) ;
-  E = (3*i + 1) % 12; 
+  E = (3*i + 1) % 12;
   i = v; //@ assert ((i>=0) && (i<=100)) ;
-    
+
   C = (4 * i + 1) % 4;
-  D = (3*i + 1) % 12; 
-  F = (24*i + 5) % 12;    
-  G = (24*i + 5) % 13;    
+  D = (3*i + 1) % 12;
+  F = (24*i + 5) % 12;
+  G = (24*i + 5) % 13;
   H = i % 1000;
   I = (2 * i+1101) % 1000;
   J = (5 * i - 201) % 1000;
@@ -131,7 +131,7 @@ void extract_bits_modulo(void)
 //volatile int v;
 
 // Test extraction of modulo with 'positive' semantics (ie. not nearest
-// to zero in absolute value, which is the one '%' would have used). 
+// to zero in absolute value, which is the one '%' would have used).
 void pos_rem(void) {
   int n = v;
   //@ assert -1 <= n <= 255;
@@ -147,6 +147,18 @@ void pos_rem(void) {
   int l = (int)*(signed char*)&n; // Best rem is ([0..72] \cup {255})%255, we approximate by [-128..127]
 }
 
+/* No overflow alarms should be emitted on mod operations, even on addresses. */
+void address_modulo(void) {
+  int* ptr = v ? &A : &B;
+  unsigned int uaddr = (unsigned int) ptr;
+  int addr = (int) uaddr;
+  int i = v % 100;
+  int r = addr % 16;
+  r = addr % i;
+  r = uaddr % 16;
+  r = uaddr % i;
+}
+
 void main() {
   if (v) { pgcd1(a, b); }
   if (v) { pgcd2(a, b); }
@@ -157,4 +169,5 @@ void main() {
   shift_modulo();
   extract_bits_modulo();
   pos_rem();
+  address_modulo();
 }

tests/value/oracle/modulo.res.oracle

@@ -26,8 +26,8 @@
   b ∈ [--..--]
   i2 ∈ [--..--]
 [eva] computing for function pgcd1 <- main.
-  Called from modulo.i:151.
-[eva:alarm] modulo.i:151: Warning: 
+  Called from modulo.i:163.
+[eva:alarm] modulo.i:163: Warning: 
   function pgcd1: precondition got status unknown.
 [eva] modulo.i:37: loop invariant got status valid.
 [eva] modulo.i:38: loop invariant got status valid.
@@ -40,8 +40,8 @@
 [eva] Recording results for pgcd1
 [eva] Done for function pgcd1
 [eva] computing for function pgcd2 <- main.
-  Called from modulo.i:152.
-[eva:alarm] modulo.i:152: Warning: 
+  Called from modulo.i:164.
+[eva:alarm] modulo.i:164: Warning: 
   function pgcd2: precondition got status unknown.
 [eva] modulo.i:50: loop invariant got status valid.
 [eva] modulo.i:53: Frama_C_show_each_2: [-10..10], [1..10], [-9..9]
@@ -49,15 +49,15 @@
 [eva] Recording results for pgcd2
 [eva] Done for function pgcd2
 [eva] computing for function pgcd3 <- main.
-  Called from modulo.i:153.
-[eva:alarm] modulo.i:153: Warning: 
+  Called from modulo.i:165.
+[eva:alarm] modulo.i:165: Warning: 
   function pgcd3: precondition got status unknown.
 [eva:alarm] modulo.i:63: Warning: division by zero. assert b_0 ≢ 0;
 [eva] modulo.i:64: Frama_C_show_each_3: [-10..10], [-10..10], [-9..9]
 [eva] Recording results for pgcd3
 [eva] Done for function pgcd3
 [eva] computing for function main2 <- main.
-  Called from modulo.i:155.
+  Called from modulo.i:167.
 [eva:alarm] modulo.i:9: Warning: signed overflow. assert -2147483648 ≤ 4 * i;
 [eva:alarm] modulo.i:9: Warning: signed overflow. assert 4 * i ≤ 2147483647;
 [eva:alarm] modulo.i:10: Warning: signed overflow. assert -2147483648 ≤ 4 * i;
@@ -69,12 +69,12 @@
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function simultaneous_congruences <- main.
-  Called from modulo.i:156.
+  Called from modulo.i:168.
 [eva:alarm] modulo.i:76: Warning: assertion got status unknown.
 [eva] Recording results for simultaneous_congruences
 [eva] Done for function simultaneous_congruences
 [eva] computing for function shift_modulo <- main.
-  Called from modulo.i:157.
+  Called from modulo.i:169.
 [eva:alarm] modulo.i:100: Warning: assertion got status unknown.
 [eva:alarm] modulo.i:103: Warning: 
   signed overflow. assert (int)((int)(i * 12) + 5) << 25 ≤ 2147483647;
@@ -83,21 +83,42 @@
 [eva] Recording results for shift_modulo
 [eva] Done for function shift_modulo
 [eva] computing for function extract_bits_modulo <- main.
-  Called from modulo.i:158.
+  Called from modulo.i:170.
 [eva:alarm] modulo.i:109: Warning: assertion got status unknown.
 [eva] Recording results for extract_bits_modulo
 [eva] Done for function extract_bits_modulo
 [eva] computing for function pos_rem <- main.
-  Called from modulo.i:159.
+  Called from modulo.i:171.
 [eva:alarm] modulo.i:137: Warning: assertion got status unknown.
 [eva:alarm] modulo.i:142: Warning: assertion got status unknown.
 [eva:alarm] modulo.i:146: Warning: assertion got status unknown.
 [eva] Recording results for pos_rem
 [eva] Done for function pos_rem
+[eva] computing for function address_modulo <- main.
+  Called from modulo.i:172.
+[eva:garbled-mix:write] modulo.i:156: 
+  Assigning imprecise value to r because of arithmetic operation on addresses.
+[eva:alarm] modulo.i:157: Warning: division by zero. assert i ≢ 0;
+[eva:garbled-mix:write] modulo.i:157: 
+  Assigning imprecise value to r because of arithmetic operation on addresses.
+[eva:garbled-mix:write] modulo.i:158: 
+  Assigning imprecise value to r because of arithmetic operation on addresses.
+[eva:alarm] modulo.i:159: Warning: 
+  division by zero. assert (unsigned int)i ≢ 0;
+[eva:garbled-mix:write] modulo.i:159: 
+  Assigning imprecise value to r because of arithmetic operation on addresses.
+[eva] Recording results for address_modulo
+[eva] Done for function address_modulo
 [eva] Recording results for main
 [eva] Done for function main
 [scope:rm_asserts] removing 2 assertion(s)
 [eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function address_modulo:
+  ptr ∈ {{ &A ; &B }}
+  uaddr ∈ {{ (unsigned int)&A ; (unsigned int)&B }}
+  addr ∈ {{ (int)&A ; (int)&B }}
+  i ∈ [-99..99]
+  r ∈ {{ garbled mix of &{A; B} (origin: Arithmetic {modulo.i:159}) }}
 [eva:final-states] Values at end of function extract_bits_modulo:
   i ∈ [0..10]
   aa1 ∈ [1291..32011],1291%3072
@@ -182,6 +203,8 @@
   O ∈ [0..11]
   P ∈ {0}
   Q ∈ [-8..8]
+[from] Computing for function address_modulo
+[from] Done for function address_modulo
 [from] Computing for function extract_bits_modulo
 [from] Done for function extract_bits_modulo
 [from] Computing for function main2
@@ -202,6 +225,8 @@
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
+[from] Function address_modulo:
+  NO EFFECTS
 [from] Function extract_bits_modulo:
   NO EFFECTS
 [from] Function main2:
@@ -253,6 +278,10 @@
   P FROM v
   Q FROM v
 [from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function address_modulo:
+    ptr; tmp; uaddr; addr; i; r
+[inout] Inputs for function address_modulo:
+    v
 [inout] Out (internal) for function extract_bits_modulo:
     i; aa1; ptr1; m1; n1; aa2; ptr2; m2; n2; aa3; ptr3; m3; n3; aa4; ptr4; 
     m4; n4