[Eva] Adds a test for string builtins applied on misaligned offsetmap or pointer.

tests/builtins/oracle/wcslen.res.oracle

@@ -31,7 +31,7 @@
                      [11] ∈ {100}
   nondet ∈ [--..--]
 [eva] computing for function small_sets <- main.
-  Called from tests/builtins/wcslen.c:339.
+  Called from tests/builtins/wcslen.c:370.
 [eva] tests/builtins/wcslen.c:60: Call to builtin wcslen
 [eva] tests/builtins/wcslen.c:60: 
   function wcslen: precondition 'valid_string_s' got status valid.
@@ -55,7 +55,7 @@
 [eva] Recording results for small_sets
 [eva] Done for function small_sets
 [eva] computing for function zero_termination <- main.
-  Called from tests/builtins/wcslen.c:340.
+  Called from tests/builtins/wcslen.c:371.
 [eva] tests/builtins/wcslen.c:89: Call to builtin wcslen
 [eva:alarm] tests/builtins/wcslen.c:89: Warning: 
   function wcslen: precondition 'valid_string_s' got status unknown.
@@ -69,7 +69,7 @@
 [eva] Recording results for zero_termination
 [eva] Done for function zero_termination
 [eva] computing for function wcslen_initialization <- main.
-  Called from tests/builtins/wcslen.c:341.
+  Called from tests/builtins/wcslen.c:372.
 [eva] tests/builtins/wcslen.c:105: Call to builtin wcslen
 [eva:alarm] tests/builtins/wcslen.c:105: Warning: 
   function wcslen: precondition 'valid_string_s' got status unknown.
@@ -88,7 +88,7 @@
 [eva] Recording results for wcslen_initialization
 [eva] Done for function wcslen_initialization
 [eva] computing for function wcslen_large <- main.
-  Called from tests/builtins/wcslen.c:342.
+  Called from tests/builtins/wcslen.c:373.
 [eva] computing for function init_array_nondet <- wcslen_large <- main.
   Called from tests/builtins/wcslen.c:168.
 [eva] tests/builtins/wcslen.c:161: Call to builtin memset
@@ -152,7 +152,7 @@
 [eva] Recording results for wcslen_large
 [eva] Done for function wcslen_large
 [eva] computing for function wcslen_large_uninit <- main.
-  Called from tests/builtins/wcslen.c:343.
+  Called from tests/builtins/wcslen.c:374.
 [eva] computing for function init_array_nondet <- wcslen_large_uninit <- main.
   Called from tests/builtins/wcslen.c:197.
 [eva] tests/builtins/wcslen.c:161: Call to builtin memset
@@ -193,7 +193,7 @@
 [eva] Recording results for wcslen_large_uninit
 [eva] Done for function wcslen_large_uninit
 [eva] computing for function misc <- main.
-  Called from tests/builtins/wcslen.c:344.
+  Called from tests/builtins/wcslen.c:375.
 [eva] tests/builtins/wcslen.c:241: Call to builtin wcslen
 [eva:alarm] tests/builtins/wcslen.c:241: Warning: 
   function wcslen: precondition 'valid_string_s' got status invalid.
@@ -245,14 +245,14 @@
 [eva] Recording results for misc
 [eva] Done for function misc
 [eva] computing for function bitfields <- main.
-  Called from tests/builtins/wcslen.c:345.
+  Called from tests/builtins/wcslen.c:376.
 [eva] tests/builtins/wcslen.c:140: Call to builtin wcslen
 [eva:alarm] tests/builtins/wcslen.c:140: Warning: 
   function wcslen: precondition 'valid_string_s' got status invalid.
 [eva] Recording results for bitfields
 [eva] Done for function bitfields
 [eva] computing for function bitfields2 <- main.
-  Called from tests/builtins/wcslen.c:346.
+  Called from tests/builtins/wcslen.c:377.
 [eva] tests/builtins/wcslen.c:155: Call to builtin wcslen
 [eva] tests/builtins/wcslen.c:155: 
   function wcslen: precondition 'valid_string_s' got status valid.
@@ -260,7 +260,7 @@
 [eva] Recording results for bitfields2
 [eva] Done for function bitfields2
 [eva] computing for function escaping <- main.
