[Libc] add more interval function C stubs; add test

share/libc/__fc_builtin.c

@@ -22,6 +22,7 @@
 
 #include "__fc_builtin.h"
 __PUSH_FC_STDLIB
+#include "limits.h"
 
 /* Those builtins implementations could probably be removed entirely for
    Value, as the spec is informative enough. There remains a slight difference
@@ -30,6 +31,11 @@ __PUSH_FC_STDLIB
 
 int volatile Frama_C_entropy_source;
 
+// Additional entropy sources for some interval functions
+unsigned int volatile __fc_unsigned_int_entropy;
+long volatile __fc_long_entropy;
+unsigned long volatile __fc_unsigned_long_entropy;
+
 //@ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 void Frama_C_update_entropy(void) {
   Frama_C_entropy_source = Frama_C_entropy_source;
@@ -56,10 +62,10 @@ void *Frama_C_nondet_ptr(void *a, void *b)
 
 int Frama_C_interval(int min, int max)
 {
-  int r,aux;
+  int r, aux;
   Frama_C_update_entropy();
   aux = Frama_C_entropy_source;
-  if ((aux>=min) && (aux <=max))
+  if (aux >= min && aux <= max)
     r = aux;
   else
     r = min;
@@ -68,27 +74,60 @@ int Frama_C_interval(int min, int max)
 
 char Frama_C_char_interval(char min, char max)
 {
-  int r;
-  char aux;
+  return (char)Frama_C_interval(min, max);
+}
+
+float Frama_C_float_interval(float min, float max)
+{
   Frama_C_update_entropy();
-  aux = Frama_C_entropy_source;
-  if ((aux>=min) && (aux <=max))
+  return Frama_C_entropy_source ? min : max;
+}
+
+double Frama_C_double_interval(double min, double max)
+{
+  Frama_C_update_entropy();
+  return Frama_C_entropy_source ? min : max;
+}
+
+unsigned char Frama_C_unsigned_char_interval(unsigned char min, unsigned char max)
+{
+  return (unsigned char)Frama_C_interval(min, max);
+}
+
+unsigned int Frama_C_unsigned_int_interval(unsigned int min, unsigned int max)
+{
+  unsigned int r, aux;
+  Frama_C_update_entropy();
+  aux = __fc_unsigned_int_entropy;
+  if (aux >= min && aux <= max)
     r = aux;
   else
     r = min;
   return r;
 }
 
-float Frama_C_float_interval(float min, float max)
+long Frama_C_long_interval(long min, long max)
 {
+  long r, aux;
   Frama_C_update_entropy();
-  return Frama_C_entropy_source ? min : max;
+  aux = __fc_long_entropy;
+  if (aux >= min && aux <= max)
+    r = aux;
+  else
+    r = min;
+  return r;
 }
 
-double Frama_C_double_interval(double min, double max)
+unsigned long Frama_C_unsigned_long_interval(unsigned long min, unsigned long max)
 {
+  unsigned long r, aux;
   Frama_C_update_entropy();
-  return Frama_C_entropy_source ? min : max;
+  aux = __fc_unsigned_long_entropy;
+  if (aux >= min && aux <= max)
+    r = aux;
+  else
+    r = min;
+  return r;
 }
 
 extern void __builtin_abort(void) __attribute__((noreturn)); // GCC builtin

tests/libc/fc_builtin_c.c

+#include "__fc_builtin.c"
+#include <limits.h>
+
+// The "sampling:unknown" assertions check whether a given value _may_ be
+// in the interval; they are supposed to return 'unknown', but never 'invalid'.
+
+int main() {
+  int i = Frama_C_interval(10, INT_MAX - 20);
+  //@ assert bounds: 10 <= i <= INT_MAX - 20;
+  //@ assert sampling:unknown: i == INT_MAX/2;
+
+  char c = Frama_C_char_interval(CHAR_MIN + 1, CHAR_MAX - 4);
+  //@ assert bounds: CHAR_MIN + 1 <= c <= CHAR_MAX - 4;
+  //@ assert sampling:unknown: c == 42;
+
+  unsigned int ui = Frama_C_unsigned_int_interval(INT_MAX, UINT_MAX);
+  //@ assert bounds: INT_MAX <= ui <= UINT_MAX;
+  //@ assert sampling:unknown: ui == UINT_MAX - 10000;
+
+  float f = Frama_C_float_interval(1.0, 2.0);
+  //@ assert bounds: 1.0 <= f <= 2.0;
+  //@ assert sampling:unknown: f == 1.5;
+
+  double one_e_100 = 0x1.249ad2594c37dp332;
+  double d = Frama_C_double_interval(1e10, one_e_100);
+  //@ assert bounds: 1e10 <= d <= one_e_100;
+  //@ assert sampling:unknown: d == 12345678901.2;
+
+  long l = Frama_C_long_interval(LONG_MIN, -2L);
+  //@ assert bounds: LONG_MIN <= l <= -2;
+  //@ assert sampling:unknown: l == -3;
+
+  unsigned long ul =
+    Frama_C_unsigned_long_interval(LONG_MAX - 1UL, LONG_MAX + 1UL);
+  //@ assert bounds: LONG_MAX - 1 <= ul <= LONG_MAX + 1;
+  //@ assert sampling:unknown: ul == LONG_MAX;
+}

tests/libc/oracle/fc_builtin_c.res.oracle

+[kernel] Parsing tests/libc/fc_builtin_c.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
+  
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/fc_builtin_c.c:8.
+[eva] computing for function Frama_C_update_entropy <- Frama_C_interval <- main.
+  Called from share/libc/__fc_builtin.c:66.
+[eva] Recording results for Frama_C_update_entropy
+[eva] Done for function Frama_C_update_entropy
+[eva] Recording results for Frama_C_interval
+[eva] Done for function Frama_C_interval
+[eva] tests/libc/fc_builtin_c.c:9: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:10: Warning: 
+  assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_char_interval <- main.
+  Called from tests/libc/fc_builtin_c.c:12.
+[eva] computing for function Frama_C_interval <- Frama_C_char_interval <- main.
+  Called from share/libc/__fc_builtin.c:77.
+[eva] share/libc/__fc_builtin.c:66: 
+  Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_interval
+[eva] Done for function Frama_C_interval
+[eva] Recording results for Frama_C_char_interval
+[eva] Done for function Frama_C_char_interval
+[eva] tests/libc/fc_builtin_c.c:13: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:14: Warning: 
+  assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_unsigned_int_interval <- main.
+  Called from tests/libc/fc_builtin_c.c:16.
+[eva] share/libc/__fc_builtin.c:100: 
+  Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_unsigned_int_interval
+[eva] Done for function Frama_C_unsigned_int_interval
+[eva] tests/libc/fc_builtin_c.c:17: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:18: Warning: 
+  assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_float_interval <- main.
+  Called from tests/libc/fc_builtin_c.c:20.
+[eva] share/libc/__fc_builtin.c:82: 
+  Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_float_interval
+[eva] Done for function Frama_C_float_interval
+[eva] tests/libc/fc_builtin_c.c:21: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:22: Warning: 
+  assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_double_interval <- main.
+  Called from tests/libc/fc_builtin_c.c:25.
+[eva] share/libc/__fc_builtin.c:88: 
+  Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_double_interval
+[eva] Done for function Frama_C_double_interval
+[eva] tests/libc/fc_builtin_c.c:26: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:27: Warning: 
+  assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_long_interval <- main.
+  Called from tests/libc/fc_builtin_c.c:29.
+[eva] share/libc/__fc_builtin.c:112: 
+  Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_long_interval
+[eva] Done for function Frama_C_long_interval
+[eva] tests/libc/fc_builtin_c.c:30: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:31: Warning: 
+  assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_unsigned_long_interval <- main.
+  Called from tests/libc/fc_builtin_c.c:34.
+[eva] share/libc/__fc_builtin.c:124: 
+  Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_unsigned_long_interval
+[eva] Done for function Frama_C_unsigned_long_interval
+[eva] tests/libc/fc_builtin_c.c:35: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:36: Warning: 
+  assertion 'sampling,unknown' got status unknown.
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function Frama_C_update_entropy:
+  Frama_C_entropy_source ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_double_interval:
+  Frama_C_entropy_source ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_float_interval:
+  Frama_C_entropy_source ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_interval:
+  Frama_C_entropy_source ∈ [--..--]
+  r ∈ [-127..2147483627]
+  aux ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_char_interval:
+  Frama_C_entropy_source ∈ [--..--]
+  __retres ∈ [-127..123]
+[eva:final-states] Values at end of function Frama_C_long_interval:
+  Frama_C_entropy_source ∈ [--..--]
+  r ∈ [-2147483648..-2]
+  aux ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_unsigned_int_interval:
+  Frama_C_entropy_source ∈ [--..--]
+  r ∈ [2147483647..4294967295]
+  aux ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_unsigned_long_interval:
+  Frama_C_entropy_source ∈ [--..--]
+  r ∈ {2147483646; 2147483647; 2147483648}
+  aux ∈ [--..--]
+[eva:final-states] Values at end of function main:
+  Frama_C_entropy_source ∈ [--..--]
+  i ∈ {1073741823}
+  c ∈ {42}
+  ui ∈ {4294957295}
+  f ∈ {1.5}
+  one_e_100 ∈ {1e+100}
+  d ∈ [12345678901.2 .. 12345678901.2]
+  l ∈ {-3}
+  ul ∈ {2147483647}
+  __retres ∈ {0}