[Eva] Tests the reduction by ACSL predicates valid_string and valid_read_string.

tests/value/oracle/strings_logic.res.oracle

+[kernel] Parsing strings_logic.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
+  nondet ∈ [--..--]
+[eva] computing for function reduce_by_valid_string <- main.
+  Called from strings_logic.c:177.
+[eva:loop-unroll:auto] strings_logic.c:30: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:36: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:41: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:48: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:53: Automatic loop unrolling.
+[eva:alarm] strings_logic.c:84: Warning: assertion got status unknown.
+[eva] strings_logic.c:85: 
+  Frama_C_show_each_valid_string_zero_offset:
+  {{ &s1 ; &s2 ; &s_zero ; &s_partially_valid ; &s_imprecise ; &s_unknown ;
+     &anything }}
+[eva:alarm] strings_logic.c:89: Warning: assertion got status unknown.
+[eva] strings_logic.c:90: 
+  Frama_C_show_each_valid_read_string_zero_offset:
+  {{ &s1 ; &s2 ; &s_const ; &s_zero ; &s_partially_valid ; &s_imprecise ;
+     &s_unknown ; &anything ; "hello\000 world" ; "hello world" }}
+[eva:alarm] strings_logic.c:94: Warning: assertion got status unknown.
+[eva] strings_logic.c:95: 
+  Frama_C_show_each_invalid_string_zero_offset:
+  {{ NULL ; &s_const ; &s_uninit ; &s_partially_initialized ; &s_imprecise ;
+     &s_unknown ; &anything ; "hello\000 world" ; "hello world" }}
+[eva:alarm] strings_logic.c:99: Warning: assertion got status unknown.
+[eva] strings_logic.c:100: 
+  Frama_C_show_each_invalid_read_string_zero_offset:
+  {{ NULL ; &s_uninit ; &s_partially_initialized ; &s_imprecise ; &s_unknown ;
+     &anything }}
+[eva:alarm] strings_logic.c:108: Warning: assertion got status unknown.
+[eva] strings_logic.c:109: 
+  Frama_C_show_each_valid_string_precise_offset:
+  {{ &s1 + {5; 10} ; &s2 + {5; 10} ; &s_zero + {5; 10; 20} ;
+     &s_partially_initialized + {5; 10; 20} ;
+     &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+     &s_unknown + {5; 10; 20} ; &anything + {5; 10} }}
+[eva:alarm] strings_logic.c:113: Warning: assertion got status unknown.
+[eva] strings_logic.c:114: 
+  Frama_C_show_each_valid_read_string_precise_offset:
+  {{ &s1 + {5; 10} ; &s2 + {5; 10} ; &s_const + {5; 10} ;
+     &s_zero + {5; 10; 20} ; &s_partially_initialized + {5; 10; 20} ;
+     &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+     &s_unknown + {5; 10; 20} ; &anything + {5; 10} ;
+     "hello\000 world" + {5; 10} ; "hello world" + {5; 10} }}
+[eva:alarm] strings_logic.c:118: Warning: assertion got status unknown.
+[eva] strings_logic.c:119: 
+  Frama_C_show_each_invalid_string_precise_offset:
+  {{ NULL + {5; 10; 20} ; &s1 + {5; 10; 20} ; &s2 + {5; 10; 20} ;
+     &s_const + {5; 10; 20} ; &s_uninit + {5; 10; 20} ;
+     &s_partially_initialized + {5; 10; 20} ;
+     &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+     &s_unknown + {5; 10; 20} ; &anything + {5; 10; 20} ;
+     "hello\000 world" + {5; 10; 20} ; "hello world" + {5; 10; 20} }}
+[eva:alarm] strings_logic.c:123: Warning: assertion got status unknown.
+[eva] strings_logic.c:124: 
+  Frama_C_show_each_invalid_read_string_precise_offset:
+  {{ NULL + {5; 10; 20} ; &s1 + {5; 10; 20} ; &s2 + {5; 10; 20} ;
+     &s_const + {5; 10; 20} ; &s_uninit + {5; 10; 20} ;
+     &s_partially_initialized + {5; 10; 20} ;
+     &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+     &s_unknown + {5; 10; 20} ; &anything + {5; 10; 20} ;
+     "hello\000 world" + {5; 10; 20} ; "hello world" + {5; 10; 20} }}
+[eva:alarm] strings_logic.c:131: Warning: assertion got status unknown.
+[eva] strings_logic.c:132: 
+  Frama_C_show_each_valid_string_imprecise_offset:
+  {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_zero + [0..31] ;
+     &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+     &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] }}
+[eva:alarm] strings_logic.c:136: Warning: assertion got status unknown.
+[eva] strings_logic.c:137: 
+  Frama_C_show_each_valid_read_string_imprecise_offset:
+  {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_const + [0..16] ; &s_zero + [0..31] ;
+     &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+     &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] ;
+     "hello\000 world" + [0..12] ; "hello world" + [0..11] }}
+[eva:alarm] strings_logic.c:141: Warning: assertion got status unknown.
+[eva] strings_logic.c:142: 
+  Frama_C_show_each_invalid_string_imprecise_offset:
+  {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+     &s_const + [-123..147] ; &s_zero + [-123..147] ; &s_uninit + [-123..147] ;
+     &s_partially_initialized + [-123..147] ;
+     &s_partially_valid + [-123..147] ; &s_imprecise + [-123..147] ;
+     &s_unknown + [-123..147] ; &anything + [-123..147] ;
+     "hello\000 world" + [-123..147] ; "hello world" + [-123..147] }}
+[eva:alarm] strings_logic.c:146: Warning: assertion got status unknown.
+[eva] strings_logic.c:147: 
+  Frama_C_show_each_invalid_read_string_imprecise_offset:
+  {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+     &s_const + [-123..147] ; &s_zero + [-123..147] ; &s_uninit + [-123..147] ;
+     &s_partially_initialized + [-123..147] ;
+     &s_partially_valid + [-123..147] ; &s_imprecise + [-123..147] ;
+     &s_unknown + [-123..147] ; &anything + [-123..147] ;
+     "hello\000 world" + [-123..147] ; "hello world" + [-123..147] }}
+[eva] computing for function garbled_mix <- reduce_by_valid_string <- main.
+  Called from strings_logic.c:151.
+[eva] using specification for function garbled_mix
+[eva:garbled-mix:assigns] strings_logic.c:151: 
+  The specification of function garbled_mix
+  has generated a garbled mix of addresses for assigns clause \result.
+[eva] Done for function garbled_mix
+[eva:alarm] strings_logic.c:154: Warning: assertion got status unknown.
+[eva] strings_logic.c:155: 
+  Frama_C_show_each_valid_string_garbled_mix:
+  {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_zero + [0..31] ;
+     &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+     &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] }}
+[eva:alarm] strings_logic.c:159: Warning: assertion got status unknown.
+[eva] strings_logic.c:160: 
+  Frama_C_show_each_valid_read_string_garbled_mix:
+  {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_const + [0..16] ; &s_zero + [0..31] ;
+     &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+     &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] ;
+     "hello\000 world" + [0..12] ; "hello world" + [0..11] }}
+[eva:alarm] strings_logic.c:164: Warning: assertion got status unknown.
+[eva] strings_logic.c:165: 
+  Frama_C_show_each_invalid_string_garbled_mix:
+  {{ garbled mix of &{s1; s2; s_const; s_zero; s_uninit;
+                      s_partially_initialized; s_partially_valid; s_imprecise;
+                      s_unknown; anything; "hello\000 world"; "hello world"}
+  (origin: Library function {strings_logic.c:151}) }}
+[eva:alarm] strings_logic.c:169: Warning: assertion got status unknown.
+[eva] strings_logic.c:170: 
+  Frama_C_show_each_invalid_read_string_garbled_mix:
+  {{ garbled mix of &{s1; s2; s_const; s_zero; s_uninit;
+                      s_partially_initialized; s_partially_valid; s_imprecise;
+                      s_unknown; anything; "hello\000 world"; "hello world"}
+  (origin: Library function {strings_logic.c:151}) }}
+[eva] Recording results for reduce_by_valid_string
+[eva] Done for function reduce_by_valid_string
+[eva] Recording results for main
+[eva] Done for function main
+[eva:garbled-mix:summary] 
+  Origins of garbled mix generated during analysis:
+    strings_logic.c:151: assigns clause on addresses
+      (read in 2 statements, propagated through 1 statement)
+      garbled mix of &{s1; s2; s_const; s_zero; s_uninit;
+                       s_partially_initialized; s_partially_valid; s_imprecise;
+                       s_unknown; anything; "hello\000 world"; "hello world"}
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function reduce_by_valid_string:
+  s1[0] ∈ {104}
+    [1] ∈ {101}
+    [2..3] ∈ {108}
+    [4] ∈ {111}
+    [5] ∈ {0}
+    [6] ∈ {32}
+    [7] ∈ {119}
+    [8] ∈ {111}
+    [9] ∈ {114}
+    [10] ∈ {108}
+    [11] ∈ {100}
+    [12] ∈ {33}
+    [13] ∈ {0}
+  s2[0] ∈ {104}
+    [1] ∈ {101}
+    [2..3] ∈ {108}
+    [4] ∈ {111}
+    [5] ∈ {32}
+    [6] ∈ {119}
+    [7] ∈ {111}
+    [8] ∈ {114}
+    [9] ∈ {108}
+    [10] ∈ {100}
+    [11] ∈ {33}
+    [12] ∈ {0}
+  s_const[0] ∈ {99}
+         [1] ∈ {111}
+         [2] ∈ {110}
+         [3] ∈ {115}
+         [4] ∈ {116}
+         [5] ∈ {32}
+         [6] ∈ {99}
+         [7] ∈ {104}
+         [8] ∈ {97}
+         [9] ∈ {114}
+         [10] ∈ {32}
+         [11] ∈ {97}
+         [12..13] ∈ {114}
+         [14] ∈ {97}
+         [15] ∈ {121}
+         [16] ∈ {0}
+  s_zero[0..31] ∈ {0}
+  s_partially_initialized[0..9] ∈ UNINITIALIZED
+                         [10..24] ∈ {105}
+                         [25] ∈ {0}
+                         [26..31] ∈ UNINITIALIZED
+  s_invalid[0..31] ∈ {97}
+  s_partially_valid[0..7] ∈ {111}
+                   [8] ∈ {0}
+                   [9..15] ∈ {111}
+                   [16] ∈ {0}
+                   [17..31] ∈ {111}
+  s_imprecise[0..31] ∈ [--..--]
+  s_unknown[0..31] ∈ [--..--] or UNINITIALIZED
+  anything.ptr ∈ {{ &x }}
+          .d ∈ [-128. .. 127.]
+          .c ∈ [--..--]
+          .[bits 104 to 127] ∈ UNINITIALIZED
+  p ∈ {0}
+  offset ∈ {5; 10; 20}
+[eva:final-states] Values at end of function main:
+  
+[from] Computing for function reduce_by_valid_string
+[from] Computing for function garbled_mix <-reduce_by_valid_string
+[from] Done for function garbled_mix
+[from] Done for function reduce_by_valid_string
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function garbled_mix:
+  \result FROM p
+[from] Function reduce_by_valid_string:
+  NO EFFECTS
+[from] Function main:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function reduce_by_valid_string:
+    s1[0..13]; s2[0..12]; s_const[0..16]; s_zero[0..31];
+    s_partially_initialized[10..25]; i; s_invalid[0..31]; i_0;
+    s_partially_valid[0..31]; i_1; s_imprecise[0..31]; i_2; s_unknown[0..31];
+    i_3; anything{.ptr; .d; .c}; p; offset; tmp; tmp_0
+[inout] Inputs for function reduce_by_valid_string:
+    nondet
+[inout] Out (internal) for function main:
+    \nothing
+[inout] Inputs for function main:
+    nondet