-  Called from tests/builtins/wcslen.c:347.
+  Called from tests/builtins/wcslen.c:378.
 [eva:alarm] tests/builtins/wcslen.c:222: Warning: 
   pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
 [eva:alarm] tests/builtins/wcslen.c:222: Warning: 
@@ -282,7 +282,7 @@
 [eva] Recording results for escaping
 [eva] Done for function escaping
 [eva] computing for function big_array <- main.
-  Called from tests/builtins/wcslen.c:348.
+  Called from tests/builtins/wcslen.c:379.
 [eva:alarm] tests/builtins/wcslen.c:287: Warning: 
   out of bounds write. assert \valid(p);
 [eva:alarm] tests/builtins/wcslen.c:291: Warning: 
@@ -312,7 +312,7 @@
 [eva] Recording results for big_array
 [eva] Done for function big_array
 [eva] computing for function negative_offsets <- main.
-  Called from tests/builtins/wcslen.c:349.
+  Called from tests/builtins/wcslen.c:380.
 [eva] tests/builtins/wcslen.c:314: starting to merge loop iterations
 [eva] computing for function Frama_C_interval <- negative_offsets <- main.
   Called from tests/builtins/wcslen.c:318.
@@ -364,6 +364,32 @@
   function wcslen: precondition 'valid_string_s' got status unknown.
 [eva] Recording results for negative_offsets
 [eva] Done for function negative_offsets
+[eva] computing for function misaligned_string <- main.
+  Called from tests/builtins/wcslen.c:381.
+[eva] tests/builtins/wcslen.c:345: assertion got status valid.
+[eva] tests/builtins/wcslen.c:346: Call to builtin wcslen
+[eva] tests/builtins/wcslen.c:346: 
+  function wcslen: precondition 'valid_string_s' got status valid.
+[eva] computing for function Frama_C_interval <- misaligned_string <- main.
+  Called from tests/builtins/wcslen.c:350.
+[eva] tests/builtins/wcslen.c:350: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] tests/builtins/wcslen.c:351: Warning: 
+  out of bounds write. assert \valid((char *)((wchar_t *)b) + i);
+[eva:alarm] tests/builtins/wcslen.c:352: Warning: assertion got status unknown.
+[eva] tests/builtins/wcslen.c:353: Call to builtin wcslen
+[eva:alarm] tests/builtins/wcslen.c:353: Warning: 
+  function wcslen: precondition 'valid_string_s' got status unknown.
+[eva:alarm] tests/builtins/wcslen.c:361: Warning: assertion got status unknown.
+[eva] tests/builtins/wcslen.c:362: Call to builtin wcslen
+[eva:alarm] tests/builtins/wcslen.c:362: Warning: 
+  function wcslen: precondition 'valid_string_s' got status unknown.
+[eva] tests/builtins/wcslen.c:365: Call to builtin wcslen
+[eva:alarm] tests/builtins/wcslen.c:365: Warning: 
+  function wcslen: precondition 'valid_string_s' got status invalid.
+[eva] Recording results for misaligned_string
+[eva] Done for function misaligned_string
 [eva] Recording results for main
 [eva] done for function main
 [scope:rm_asserts] removing 3 assertion(s)
@@ -405,6 +431,24 @@
    [1..3] ∈ ESCAPINGADDR
   z1 ∈ {0}
   z2 ∈ {0}
