diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index 6af4807ad9b794215796de279d6fd12c749bf790..64b75c8765fc4219d2c831d6d1f165cd59197ca2 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -286,41 +286,6 @@ module Location_Bytes = struct
| Base.Variable { Base.weak } -> not weak
with Not_found -> false
- let iter_on_strings =
- let z = "\000" in
- fun ~skip f l ->
- match l with
- | Top _ ->
- assert false
- | Map m ->
- M.iter
- (fun base offs ->
- match skip with
- Some base_to_skip when Base.equal base base_to_skip -> ()
- | _ ->
- match base with
- Base.String (_, strid) ->
- let str =
- match strid with
- | Base.CSString s -> s
- | Base.CSWstring _ ->
- failwith "Unimplemented: wide strings"
- in
- let strz = str ^ z in
- let len = String.length str in
- let range =
- Ival.inject_range
- (Some Int.zero)
- (Some (Int.of_int len))
- in
- let roffs = Ival.narrow range offs in
- Ival.fold_int
- (fun i () -> f base strz (Int.to_int i) len)
- roffs
- ()
- | _ -> ())
- m
-
let topify_merge_origin v =
topify_with_origin_kind Origin.K_Merge v
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index f96d8f6bccf067d275003dec375f9f13a8bb9d5d..b8de6dce344930a6d04a3a1b97088f0a966d7976 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -194,9 +194,6 @@ module Location_Bytes : sig
(** {2 Misc} *)
- val iter_on_strings :
- skip:Base.t option -> (Base.t -> string -> int -> int -> unit) -> t -> unit
-
(** [is_relationable loc] returns [true] iff [loc] represents a single
memory location. *)
val is_relationable: t -> bool
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index 6822e5f5a5c0218144b3776f9d489431f8c63b9e..91263cb385821059a3a9b72b50ad514a788a35f0 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -28,28 +28,54 @@ open Abstract_value
Comparison
-------------------------------------------------------------------------- *)
+(* Representation of a pointer value to a literal string, with the string
+ itself, its length and the offsets pointed to in the string. *)
+type str = { string: string; offset: Ival.t; length: int; }
+
+(* Returns true if one string is a suffix of the other, and if there are offsets
+ pointing to the same point in this suffix. *)
+let may_be_suffix s1 s2 =
+ (* Requires [s1.length] <= [s2.length]. *)
+ let is_suffix s1 s2 =
+ let sub2 = String.sub s2.string (s2.length - s1.length) s1.length in
+ String.equal s1.string sub2 &&
+ let delta = Integer.of_int (s1.length - s2.length) in
+ let off2 = Ival.add_singleton_int delta s2.offset in
+ not (Ival.is_bottom (Ival.narrow s1.offset off2))
+ in
+ if s1.length <= s2.length then is_suffix s1 s2 else is_suffix s2 s1
+
+(* Returns true if [s1] may be shared with [s2] or a substring of [s2]. *)
+let rec may_be_shared_within s1 s2 =
+ may_be_suffix s1 s2 ||
+ match String.rindex_opt s2.string '\x00' with
+ | None -> false
+ | Some i ->
+ let s2 = { s2 with string = String.sub s2.string 0 i; length = i } in
+ may_be_shared_within s1 s2
+
+(* Returns true if [s1] and [s2] might point to the same literal string. *)
+let may_be_shared str1 off1 str2 off2 =
+ let s1 = { string = str1; offset = off1; length = String.length str1 }
+ and s2 = { string = str2; offset = off2; length = String.length str2 } in
+ may_be_shared_within s1 s2 || may_be_shared_within s2 s1
+
+(* Checks if all string bases of [v] satisfy [f]. *)
+let for_all_string v f =
+ Locations.Location_Bytes.for_all
+ (fun base off -> match base with
+ | Base.String (_, Base.CSString str) -> f base str off
+ | Base.String (_, Base.CSWstring _ ) -> false (* Not implemented yet *)
+ | _ -> true)
+ v
+
(* Literal strings can only be compared if their contents are recognizably
different (or the strings are physically the same). *)
-let are_comparable_string pointer1 pointer2 =
- try
- Locations.Location_Bytes.iter_on_strings ~skip:None
- (fun base1 s1 offs1 len1 ->
- Locations.Location_Bytes.iter_on_strings ~skip:(Some base1)
- (fun _ s2 offs2 len2 ->
- let delta = offs1 - offs2 in
- let start = if delta <= 0 then -delta else 0
- and max = min len2 (len1 - delta) in
- let length = max - start + 1 in
- let sub1 = String.sub s1 (start + delta) length
- and sub2 = String.sub s2 start length in
- if String.compare sub1 sub2 = 0
- then raise Not_found)
- pointer1)
- pointer2;
- true
- with
- | Not_found -> false
- | Invalid_argument _s -> assert false
+let are_comparable_string v1 v2 =
+ for_all_string v1 (fun base1 str1 off1 ->
+ for_all_string v2 (fun base2 str2 off2 ->
+ Base.equal base1 base2 ||
+ not (may_be_shared str1 off1 str2 off2)))
(* Under-approximation of the fact that a pointer is actually correct w.r.t.
what can be created through pointer arithmetics. See C99 6.5.6 and 6.5.8
diff --git a/tests/value/oracle/strings.0.res.oracle b/tests/value/oracle/strings.0.res.oracle
deleted file mode 100644
index f82b23c4a9e97d73b6db8238c657b9fee2c9bc52..0000000000000000000000000000000000000000
--- a/tests/value/oracle/strings.0.res.oracle
+++ /dev/null
@@ -1,152 +0,0 @@
-[kernel] Parsing tests/value/strings.i (no preprocessing)
-[eva] Analyzing a complete application starting at main1
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- 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] ∈ {0}
- s2[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- s5 ∈ {0}
- s6 ∈ {0}
- cc ∈ {97}
- Q ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0}
- U ∈ {0}
- V ∈ {0}
- W ∈ {0}
- X ∈ {0}
- Y ∈ {0}
- Z ∈ {0}
- s3 ∈ {{ "tutu" }}
- s4 ∈ {{ "tutu" }}
- s7 ∈ {{ "hello\000 world" }}
- s8 ∈ {{ "hello" }}
-[eva] computing for function u <- main1.
- Called from tests/value/strings.i:39.
-[kernel:annot:missing-spec] tests/value/strings.i:39: Warning:
- Neither code nor specification for function u, generating default assigns from the prototype
-[eva] using specification for function u
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:39: Warning:
- out of bounds read. assert \valid_read(p - 4);
-[eva] computing for function u <- main1.
- Called from tests/value/strings.i:42.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:42: Warning:
- out of bounds read. assert \valid_read(p + 12);
-[eva] computing for function u <- main1.
- Called from tests/value/strings.i:44.
-[eva] Done for function u
-[eva] computing for function u <- main1.
- Called from tests/value/strings.i:48.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:48: Warning:
- out of bounds read. assert \valid_read(p - 4);
-[eva] computing for function u <- main1.
- Called from tests/value/strings.i:53.
-[eva] Done for function u
-[eva] computing for function strcpy <- main1.
- Called from tests/value/strings.i:53.
-[eva:alarm] tests/value/strings.i:21: Warning:
- out of bounds write.
- assert \valid(tmp_unroll_46);
- (tmp_unroll_46 from ldst++)
-[kernel] tests/value/strings.i:21: Warning:
- all target addresses were invalid. This path is assumed to be dead.
-[eva] Recording results for strcpy
-[eva] Done for function strcpy
-[eva] computing for function strlen <- main1.
- Called from tests/value/strings.i:58.
-[eva] Recording results for strlen
-[eva] Done for function strlen
-[eva] Recording results for main1
-[eva] done for function main1
-[eva] tests/value/strings.i:21:
- assertion 'Eva,mem_access' got final status invalid.
-[eva] tests/value/strings.i:39:
- assertion 'Eva,mem_access' got final status invalid.
-[eva] tests/value/strings.i:42:
- assertion 'Eva,mem_access' got final status invalid.
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function strcpy:
- NON TERMINATING FUNCTION
-[eva:final-states] Values at end of function strlen:
- s ∈ {{ &s1[6] }}
- l ∈ {5}
-[eva:final-states] Values at end of function main1:
- s1[0] ∈ {104}
- [1] ∈ {101}
- [2] ∈ {108}
- [3] ∈ {97}
- [4] ∈ {111}
- [5] ∈ {0}
- [6] ∈ {97}
- [7] ∈ {119}
- [8] ∈ {111}
- [9] ∈ {114}
- [10] ∈ {108}
- [11] ∈ {100}
- [12] ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0; 101}
- p ∈ {{ &s1[5] ; &s2[3] }}
- __retres ∈ {5}
-[from] Computing for function strcpy
-[from] Non-terminating function strcpy (no dependencies)
-[from] Done for function strcpy
-[from] Computing for function strlen
-[from] Done for function strlen
-[from] Computing for function main1
-[from] Computing for function u <-main1
-[from] Done for function u
-[from] Done for function main1
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function strcpy:
- NON TERMINATING - NO EFFECTS
-[from] Function strlen:
- \result FROM s1[0..4]; s
-[from] Function u:
- \result FROM \nothing
-[from] Function main1:
- s1{[3]; [6]} FROM cc
- R FROM \nothing (and SELF)
- S FROM \nothing (and SELF)
- T FROM s1[1] (and SELF)
- \result FROM s1{[0..2]; [4]}; cc
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function strcpy:
- src; ldst; b[0..4]; tmp_unroll_46; tmp_1_unroll_46; tmp_0_unroll_46;
- tmp_unroll_49; tmp_1_unroll_49; tmp_0_unroll_49; tmp_unroll_52;
- tmp_1_unroll_52; tmp_0_unroll_52; tmp_unroll_55; tmp_1_unroll_55;
- tmp_0_unroll_55; tmp_unroll_58; tmp_1_unroll_58; tmp_0_unroll_58;
- tmp_unroll_61; tmp_1_unroll_61; tmp_0_unroll_61
-[inout] Inputs for function strcpy:
- a[0..5]
-[inout] Out (internal) for function strlen:
- s; l; tmp_unroll_106; tmp_unroll_109; tmp_unroll_112; tmp_unroll_115;
- tmp_unroll_118; tmp_unroll_121
-[inout] Inputs for function strlen:
- s1[0..5]
-[inout] Out (internal) for function main1:
- s1{[3]; [6]}; R; S; T; p; tmp; tmp_0; tmp_1; tmp_2; a[0..9]; b[0..4];
- tmp_3; tmp_4; __retres
-[inout] Inputs for function main1:
- s1[0..5]; cc
diff --git a/tests/value/oracle/strings.1.res.oracle b/tests/value/oracle/strings.1.res.oracle
deleted file mode 100644
index cf5a4433579e96602d54f51e4a713f7e1c7fe4d9..0000000000000000000000000000000000000000
--- a/tests/value/oracle/strings.1.res.oracle
+++ /dev/null
@@ -1,145 +0,0 @@
-[kernel] Parsing tests/value/strings.i (no preprocessing)
-[eva] Analyzing a complete application starting at main6
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- 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] ∈ {0}
- s2[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- s5 ∈ {0}
- s6 ∈ {0}
- cc ∈ {97}
- Q ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0}
- U ∈ {0}
- V ∈ {0}
- W ∈ {0}
- X ∈ {0}
- Y ∈ {0}
- Z ∈ {0}
- s3 ∈ {{ "tutu" }}
- s4 ∈ {{ "tutu" }}
- s7 ∈ {{ "hello\000 world" }}
- s8 ∈ {{ "hello" }}
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:72.
-[kernel:annot:missing-spec] tests/value/strings.i:72: Warning:
- Neither code nor specification for function u, generating default assigns from the prototype
-[eva] using specification for function u
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:73: Warning:
- pointer comparison. assert \pointer_comparable((void *)s3, (void *)s4);
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:74.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:76.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:78.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:79: Warning:
- pointer comparison. assert \pointer_comparable((void *)s7, (void *)s8);
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:80.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:82.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:83: Warning:
- pointer comparison.
- assert \pointer_comparable((void *)(s7 + 1), (void *)(s8 + 1));
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:84.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:86.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:87.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:88.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:89.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:89.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:90.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:91: Warning:
- pointer comparison. assert \pointer_comparable((void *)s5, (void *)s6);
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:92.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:93: Warning:
- pointer comparison.
- assert \pointer_comparable((void *)("oh, hello" + 4), (void *)s7);
-[eva] Recording results for main6
-[eva] done for function main6
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main6:
- s5 ∈ {{ "tutu" ; "hello" }}
- s6 ∈ {{ "tutu" ; "tutu" ; "hello" }}
- cc ∈ {116}
- Q ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0}
- U ∈ {0}
- V ∈ {0}
- W ∈ {0}
- X ∈ {0; 1}
- Y ∈ {0; 1}
- Z ∈ {0; 1}
- s ∈ {{ "toto" }}
- __retres ∈ {116}
-[from] Computing for function main6
-[from] Computing for function u <-main6
-[from] Done for function u
-[from] Done for function main6
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function u:
- \result FROM \nothing
-[from] Function main6:
- s5 FROM s3; s8
- s6 FROM s3; s4; s8
- cc FROM "toto"[bits 0 to 7]
- Q FROM s7 (and SELF)
- R FROM s3; s4 (and SELF)
- S FROM \nothing (and SELF)
- T FROM s3 (and SELF)
- U FROM s7; s8 (and SELF)
- V FROM s4; s7 (and SELF)
- W FROM s7; s8 (and SELF)
- X FROM s3 (and SELF)
- Y FROM s3; s8 (and SELF)
- Z FROM s3; s4; s8 (and SELF)
- \result FROM "toto"[bits 0 to 7]
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main6:
- s5; s6; cc; Q; R; S; T; U; V; W; X; Y; Z; s; tmp; tmp_0; tmp_1; tmp_2;
- tmp_3; tmp_4; tmp_5; tmp_6; tmp_7; tmp_8; tmp_9; tmp_10; tmp_11; tmp_12;
- tmp_13; tmp_14; __retres
-[inout] Inputs for function main6:
- s5; s6; cc; s3; s4; s7; s8; "toto"[bits 0 to 7]
diff --git a/tests/value/oracle/strings.2.res.oracle b/tests/value/oracle/strings.2.res.oracle
deleted file mode 100644
index daea0f31e7890e94748290ff519bbb703421d0d5..0000000000000000000000000000000000000000
--- a/tests/value/oracle/strings.2.res.oracle
+++ /dev/null
@@ -1,69 +0,0 @@
-[kernel] Parsing tests/value/strings.i (no preprocessing)
-[eva] Analyzing a complete application starting at main7
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- 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] ∈ {0}
- s2[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- s5 ∈ {0}
- s6 ∈ {0}
- cc ∈ {97}
- Q ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0}
- U ∈ {0}
- V ∈ {0}
- W ∈ {0}
- X ∈ {0}
- Y ∈ {0}
- Z ∈ {0}
- s3 ∈ {{ "tutu" }}
- s4 ∈ {{ "tutu" }}
- s7 ∈ {{ "hello\000 world" }}
- s8 ∈ {{ "hello" }}
-[eva:alarm] tests/value/strings.i:101: Warning:
- out of bounds write. assert \valid(tmp);
- (tmp from f?s5 + 2:& c)
-[eva:alarm] tests/value/strings.i:103: Warning:
- out of bounds write. assert \valid(s5);
-[eva:alarm] tests/value/strings.i:105: Warning:
- out of bounds write. assert \valid(s6);
-[eva] Recording results for main7
-[eva] done for function main7
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main7:
- s5 ∈ {{ &c }}
- s6 ∈ {{ &c }}
- R ∈ {84}
- c ∈ {116}
- __retres ∈ {116}
-[from] Computing for function main7
-[from] Done for function main7
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function main7:
- s5 FROM s3; d
- s6 FROM s3; e
- R FROM s3; d; f
- \result FROM s4; "tutu"[bits 0 to 7]
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main7:
- s5; s6; R; c; tmp; __retres
-[inout] Inputs for function main7:
- s5; s6; cc; s3; s4; "tutu"[bits 0 to 7]
diff --git a/tests/value/oracle/strings.3.res.oracle b/tests/value/oracle/strings.3.res.oracle
deleted file mode 100644
index 45b2847cf8c3a1cad1f6fa02a39b71c5a17765df..0000000000000000000000000000000000000000
--- a/tests/value/oracle/strings.3.res.oracle
+++ /dev/null
@@ -1,114 +0,0 @@
-[kernel] Parsing tests/value/strings.i (no preprocessing)
-[eva] Analyzing a complete application starting at main8
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- 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] ∈ {0}
- s2[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- s5 ∈ {0}
- s6 ∈ {0}
- cc ∈ {97}
- Q ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0}
- U ∈ {0}
- V ∈ {0}
- W ∈ {0}
- X ∈ {0}
- Y ∈ {0}
- Z ∈ {0}
- s3 ∈ {{ "tutu" }}
- s4 ∈ {{ "tutu" }}
- s7 ∈ {{ "hello\000 world" }}
- s8 ∈ {{ "hello" }}
-[eva] computing for function assigns <- main8.
- Called from tests/value/strings.i:127.
-[eva] using specification for function assigns
-[eva] tests/value/strings.i:121: Warning:
- no \from part for clause 'assigns *(p + (0 .. s - 1));'
-[eva] Done for function assigns
-[eva] computing for function strcmp <- main8.
- Called from tests/value/strings.i:128.
-[eva:alarm] tests/value/strings.i:114: Warning:
- out of bounds read. assert \valid_read(tmp_0);
- (tmp_0 from s2_0++)
-[eva] Recording results for strcmp
-[eva] Done for function strcmp
-[eva] Recording results for main8
-[eva] done for function main8
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function strcmp:
- s1_0 ∈ {{ &long_chain + [0..29] }}
- s2_0 ∈ {{ &tc + [0..29] }}
- __retres ∈ [-223..121]
-[eva:final-states] Values at end of function main8:
- tc[0..29] ∈ [--..--]
- long_chain[0] ∈ {114}
- [1] ∈ {101}
- [2] ∈ {97}
- [3..4] ∈ {108}
- [5] ∈ {121}
- [6] ∈ {32}
- [7] ∈ {114}
- [8] ∈ {101}
- [9] ∈ {97}
- [10..11] ∈ {108}
- [12] ∈ {121}
- [13] ∈ {32}
- [14] ∈ {114}
- [15] ∈ {101}
- [16] ∈ {97}
- [17..18] ∈ {108}
- [19] ∈ {121}
- [20] ∈ {32}
- [21] ∈ {108}
- [22] ∈ {111}
- [23] ∈ {110}
- [24] ∈ {103}
- [25] ∈ {32}
- [26] ∈ {99}
- [27] ∈ {104}
- [28] ∈ {97}
- [29] ∈ {105}
- [30] ∈ {110}
- [31] ∈ {0}
- x ∈ [-223..121]
-[from] Computing for function strcmp
-[from] Done for function strcmp
-[from] Computing for function main8
-[from] Computing for function assigns <-main8
-[from] Done for function assigns
-[from] Done for function main8
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function assigns:
- tc[0..29] FROM ANYTHING(origin:Unknown) (and SELF)
-[from] Function strcmp:
- \result FROM s1_0; s2_0; tc[0..29]; long_chain[0..30]
-[from] Function main8:
- \result FROM ANYTHING(origin:Unknown)
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function strcmp:
- s1_0; s2_0; tmp; tmp_0; __retres
-[inout] Inputs for function strcmp:
- tc[0..29]; long_chain[0..30]
-[inout] Out (internal) for function main8:
- tc[0..29]; long_chain[0..31]; x
-[inout] Inputs for function main8:
- ANYTHING(origin:Unknown)
diff --git a/tests/value/oracle/strings.res.oracle b/tests/value/oracle/strings.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5e410a5aad929dc5580b43a5d42f68a94d87a59f
--- /dev/null
+++ b/tests/value/oracle/strings.res.oracle
@@ -0,0 +1,428 @@
+[kernel] Parsing tests/value/strings.i (no 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 ∈ [--..--]
+ 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] ∈ {0}
+ s2[0] ∈ {104}
+ [1] ∈ {101}
+ [2..3] ∈ {108}
+ [4] ∈ {111}
+ [5] ∈ {0}
+ s3 ∈ {{ "tutu" }}
+ s4 ∈ {{ "tutu" }}
+ s5 ∈ {0}
+ s6 ∈ {0}
+ s7 ∈ {{ "hello\000 world" }}
+ s8 ∈ {{ "hello" }}
+ cc ∈ {97}
+ Q ∈ {0}
+ R ∈ {0}
+ S ∈ {0}
+ T ∈ {0}
+ U ∈ {0}
+ V ∈ {0}
+ W ∈ {0}
+ X ∈ {0}
+ Y ∈ {0}
+ Z ∈ {0}
+[eva] computing for function string_reads <- main.
+ Called from tests/value/strings.i:142.
+[eva] computing for function u <- string_reads <- main.
+ Called from tests/value/strings.i:39.
+[kernel:annot:missing-spec] tests/value/strings.i:39: Warning:
+ Neither code nor specification for function u, generating default assigns from the prototype
+[eva] using specification for function u
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:39: Warning:
+ out of bounds read. assert \valid_read(p - 4);
+[eva] computing for function u <- string_reads <- main.
+ Called from tests/value/strings.i:42.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:42: Warning:
+ out of bounds read. assert \valid_read(p + 12);
+[eva] computing for function u <- string_reads <- main.
+ Called from tests/value/strings.i:44.
+[eva] Done for function u
+[eva] computing for function u <- string_reads <- main.
+ Called from tests/value/strings.i:48.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:48: Warning:
+ out of bounds read. assert \valid_read(p - 4);
+[eva] computing for function u <- string_reads <- main.
+ Called from tests/value/strings.i:53.
+[eva] Done for function u
+[eva] computing for function strcpy <- string_reads <- main.
+ Called from tests/value/strings.i:53.
+[eva:alarm] tests/value/strings.i:23: Warning:
+ out of bounds write.
+ assert \valid(tmp_unroll_46);
+ (tmp_unroll_46 from ldst++)
+[kernel] tests/value/strings.i:23: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva] Recording results for strcpy
+[eva] Done for function strcpy
+[eva] computing for function strlen <- string_reads <- main.
+ Called from tests/value/strings.i:58.
+[eva] Recording results for strlen
+[eva] Done for function strlen
+[eva] Recording results for string_reads
+[eva] Done for function string_reads
+[eva] computing for function string_writes <- main.
+ Called from tests/value/strings.i:143.
+[eva:alarm] tests/value/strings.i:64: Warning:
+ out of bounds write. assert \valid(tmp);
+ (tmp from nondet?s5 + 2:& c)
+[eva:alarm] tests/value/strings.i:66: Warning:
+ out of bounds write. assert \valid(s5);
+[eva:alarm] tests/value/strings.i:68: Warning:
+ out of bounds write. assert \valid(s6);
+[eva] Recording results for string_writes
+[eva] Done for function string_writes
+[eva:locals-escaping] tests/value/strings.i:143: Warning:
+ locals {c} escaping the scope of string_writes through s5
+[eva:locals-escaping] tests/value/strings.i:143: Warning:
+ locals {c} escaping the scope of string_writes through s6
+[eva] computing for function string_comparison <- main.
+ Called from tests/value/strings.i:144.
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:78.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:79: Warning:
+ pointer comparison. assert \pointer_comparable((void *)s3, (void *)s4);
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:80.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:82.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:84.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:85: Warning:
+ pointer comparison. assert \pointer_comparable((void *)s7, (void *)s8);
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:86.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:88.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:89: Warning:
+ pointer comparison.
+ assert \pointer_comparable((void *)(s7 + 1), (void *)(s8 + 1));
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:90.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:92.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:93.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:94.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:95.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:95.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:96.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:97: Warning:
+ pointer comparison. assert \pointer_comparable((void *)s5, (void *)s6);
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:98.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:99: Warning:
+ pointer comparison.
+ assert \pointer_comparable((void *)("oh, hello" + 4), (void *)s7);
+[eva] Recording results for string_comparison
+[eva] Done for function string_comparison
+[eva] computing for function wide_string_comparison <- main.
+ Called from tests/value/strings.i:145.
+[eva:alarm] tests/value/strings.i:111: Warning:
+ pointer comparison. assert \pointer_comparable((void *)w1, (void *)w2);
+[eva:alarm] tests/value/strings.i:114: Warning:
+ pointer comparison. assert \pointer_comparable((void *)w2, (void *)w3);
+[eva] Recording results for wide_string_comparison
+[eva] Done for function wide_string_comparison
+[eva] computing for function long_chain <- main.
+ Called from tests/value/strings.i:146.
+[eva] computing for function assigns <- long_chain <- main.
+ Called from tests/value/strings.i:135.
+[eva] using specification for function assigns
+[eva] tests/value/strings.i:129: Warning:
+ no \from part for clause 'assigns *(p + (0 .. s - 1));'
+[eva] Done for function assigns
+[eva] computing for function strcmp <- long_chain <- main.
+ Called from tests/value/strings.i:136.
+[eva:alarm] tests/value/strings.i:123: Warning:
+ out of bounds read. assert \valid_read(tmp_0);
+ (tmp_0 from s2_0++)
+[eva] Recording results for strcmp
+[eva] Done for function strcmp
+[eva] Recording results for long_chain
+[eva] Done for function long_chain
+[eva] Recording results for main
+[eva] done for function main
+[eva] tests/value/strings.i:23:
+ assertion 'Eva,mem_access' got final status invalid.
+[eva] tests/value/strings.i:39:
+ assertion 'Eva,mem_access' got final status invalid.
+[eva] tests/value/strings.i:42:
+ assertion 'Eva,mem_access' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function strcmp:
+ s1_0 ∈ {{ &long_chain_0 + [0..29] }}
+ s2_0 ∈ {{ &tc + [0..29] }}
+ __retres ∈ [-223..121]
+[eva:final-states] Values at end of function long_chain:
+ tc[0..29] ∈ [--..--]
+ long_chain_0[0] ∈ {114}
+ [1] ∈ {101}
+ [2] ∈ {97}
+ [3..4] ∈ {108}
+ [5] ∈ {121}
+ [6] ∈ {32}
+ [7] ∈ {114}
+ [8] ∈ {101}
+ [9] ∈ {97}
+ [10..11] ∈ {108}
+ [12] ∈ {121}
+ [13] ∈ {32}
+ [14] ∈ {114}
+ [15] ∈ {101}
+ [16] ∈ {97}
+ [17..18] ∈ {108}
+ [19] ∈ {121}
+ [20] ∈ {32}
+ [21] ∈ {108}
+ [22] ∈ {111}
+ [23] ∈ {110}
+ [24] ∈ {103}
+ [25] ∈ {32}
+ [26] ∈ {99}
+ [27] ∈ {104}
+ [28] ∈ {97}
+ [29] ∈ {105}
+ [30] ∈ {110}
+ [31] ∈ {0}
+ x ∈ [-223..121]
+[eva:final-states] Values at end of function strcpy:
+ NON TERMINATING FUNCTION
+[eva:final-states] Values at end of function string_writes:
+ s5 ∈ {{ &c }}
+ s6 ∈ {{ &c }}
+ R ∈ {84}
+ c ∈ {116}
+ __retres ∈ {116}
+[eva:final-states] Values at end of function strlen:
+ s ∈ {{ &s1[6] }}
+ l ∈ {5}
+[eva:final-states] Values at end of function string_comparison:
+ s5 ∈ {{ "tutu" ; "hello" }}
+ s6 ∈ {{ "tutu" ; "tutu" ; "hello" }}
+ cc ∈ {116}
+ Q ∈ {0}
+ R ∈ {0; 84}
+ S ∈ {0}
+ T ∈ {0; 101}
+ U ∈ {0}
+ V ∈ {0}
+ W ∈ {0}
+ X ∈ {0; 1}
+ Y ∈ {0; 1}
+ Z ∈ {0; 1}
+ s ∈ {{ "toto" }}
+ __retres ∈ {116}
+[eva:final-states] Values at end of function string_reads:
+ s1[0] ∈ {104}
+ [1] ∈ {101}
+ [2] ∈ {108}
+ [3] ∈ {97}
+ [4] ∈ {111}
+ [5] ∈ {0}
+ [6] ∈ {97}
+ [7] ∈ {119}
+ [8] ∈ {111}
+ [9] ∈ {114}
+ [10] ∈ {108}
+ [11] ∈ {100}
+ [12] ∈ {0}
+ R ∈ {0}
+ S ∈ {0}
+ T ∈ {0; 101}
+ p ∈ {{ &s1[5] ; &s2[3] }}
+ __retres ∈ {5}
+[eva:final-states] Values at end of function wide_string_comparison:
+ w1 ∈ {{ L"abcdef" }}
+ w2 ∈ {{ L"def" }}
+ w3 ∈ {{ L"abc" }}
+ res ∈ {0}
+[eva:final-states] Values at end of function main:
+ s1[0] ∈ {104}
+ [1] ∈ {101}
+ [2] ∈ {108}
+ [3] ∈ {97}
+ [4] ∈ {111}
+ [5] ∈ {0}
+ [6] ∈ {97}
+ [7] ∈ {119}
+ [8] ∈ {111}
+ [9] ∈ {114}
+ [10] ∈ {108}
+ [11] ∈ {100}
+ [12] ∈ {0}
+ s5 ∈ {{ "tutu" ; "hello" }}
+ s6 ∈ {{ "tutu" ; "tutu" ; "hello" }}
+ cc ∈ {116}
+ Q ∈ {0}
+ R ∈ {0; 84}
+ S ∈ {0}
+ T ∈ {0; 101}
+ U ∈ {0}
+ V ∈ {0}
+ W ∈ {0}
+ X ∈ {0; 1}
+ Y ∈ {0; 1}
+ Z ∈ {0; 1}
+[from] Computing for function strcmp
+[from] Done for function strcmp
+[from] Computing for function long_chain
+[from] Computing for function assigns <-long_chain
+[from] Done for function assigns
+[from] Done for function long_chain
+[from] Computing for function strcpy
+[from] Non-terminating function strcpy (no dependencies)
+[from] Done for function strcpy
+[from] Computing for function string_writes
+[from] Done for function string_writes
+[from] Computing for function strlen
+[from] Done for function strlen
+[from] Computing for function string_comparison
+[from] Computing for function u <-string_comparison
+[from] Done for function u
+[from] Done for function string_comparison
+[from] Computing for function string_reads
+[from] Done for function string_reads
+[from] Computing for function wide_string_comparison
+[from] Done for function wide_string_comparison
+[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 assigns:
+ tc[0..29] FROM ANYTHING(origin:Unknown) (and SELF)
+[from] Function strcmp:
+ \result FROM s1_0; s2_0; tc[0..29]; long_chain_0[0..30]
+[from] Function long_chain:
+ \result FROM ANYTHING(origin:Unknown)
+[from] Function strcpy:
+ NON TERMINATING - NO EFFECTS
+[from] Function string_writes:
+ s5 FROM nondet; s3
+ s6 FROM nondet; s3
+ R FROM nondet; s3
+ \result FROM s4; "tutu"[bits 0 to 7]
+[from] Function strlen:
+ \result FROM s1[0..4]; s
+[from] Function u:
+ \result FROM \nothing
+[from] Function string_comparison:
+ s5 FROM s3; s8
+ s6 FROM s3; s4; s8
+ cc FROM "toto"[bits 0 to 7]
+ Q FROM s7 (and SELF)
+ R FROM s3; s4 (and SELF)
+ S FROM \nothing (and SELF)
+ T FROM s3 (and SELF)
+ U FROM s7; s8 (and SELF)
+ V FROM s4; s7 (and SELF)
+ W FROM s7; s8 (and SELF)
+ X FROM s3 (and SELF)
+ Y FROM s3; s8 (and SELF)
+ Z FROM s3; s4; s8 (and SELF)
+ \result FROM "toto"[bits 0 to 7]
+[from] Function string_reads:
+ s1{[3]; [6]} FROM cc
+ R FROM \nothing (and SELF)
+ S FROM \nothing (and SELF)
+ T FROM s1[1] (and SELF)
+ \result FROM s1{[0..2]; [4]}; cc
+[from] Function wide_string_comparison:
+ \result FROM \nothing
+[from] Function main:
+ s1{[3]; [6]} FROM cc
+ s5 FROM s3; s8
+ s6 FROM s3; s4; s8
+ cc FROM "toto"[bits 0 to 7]
+ Q FROM s7 (and SELF)
+ R FROM nondet; s3; s4
+ S FROM \nothing (and SELF)
+ T FROM s1[1]; s3 (and SELF)
+ U FROM s7; s8 (and SELF)
+ V FROM s4; s7 (and SELF)
+ W FROM s7; s8 (and SELF)
+ X FROM s3 (and SELF)
+ Y FROM s3; s8 (and SELF)
+ Z FROM s3; s4; s8 (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function strcmp:
+ s1_0; s2_0; tmp; tmp_0; __retres
+[inout] Inputs for function strcmp:
+ tc[0..29]; long_chain_0[0..30]
+[inout] Out (internal) for function long_chain:
+ tc[0..29]; long_chain_0[0..31]; x
+[inout] Inputs for function long_chain:
+ ANYTHING(origin:Unknown)
+[inout] Out (internal) for function strcpy:
+ src; ldst; b[0..4]; tmp_unroll_46; tmp_1_unroll_46; tmp_0_unroll_46;
+ tmp_unroll_49; tmp_1_unroll_49; tmp_0_unroll_49; tmp_unroll_52;
+ tmp_1_unroll_52; tmp_0_unroll_52; tmp_unroll_55; tmp_1_unroll_55;
+ tmp_0_unroll_55; tmp_unroll_58; tmp_1_unroll_58; tmp_0_unroll_58;
+ tmp_unroll_61; tmp_1_unroll_61; tmp_0_unroll_61
+[inout] Inputs for function strcpy:
+ a[0..5]
+[inout] Out (internal) for function string_writes:
+ s5; s6; R; c; tmp; __retres
+[inout] Inputs for function string_writes:
+ nondet; s3; s4; s5; s6; cc; "tutu"[bits 0 to 7]
+[inout] Out (internal) for function strlen:
+ s; l; tmp_unroll_106; tmp_unroll_109; tmp_unroll_112; tmp_unroll_115;
+ tmp_unroll_118; tmp_unroll_121
+[inout] Inputs for function strlen:
+ s1[0..5]
+[inout] Out (internal) for function string_comparison:
+ s5; s6; cc; Q; R; S; T; U; V; W; X; Y; Z; s; tmp; tmp_0; tmp_1; tmp_2;
+ tmp_3; tmp_4; tmp_5; tmp_6; tmp_7; tmp_8; tmp_9; tmp_10; tmp_11; tmp_12;
+ tmp_13; tmp_14; __retres
+[inout] Inputs for function string_comparison:
+ s3; s4; s5; s6; s7; s8; cc; "toto"[bits 0 to 7]
+[inout] Out (internal) for function string_reads:
+ s1{[3]; [6]}; R; S; T; p; tmp; tmp_0; tmp_1; tmp_2; a[0..9]; b[0..4];
+ tmp_3; tmp_4; __retres
+[inout] Inputs for function string_reads:
+ s1[0..5]; cc
+[inout] Out (internal) for function wide_string_comparison:
+ w1; w2; w3; res
+[inout] Inputs for function wide_string_comparison:
+ \nothing
+[inout] Out (internal) for function main:
+ s1{[3]; [6]}; s5; s6; cc; Q; R; S; T; U; V; W; X; Y; Z
+[inout] Inputs for function main:
+ ANYTHING(origin:Unknown)
diff --git a/tests/value/strings.i b/tests/value/strings.i
index f4ca9828f5bfd47f713c0fab8528a6a56cb64c6b..0f6087161602aca84fc72009a38b18e5ccb75272 100644
--- a/tests/value/strings.i
+++ b/tests/value/strings.i
@@ -1,21 +1,23 @@
/* run.config*
- GCC:
- STDOPT: #"-main main1 -eva-no-builtins-auto"
- STDOPT: #"-main main6 -eva-no-builtins-auto"
- STDOPT: #"-main main7 -eva-no-builtins-auto"
- STDOPT: #"-main main8 -slevel-function strcmp:50 -eva-no-builtins-auto"
+ STDOPT: #"-eva-no-builtins-auto -eva-slevel-function strcmp:50"
*/
+
+volatile int nondet;
+
char s1[]="hello\000 world";
char s2[]="hello";
+char *s3="tutu";
+char *s4="tutu";
char *s5, *s6;
+char *s7="hello\x00 world";
+char *s8="hello";
int u(void);
char cc = 'a';
char Q, R, S, T, U, V, W, X, Y, Z;
-char *strcpy(char*dst, char*src)
-{
+char *strcpy(char*dst, char*src) {
char* ldst=dst;
/*@ loop pragma UNROLL 20; */
while (*ldst++ = *src++)
@@ -23,8 +25,7 @@ char *strcpy(char*dst, char*src)
return dst;
}
-unsigned int strlen(char *s)
-{
+unsigned int strlen(char *s) {
unsigned int l=0;
/*@ loop pragma UNROLL 20; */
while(*s++ != 0)
@@ -32,8 +33,7 @@ unsigned int strlen(char *s)
return l;
}
-int main1(void)
-{
+int string_reads() {
char *p;
p = &s1[3];
if (u()) R=*(p-4);
@@ -48,24 +48,30 @@ int main1(void)
if (u()) T=*(p-4);
{
- char a[10] = "Not ok";
- char b [5];
- if (u()) strcpy(b,a);
- }
-
+ char a[10] = "Not ok";
+ char b [5];
+ if (u()) strcpy(b,a);
+ }
+
s1[3]=cc;
s1[6]=cc;
return strlen(s1);
}
+int string_writes() {
+ char c=-1;
+ if (nondet) s5 = s3; else s5 = &c;
+ *(nondet ? s5 + 2 : &c) = 'T';
+ R=c;
+ *s5=' ';
+ if (nondet) s6 = s3+1; else s6 = &c;
+ *s6=cc;
+ c=*s4;
+ return c;
+}
-char *s3="tutu";
-char *s4="tutu";
-char *s7="hello\x00 world";
-char *s8="hello";
-int main6(void)
-{
+int string_comparison() {
char *s;
s = "toto";
cc = *s;
@@ -82,29 +88,32 @@ int main6(void)
if (u())
W = (s7 + 1 == s8 + 1);
if (u())
- X = (s3 == s3);
- s5 = (u()?s3:s8);
+ X = (s3 == s3);
+ s5 = (u()?s3:s8);
if (u())
Y = ((u()?s3:s8) == s5);
- s6 = (u()?(u()?s3:s8):s4);
+ s6 = (u()?(u()?s3:s8):s4);
if (u())
Z = (s5 == s6);
if (u())
- Q = ("oh, hello"+4 == s7);
+ Q = ("oh, hello"+4 == s7);
return cc;
}
-int main7(int d, int e, int f)
-{
- char c=-1;
- if (d) s5 = s3; else s5 = &c;
- *(f ? s5 + 2 : &c) = 'T';
- R=c;
- *s5=' ';
- if (e) s6 = s3+1; else s6 = &c;
- *s6=cc;
- c=*s4;
- return c;
+/* Currently, Eva does not support wide string comparisons: alarms are emitted
+ on any comparison involving a wide string. Tests are minimal for now. */
+int wide_string_comparison() {
+ char* w1 = L"abcdef";
+ char* w2 = L"def";
+ char* w3 = L"abc";
+ int res = 0;
+ /* Must emit a comparison alarm. */
+ if (w1 == w2)
+ res = 1;
+ /* Ideally, should not emit a comparison alarm. */
+ if (w2 == w3)
+ res = -1;
+ return res;
}
int strcmp(const char *s1, const char *s2)
@@ -117,14 +126,22 @@ int strcmp(const char *s1, const char *s2)
return (*(unsigned char *)s1 - *(unsigned char *)--s2);
}
-
//@ assigns p[0..s-1]; ensures \initialized(&p[0..s-1]);
void assigns(char *p, unsigned int s);
-int main8() {
+int long_chain() {
char tc[30];
char long_chain[] = "really really really long chain";
assigns(&tc[0],30);
int x = strcmp(long_chain, tc);
return x;
}
+
+
+void main() {
+ string_reads ();
+ string_writes ();
+ string_comparison ();
+ wide_string_comparison ();
+ long_chain ();
+}