tests/value/oracle_multidim/strings_logic.res.oracle

+83c83
+<   {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+---
+>   {{ NULL + [0..147] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+92c92
+<   {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+---
+>   {{ NULL + [0..147] ; &s1 + [-123..147] ; &s2 + [-123..147] ;

tests/value/strings_logic.c

+/* run.config*
+   STDOPT: +"-eva-auto-loop-unroll 32"
+*/
+
+/* Tests the evaluation and reduction by ACSL predicate on strings. */
+
+#include "__fc_string_axiomatic.h"
+
+volatile char nondet;
+
+struct anything {
+  int *ptr;
+  double d;
+  char c;
+};
+
+/*@ assigns \result \from p; */
+char* garbled_mix(char *p);
+
+/* Tests the reduction by ACSL predicate "valid_string" and "valid_read_string"
+   from the Frama-C libc. */
+void reduce_by_valid_string (void) {
+  char s1[] = "hello\000 world!";
+  char s2[] = "hello world!";
+  const char s_const[] = "const char array";
+  char s_zero[32] = {0};
+  char s_uninit[32];
+
+  char s_partially_initialized[32]; // valid only between 10 and 25.
+  for (int i = 10; i < 25; i++) {
+    s_partially_initialized[i] = 'i';
+  }
+  s_partially_initialized[25] = '\0';
+
+  char s_invalid[32]; // Invalid as no terminating \0
+  for (int i = 0; i < 32; i++){
+    s_invalid[i] = 'a';
+  }
+
+  char s_partially_valid[32]; // valid up to offset 16.
+  for (int i = 0; i < 32; i++){
+    s_partially_valid[i] = 'o';
+  }
+  s_partially_valid[8] = '\0';
+  s_partially_valid[16] = '\0';
+
+  char s_imprecise[32]; // char array of imprecise values
+  for (int i = 0; i < 32; i++){
+    s_imprecise[i] = nondet;
+  }
+
+  char s_unknown[32]; // char array of imprecise values that may be uninitialized
+  for (int i = 0; i < 32; i++) {
+    if (nondet) s_unknown[i] = nondet;
+  }
+
+  int x;
+  struct anything anything;
+  anything.ptr = &x;
+  anything.d = (double)nondet;
+  anything.c = nondet;
+
+  // Pointer p that can point to any of the strings above.
+  char *p;
+  switch (nondet) {
+    case 0: p = "hello\000 world"; break;
+    case 1: p = "hello world"; break;
+    case 2: p = s1; break;
+    case 3: p = s2; break;
+    case 4: p = s_const; break;
+    case 5: p = s_zero; break;
+    case 6: p = s_uninit; break;
+    case 7: p = s_partially_initialized; break;
+    case 8: p = s_partially_valid; break;
+    case 9: p = s_imprecise; break;
+    case 10: p = s_unknown; break;
+    case 11: p = (char *)&anything; break;
+    default: p = NULL;
+  }
+
+  // Test with a zero offset for all bases.
+
+  if (nondet) {
+    //@ assert valid_string(p);
+    Frama_C_show_each_valid_string_zero_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert valid_read_string(p);
+    Frama_C_show_each_valid_read_string_zero_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_string(p);
+    Frama_C_show_each_invalid_string_zero_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_read_string(p);
+    Frama_C_show_each_invalid_read_string_zero_offset(p);
+  }
+
+  // Test with a precise non-zero non-singleton offset.
+  int offset = nondet ? 5 : (nondet ? 10 : 20);
+  p = p + offset;
+
+  if (nondet) {
+    //@ assert valid_string(p);
+    Frama_C_show_each_valid_string_precise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert valid_read_string(p);
+    Frama_C_show_each_valid_read_string_precise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_string(p);
+    Frama_C_show_each_invalid_string_precise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_read_string(p);
+    Frama_C_show_each_invalid_read_string_precise_offset(p);
+  }
+
+  // Test with a very imprecise offset.
+  p = p + nondet;
+
+  if (nondet) {
+    //@ assert valid_string(p);
+    Frama_C_show_each_valid_string_imprecise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert valid_read_string(p);
+    Frama_C_show_each_valid_read_string_imprecise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_string(p);
+    Frama_C_show_each_invalid_string_imprecise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_read_string(p);
+    Frama_C_show_each_invalid_read_string_imprecise_offset(p);
+  }
+
+  // Test with a garbled mix.
+  p = garbled_mix(p);
+
+  if (nondet) {
+    //@ assert valid_string(p);
+    Frama_C_show_each_valid_string_garbled_mix(p);
+  }
+
+  if (nondet) {
+    //@ assert valid_read_string(p);
+    Frama_C_show_each_valid_read_string_garbled_mix(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_string(p);
+    Frama_C_show_each_invalid_string_garbled_mix(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_read_string(p);
+    Frama_C_show_each_invalid_read_string_garbled_mix(p);
+  }
+
+  p = NULL;
+}
+
+void main (void) {
+  reduce_by_valid_string();
+}