[Eva] Adds a test case of widen hints with function pointers.

tests/value/oracle/widen_non_constant.res.oracle

@@ -10,7 +10,7 @@
   t[0..19] ∈ {0}
   u[0..39] ∈ {0}
 [eva] computing for function main1 <- main.
-  Called from tests/value/widen_non_constant.i:84.
+  Called from tests/value/widen_non_constant.i:97.
 [eva] tests/value/widen_non_constant.i:11: Frama_C_show_each_out: {0}
 [eva] tests/value/widen_non_constant.i:13: Frama_C_show_each_in: {0}, {1}
 [eva] tests/value/widen_non_constant.i:12: starting to merge loop iterations
@@ -29,7 +29,7 @@
 [eva] Recording results for main1
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
-  Called from tests/value/widen_non_constant.i:85.
+  Called from tests/value/widen_non_constant.i:98.
 [eva] tests/value/widen_non_constant.i:27: Frama_C_show_each_out: {0}
 [eva] tests/value/widen_non_constant.i:29: Frama_C_show_each_in: {0}, {1}
 [eva] tests/value/widen_non_constant.i:28: starting to merge loop iterations
@@ -48,7 +48,7 @@
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
-  Called from tests/value/widen_non_constant.i:86.
+  Called from tests/value/widen_non_constant.i:99.
 [eva] tests/value/widen_non_constant.i:46: Frama_C_show_each_out: {0}
 [eva] tests/value/widen_non_constant.i:48: Frama_C_show_each_in: {0}, {1}
 [eva] tests/value/widen_non_constant.i:47: starting to merge loop iterations
@@ -67,7 +67,7 @@
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main4 <- main.
-  Called from tests/value/widen_non_constant.i:87.
+  Called from tests/value/widen_non_constant.i:100.
 [eva] tests/value/widen_non_constant.i:63: starting to merge loop iterations
 [eva] tests/value/widen_non_constant.i:69: starting to merge loop iterations
 [eva] tests/value/widen_non_constant.i:72: Frama_C_show_each: {43}
@@ -76,6 +76,11 @@
   Frama_C_show_each: {35; 36; 37; 38; 39; 40; 41; 42}
 [eva] Recording results for main4
 [eva] Done for function main4
+[eva] computing for function main5 <- main.
+  Called from tests/value/widen_non_constant.i:101.
+[eva] tests/value/widen_non_constant.i:90: starting to merge loop iterations
+[eva] Recording results for main5
+[eva] Done for function main5
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -97,6 +102,9 @@
   j ∈ {35; 36; 37; 38; 39; 40; 41; 42}
   maxi ∈ {19}
   maxj ∈ {35}
+[eva:final-states] Values at end of function main5:
+  i ∈ {32}
+  ptr ∈ {{ (void *)&sub }}
 [eva:final-states] Values at end of function main:
   t[0] ∈ {-1}
    [1..19] ∈ [0..18]
@@ -109,6 +117,8 @@
 [from] Done for function main3
 [from] Computing for function main4
 [from] Done for function main4
+[from] Computing for function main5
+[from] Done for function main5
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
@@ -123,6 +133,8 @@
   t[0] FROM \nothing
    [1..19] FROM \nothing (and SELF)
   u[0..39] FROM \nothing (and SELF)
+[from] Function main5:
+  NO EFFECTS
 [from] Function main:
   t[0] FROM \nothing
    [1..19] FROM \nothing (and SELF)
@@ -144,6 +156,10 @@
     t[0..19]; u[0..39]; i; j; maxi; maxj
 [inout] Inputs for function main4:
     \nothing
+[inout] Out (internal) for function main5:
+    i; ptr
+[inout] Inputs for function main5:
+    \nothing
 [inout] Out (internal) for function main:
     t[0..19]; u[0..39]
 [inout] Inputs for function main:

tests/value/widen_non_constant.i

@@ -80,9 +80,23 @@ void main4() {
 }
 
 
+static double sub(double a, double b) {return a - b;}
+
+/* Test for a possible crash on function pointers. */
+void main5 (void) {
+  int i = 0;
+  void *ptr = sub;
+  /* Do not add [sub] to the bases to be widened. */
+  while(i < 32 && ptr == sub) {
+    i++;
+  }
+}
+
+
 void main() {
   main1();
   main2();
   main3();
   main4();
+  main5();
 }