+[eva:final-states] Values at end of function misaligned_string:
+  Frama_C_entropy_source ∈ [--..--]
+  a[0][bits 0 to 7] ∈ {1}
+   [0][bits 8 to 31] ∈ {0}
+   [1] ∈ {1}
+   [2] ∈ {0}
+  a_length ∈ {2}
+  b[0..9999999]# ∈ {0; 17} repeated %8 
+  i ∈ [0..39999999]
+  b_length ∈ [0..9999999]
+  c[0][bits 0 to 7] ∈ {0}
+   {[0][bits 8 to 31]#; [1][bits 0 to 7]#} ∈ {1}
+   {[1][bits 8 to 31]#; [2][bits 0 to 7]#} ∈ {2}
+   {[2][bits 8 to 31]; [3][bits 0 to 7]} ∈ {0}
+   {[3][bits 8 to 31]#; [4][bits 0 to 7]#} ∈ {4}
+   [4][bits 8 to 31] ∈ {0}
+  p ∈ {{ &c + {1} }}
+  c_length ∈ {2}
 [eva:final-states] Values at end of function misc:
   Frama_C_entropy_source ∈ [--..--]
   loc_str ∈ {{ L"Bonjour Monde\n" }}
@@ -524,9 +568,11 @@
 [from] Done for function bitfields2
 [from] Computing for function escaping
 [from] Done for function escaping
-[from] Computing for function misc
-[from] Computing for function Frama_C_interval <-misc
+[from] Computing for function misaligned_string
+[from] Computing for function Frama_C_interval <-misaligned_string
 [from] Done for function Frama_C_interval
+[from] Done for function misaligned_string
+[from] Computing for function misc
 [from] Done for function misc
 [from] Computing for function negative_offsets
 [from] Done for function negative_offsets
@@ -560,7 +606,8 @@
                non_terminated2[2..3]; empty_or_uninitialized[0];
                uninitialized[0]; s[0..1]; t[0..3]; s; s; a[3..99]; a[3..99];
                s[0..3]; loc_char_array[0..4]; x[0..3]; maybe_init[0..1];
-               t[0..999999]; u[0..199]; r[0..200]; buf[0..99];
+               t[0..999999]; u[0..199]; r[0..200]; buf[0..99]; a[0..2];
+               b[0..9999999]; c{[0][bits 8 to 31]; [1..3]; [4][bits 0 to 7]};
                L"Hello World\n"[bits 0 to 415];
                L"abc\000\000\000abc"[bits 0 to 319]; L""; L"a"[bits 0 to 63];
                L"aa"[bits 0 to 95]; L"aaa"[bits 0 to 127];
@@ -582,6 +629,8 @@
   NO EFFECTS
 [from] Function escaping:
   NO EFFECTS
+[from] Function misaligned_string:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
 [from] Function misc:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
 [from] Function negative_offsets:
@@ -620,6 +669,11 @@
     s[0..3]; z1; tmp; z2; tmp_0
 [inout] Inputs for function escaping:
     nondet
+[inout] Out (internal) for function misaligned_string:
+    Frama_C_entropy_source; a[0..2]; a_length; b[0..9999999]; i; b_length;
+    c[0..4]; p; c_length
+[inout] Inputs for function misaligned_string:
+    Frama_C_entropy_source; nondet
 [inout] Out (internal) for function misc:
     Frama_C_entropy_source; loc_str; loc_char_array[3]; sz1; sz2; sz3; 
     sz4; sz5; sz6; sz7; sz8; x[0..3]; z[0..3]; i; str; s1; tmp; s2; tmp_0; 

tests/builtins/wcslen.c

@@ -335,6 +335,37 @@ void negative_offsets() {
   wchar_t dest[100 * 2];
 }
 
+#define MAX 10000000
+
+void misaligned_string () {
+  // Read an offsetmap with a value range smaller than the read characters.
+  wchar_t a[3] = {0};
+  *(char *)a = 1;
+  a[1] = 1;
+  //@ assert valid_read_wstring(&a[0]);
+  unsigned int a_length = wcslen(&a[0]);
+  /* Read an offsetmap with repeated values smaller than the searched
+     characters: test a performance issue. */
+  wchar_t b[MAX] = {0};
+  int i = Frama_C_interval(0, MAX * 4);
+  *((char *)b + i) = (char)17;
+  //@ assert valid_read_wstring(&b[0]);
+  unsigned int b_length = wcslen(&b[0]);
+  /* Read an offsetmap through a misaligned pointer. */
+  wchar_t c[5] = {0};
+  wchar_t *p = (wchar_t *)( (char *)c + 1);
+  *p = 1;
+  *(p+1) = 2;
+  *(p+2) = 0; // If we accept the string pointed by p, its length should be 2.
+  *(p+3) = 4;
+  //@ assert valid_read_wstring(p);
+  unsigned int c_length = wcslen(p);
+  if (nondet) {
+    *(p+2) = 3; // The string pointed by p cannot be valid here.
+    c_length = wcslen(p);
+  }
+}
+
 int main (int c) {
   small_sets();
   zero_termination();
@@ -347,5 +378,6 @@ int main (int c) {
   escaping();
   big_array();
   negative_offsets();
+  misaligned_string();
   return 0;
 }