[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/libc/string_c.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
  __fc_random_counter ∈ {0}
  __fc_rand_max ∈ {32767}
  __fc_heap_status ∈ [--..--]
[value] computing for function test_memcpy <- main.
        Called from tests/libc/string_c.c:262.
tests/libc/string_c.c:10:[value] Call to builtin memcpy(({{ (void *)&dest }},{{ (void const *)&src }},{6}))
tests/libc/string_c.c:11:[value] assertion got status valid.
tests/libc/string_c.c:12:[value] assertion got status valid.
tests/libc/string_c.c:13:[value] assertion got status valid.
tests/libc/string_c.c:14:[value] assertion got status valid.
tests/libc/string_c.c:16:[value] Call to builtin memcpy(({{ (void *)&dest }},{{ (void const *)&src2 }},{5}))
tests/libc/string_c.c:17:[value] assertion got status valid.
tests/libc/string_c.c:18:[value] assertion got status valid.
tests/libc/string_c.c:19:[value] Call to builtin memcpy(({{ (void *)&dest }},{0},{0}))
tests/libc/string_c.c:20:[value] Call to builtin memcpy(({0},{0},{0}))
tests/libc/string_c.c:21:[value] assertion got status valid.
tests/libc/string_c.c:23:[value] Call to builtin memcpy(({{ (void *)&dest }},{0},{0}))
tests/libc/string_c.c:24:[value] Call to builtin memcpy(({0},{0},{0}))
tests/libc/string_c.c:25:[value] assertion got status valid.
tests/libc/string_c.c:26:[value] Call to builtin memcpy(({{ (void *)&dest }},{{ (void const *)&x }},{4}))
tests/libc/string_c.c:27:[value] assertion got status valid.
tests/libc/string_c.c:28:[value] assertion got status valid.
[value] Recording results for test_memcpy
[value] Done for function test_memcpy
[value] computing for function test_memmove <- main.
        Called from tests/libc/string_c.c:263.
[value] Called Frama_C_show_each_s0({1})
[value] Called Frama_C_show_each_s0({2})
[value] Called Frama_C_show_each_s0({3})
[value] Called Frama_C_show_each_s0({4})
[value] Called Frama_C_show_each_s0({3})
[value] Called Frama_C_show_each_s0({4})
[value] Called Frama_C_show_each_s0({5})
[value] Called Frama_C_show_each_s0({6})
[value] computing for function memmove <- test_memmove <- main.
        Called from tests/libc/string_c.c:45.
share/libc/string.h:70:[value] function memmove: precondition 'valid_dst' got status valid.
share/libc/string.h:71:[value] function memmove: precondition 'valid_src' got status valid.
[value] computing for function memoverlap <- memmove <- test_memmove <- main.
        Called from share/libc/string.c:61.
[value] using specification for function memoverlap
[value] Done for function memoverlap
share/libc/string.c:61:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:74:[value] warning: function memmove: postcondition got status unknown.
share/libc/string.h:75:[value] function memmove: postcondition got status valid.
[value] Recording results for memmove
[value] Done for function memmove
tests/libc/string_c.c:46:[value] assertion got status valid.
tests/libc/string_c.c:47:[value] assertion got status valid.
[value] computing for function memmove <- test_memmove <- main.
        Called from tests/libc/string_c.c:52.
[value] computing for function memoverlap <- memmove <- test_memmove <- main.
        Called from share/libc/string.c:61.
[value] Done for function memoverlap
share/libc/string.c:62:[value] Call to builtin memcpy(({{ (void *)&buf }},{{ (void const *)&buf[2] }},{4}))
[value] Recording results for memmove
[value] Done for function memmove
tests/libc/string_c.c:53:[value] assertion got status valid.
[value] computing for function memmove <- test_memmove <- main.
        Called from tests/libc/string_c.c:55.
[value] computing for function memoverlap <- memmove <- test_memmove <- main.
        Called from share/libc/string.c:61.
[value] Done for function memoverlap
share/libc/string.c:62:[value] Call to builtin memcpy(({{ (void *)&buf }},{{ (void const *)&buf }},{4}))
[value] Recording results for memmove
[value] Done for function memmove
tests/libc/string_c.c:56:[value] assertion got status valid.
[value] Recording results for test_memmove
[value] Done for function test_memmove
[value] computing for function test_strlen <- main.
        Called from tests/libc/string_c.c:264.
[value] computing for function strlen <- test_strlen <- main.
        Called from tests/libc/string_c.c:62.
share/libc/string.h:91:[value] function strlen: precondition 'valid_string_src' got status valid.
share/libc/string.c:78:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:93:[value] warning: function strlen: postcondition got status unknown.
[value] Recording results for strlen
[value] Done for function strlen
tests/libc/string_c.c:63:[value] assertion got status valid.
[value] computing for function strlen <- test_strlen <- main.
        Called from tests/libc/string_c.c:64.
[value] Recording results for strlen
[value] Done for function strlen
tests/libc/string_c.c:65:[value] assertion got status valid.
[value] computing for function strlen <- test_strlen <- main.
        Called from tests/libc/string_c.c:66.
[value] Recording results for strlen
[value] Done for function strlen
tests/libc/string_c.c:67:[value] assertion got status valid.
[value] Recording results for test_strlen
[value] Done for function test_strlen
[value] computing for function test_memset <- main.
        Called from tests/libc/string_c.c:265.
[value] computing for function memset <- test_memset <- main.
        Called from tests/libc/string_c.c:73.
share/libc/string.h:81:[value] function memset: precondition got status valid.
share/libc/string.c:87:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:84:[value] warning: function memset: postcondition got status unknown.
share/libc/string.h:85:[value] function memset: postcondition got status valid.
[value] Recording results for memset
[value] Done for function memset
tests/libc/string_c.c:74:[value] assertion got status valid.
tests/libc/string_c.c:75:[value] assertion got status valid.
tests/libc/string_c.c:76:[value] assertion got status valid.
[value] computing for function memset <- test_memset <- main.
        Called from tests/libc/string_c.c:77.
[value] Recording results for memset
[value] Done for function memset
tests/libc/string_c.c:78:[value] assertion got status valid.
[value] Recording results for test_memset
[value] Done for function test_memset
[value] computing for function test_strcmp <- main.
        Called from tests/libc/string_c.c:266.
[value] computing for function strcmp <- test_strcmp <- main.
        Called from tests/libc/string_c.c:85.
share/libc/string.h:103:[value] function strcmp: precondition 'valid_string_s1' got status valid.
share/libc/string.h:104:[value] function strcmp: precondition 'valid_string_s2' got status valid.
share/libc/string.c:96:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:106:[value] warning: function strcmp: postcondition got status unknown.
[value] Recording results for strcmp
[value] Done for function strcmp
tests/libc/string_c.c:86:[value] assertion got status valid.
[value] computing for function strcmp <- test_strcmp <- main.
        Called from tests/libc/string_c.c:87.
[value] Recording results for strcmp
[value] Done for function strcmp
tests/libc/string_c.c:88:[value] assertion got status valid.
[value] computing for function strcmp <- test_strcmp <- main.
        Called from tests/libc/string_c.c:89.
[value] Recording results for strcmp
[value] Done for function strcmp
tests/libc/string_c.c:90:[value] assertion got status valid.
[value] computing for function strcmp <- test_strcmp <- main.
        Called from tests/libc/string_c.c:91.
[value] Recording results for strcmp
[value] Done for function strcmp
tests/libc/string_c.c:92:[value] assertion got status valid.
[value] computing for function strcmp <- test_strcmp <- main.
        Called from tests/libc/string_c.c:93.
[value] Recording results for strcmp
[value] Done for function strcmp
tests/libc/string_c.c:94:[value] assertion got status valid.
[value] computing for function strcmp <- test_strcmp <- main.
        Called from tests/libc/string_c.c:95.
[value] Recording results for strcmp
[value] Done for function strcmp
tests/libc/string_c.c:96:[value] assertion got status valid.
[value] computing for function strcmp <- test_strcmp <- main.
        Called from tests/libc/string_c.c:97.
[value] Recording results for strcmp
[value] Done for function strcmp
tests/libc/string_c.c:98:[value] assertion got status valid.
[value] Recording results for test_strcmp
[value] Done for function test_strcmp
[value] computing for function test_strncmp <- main.
        Called from tests/libc/string_c.c:267.
[value] computing for function strncmp <- test_strncmp <- main.
        Called from tests/libc/string_c.c:148.
share/libc/string.h:110:[value] function strncmp: precondition 'valid_string_s1' got status valid.
share/libc/string.h:111:[value] function strncmp: precondition 'valid_string_s2' got status valid.
share/libc/string.c:107:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:113:[value] warning: function strncmp: postcondition got status unknown.
[value] Recording results for strncmp
[value] Done for function strncmp
tests/libc/string_c.c:149:[value] assertion got status valid.
[value] computing for function strncmp <- test_strncmp <- main.
        Called from tests/libc/string_c.c:150.
[value] Recording results for strncmp
[value] Done for function strncmp
tests/libc/string_c.c:151:[value] assertion got status valid.
[value] computing for function strncmp <- test_strncmp <- main.
        Called from tests/libc/string_c.c:153.
[value] Recording results for strncmp
[value] Done for function strncmp
tests/libc/string_c.c:154:[value] assertion got status valid.
[value] computing for function strncmp <- test_strncmp <- main.
        Called from tests/libc/string_c.c:155.
[value] Recording results for strncmp
[value] Done for function strncmp
tests/libc/string_c.c:156:[value] assertion got status valid.
[value] computing for function strncmp <- test_strncmp <- main.
        Called from tests/libc/string_c.c:157.
[value] Recording results for strncmp
[value] Done for function strncmp
tests/libc/string_c.c:158:[value] assertion got status valid.
[value] computing for function strncmp <- test_strncmp <- main.
        Called from tests/libc/string_c.c:159.
[value] Recording results for strncmp
[value] Done for function strncmp
tests/libc/string_c.c:160:[value] assertion got status valid.
[value] computing for function strncmp <- test_strncmp <- main.
        Called from tests/libc/string_c.c:161.
[value] Recording results for strncmp
[value] Done for function strncmp
tests/libc/string_c.c:162:[value] assertion got status valid.
[value] computing for function strncmp <- test_strncmp <- main.
        Called from tests/libc/string_c.c:163.
[value] Recording results for strncmp
[value] Done for function strncmp
tests/libc/string_c.c:164:[value] assertion got status valid.
[value] Recording results for test_strncmp
[value] Done for function test_strncmp
[value] computing for function test_memcmp <- main.
        Called from tests/libc/string_c.c:268.
[value] computing for function memcmp <- test_memcmp <- main.
        Called from tests/libc/string_c.c:169.
share/libc/string.h:35:[value] function memcmp: precondition got status valid.
share/libc/string.h:36:[value] function memcmp: precondition got status valid.
share/libc/string.c:117:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:38:[value] warning: function memcmp: postcondition got status unknown.
[value] Recording results for memcmp
[value] Done for function memcmp
tests/libc/string_c.c:170:[value] assertion got status valid.
[value] computing for function memcmp <- test_memcmp <- main.
        Called from tests/libc/string_c.c:171.
[value] Recording results for memcmp
[value] Done for function memcmp
tests/libc/string_c.c:172:[value] assertion got status valid.
[value] computing for function memcmp <- test_memcmp <- main.
        Called from tests/libc/string_c.c:173.
[value] Recording results for memcmp
[value] Done for function memcmp
tests/libc/string_c.c:174:[value] assertion got status valid.
[value] computing for function memcmp <- test_memcmp <- main.
        Called from tests/libc/string_c.c:175.
[value] Recording results for memcmp
[value] Done for function memcmp
tests/libc/string_c.c:176:[value] assertion got status valid.
[value] Recording results for test_memcmp
[value] Done for function test_memcmp
[value] computing for function test_strcat <- main.
        Called from tests/libc/string_c.c:269.
[value] computing for function strcat <- test_strcat <- main.
        Called from tests/libc/string_c.c:105.
share/libc/string.h:249:[value] function strcat: precondition 'valid_string_src' got status valid.
share/libc/string.h:250:[value] function strcat: precondition 'valid_string_dst' got status valid.
tests/libc/string_c.c:105:[value] Cannot evaluate range bound strlen(dest) + strlen(src)
        (unsupported ACSL construct: logic functions or predicates). Approximating
share/libc/string.h:251:[value] warning: function strcat: precondition 'room_string' got status unknown.
[value] computing for function strlen <- strcat <- test_strcat <- main.
        Called from share/libc/string.c:145.
[value] Recording results for strlen
[value] Done for function strlen
share/libc/string.c:150:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:254:[value] warning: function strcat: postcondition got status unknown.
share/libc/string.h:256:[value] function strcat: postcondition got status valid.
[value] Recording results for strcat
[value] Done for function strcat
tests/libc/string_c.c:106:[value] assertion got status valid.
tests/libc/string_c.c:107:[value] assertion got status valid.
[value] computing for function strcat <- test_strcat <- main.
        Called from tests/libc/string_c.c:113.
tests/libc/string_c.c:113:[value] Cannot evaluate range bound strlen(dest) + strlen(src)
        (unsupported ACSL construct: logic functions or predicates). Approximating
[value] computing for function strlen <- strcat <- test_strcat <- main.
        Called from share/libc/string.c:145.
[value] Recording results for strlen
[value] Done for function strlen
[value] Recording results for strcat
[value] Done for function strcat
tests/libc/string_c.c:114:[value] assertion got status valid.
[value] computing for function strcat <- test_strcat <- main.
        Called from tests/libc/string_c.c:115.
tests/libc/string_c.c:115:[value] Cannot evaluate range bound strlen(dest) + strlen(src)
        (unsupported ACSL construct: logic functions or predicates). Approximating
[value] computing for function strlen <- strcat <- test_strcat <- main.
        Called from share/libc/string.c:145.
[value] Recording results for strlen
[value] Done for function strlen
[value] Recording results for strcat
[value] Done for function strcat
[value] computing for function strcat <- test_strcat <- main.
        Called from tests/libc/string_c.c:116.
tests/libc/string_c.c:116:[value] Cannot evaluate range bound strlen(dest) + strlen(src)
        (unsupported ACSL construct: logic functions or predicates). Approximating
[value] computing for function strlen <- strcat <- test_strcat <- main.
        Called from share/libc/string.c:145.
[value] Recording results for strlen
[value] Done for function strlen
[value] Recording results for strcat
[value] Done for function strcat
tests/libc/string_c.c:117:[value] assertion got status valid.
[value] Recording results for test_strcat
[value] Done for function test_strcat
[value] computing for function test_strcpy <- main.
        Called from tests/libc/string_c.c:271.
[value] computing for function strcpy <- test_strcpy <- main.
        Called from tests/libc/string_c.c:123.
share/libc/string.h:208:[value] function strcpy: precondition 'valid_string_src' got status valid.
tests/libc/string_c.c:123:[value] Cannot evaluate range bound strlen(src)
        (unsupported ACSL construct: logic functions or predicates). Approximating
share/libc/string.h:209:[value] warning: function strcpy: precondition 'room_string' got status unknown.
share/libc/string.c:173:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:212:[value] warning: function strcpy: postcondition got status unknown.
share/libc/string.h:213:[value] function strcpy: postcondition got status valid.
[value] Recording results for strcpy
[value] Done for function strcpy
tests/libc/string_c.c:124:[value] assertion got status valid.
tests/libc/string_c.c:125:[value] assertion got status valid.
[value] computing for function strcpy <- test_strcpy <- main.
        Called from tests/libc/string_c.c:126.
tests/libc/string_c.c:126:[value] Cannot evaluate range bound strlen(src)
        (unsupported ACSL construct: logic functions or predicates). Approximating
[value] Recording results for strcpy
[value] Done for function strcpy
tests/libc/string_c.c:127:[value] assertion got status valid.
[value] computing for function strcpy <- test_strcpy <- main.
        Called from tests/libc/string_c.c:128.
tests/libc/string_c.c:128:[value] Cannot evaluate range bound strlen(src)
        (unsupported ACSL construct: logic functions or predicates). Approximating
[value] Recording results for strcpy
[value] Done for function strcpy
tests/libc/string_c.c:129:[value] assertion got status valid.
[value] Recording results for test_strcpy
[value] Done for function test_strcpy
[value] computing for function test_strncpy <- main.
        Called from tests/libc/string_c.c:272.
[value] computing for function strncpy <- test_strncpy <- main.
        Called from tests/libc/string_c.c:135.
share/libc/string.h:218:[value] function strncpy: precondition 'valid_string_src' got status valid.
share/libc/string.h:219:[value] function strncpy: precondition 'room_nstring' got status valid.
tests/libc/string_c.c:135:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:222:[value] function strncpy: postcondition got status valid.
share/libc/string.h:223:[value] function strncpy: postcondition got status valid.
share/libc/string.c:185:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:226:[value] warning: function strncpy, behavior complete: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:229:[value] warning: function strncpy, behavior partial: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
[value] Recording results for strncpy
[value] Done for function strncpy
tests/libc/string_c.c:136:[value] assertion got status valid.
tests/libc/string_c.c:137:[value] assertion got status valid.
[value] computing for function strncpy <- test_strncpy <- main.
        Called from tests/libc/string_c.c:138.
tests/libc/string_c.c:138:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] Recording results for strncpy
[value] Done for function strncpy
tests/libc/string_c.c:139:[value] assertion got status valid.
[value] computing for function strncpy <- test_strncpy <- main.
        Called from tests/libc/string_c.c:140.
tests/libc/string_c.c:140:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] Recording results for strncpy
[value] Done for function strncpy
tests/libc/string_c.c:141:[value] assertion got status valid.
[value] computing for function strncpy <- test_strncpy <- main.
        Called from tests/libc/string_c.c:142.
tests/libc/string_c.c:142:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] Recording results for strncpy
[value] Done for function strncpy
tests/libc/string_c.c:143:[value] assertion got status valid.
[value] Recording results for test_strncpy
[value] Done for function test_strncpy
[value] computing for function test_strchr <- main.
        Called from tests/libc/string_c.c:273.
[value] computing for function strchr <- test_strchr <- main.
        Called from tests/libc/string_c.c:182.
share/libc/string.h:123:[value] function strchr: precondition 'valid_string_src' got status valid.
tests/libc/string_c.c:182:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:127:[value] function strchr, behavior found: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:128:[value] function strchr, behavior found: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/libc/string.c:194:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:129:[value] warning: function strchr, behavior found: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:130:[value] function strchr, behavior found: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:131:[value] warning: function strchr, behavior found: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:134:[value] warning: function strchr, behavior not_found: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:136:[value] function strchr, behavior default: postcondition got status valid.
[value] Recording results for strchr
[value] Done for function strchr
tests/libc/string_c.c:183:[value] assertion got status valid.
[value] computing for function strchr <- test_strchr <- main.
        Called from tests/libc/string_c.c:184.
tests/libc/string_c.c:184:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:127:[value] warning: function strchr, behavior found: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:128:[value] warning: function strchr, behavior found: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:129:[value] warning: function strchr, behavior found: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:130:[value] warning: function strchr, behavior found: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:134:[value] function strchr, behavior not_found: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] Recording results for strchr
[value] Done for function strchr
tests/libc/string_c.c:185:[value] assertion got status valid.
[value] computing for function strchr <- test_strchr <- main.
        Called from tests/libc/string_c.c:186.
tests/libc/string_c.c:186:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] Recording results for strchr
[value] Done for function strchr
tests/libc/string_c.c:187:[value] assertion got status valid.
[value] computing for function strchr <- test_strchr <- main.
        Called from tests/libc/string_c.c:188.
tests/libc/string_c.c:188:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] Recording results for strchr
[value] Done for function strchr
tests/libc/string_c.c:189:[value] assertion got status valid.
[value] Recording results for test_strchr
[value] Done for function test_strchr
[value] computing for function test_strrchr <- main.
        Called from tests/libc/string_c.c:274.
[value] computing for function strrchr <- test_strrchr <- main.
        Called from tests/libc/string_c.c:195.
share/libc/string.h:140:[value] function strrchr: precondition 'valid_string_src' got status valid.
tests/libc/string_c.c:195:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] computing for function strlen <- strrchr <- test_strrchr <- main.
        Called from share/libc/string.c:200.
[value] Recording results for strlen
[value] Done for function strlen
share/libc/string.h:144:[value] function strrchr, behavior found: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:145:[value] function strrchr, behavior found: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:146:[value] function strrchr, behavior found: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:149:[value] warning: function strrchr, behavior not_found: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:151:[value] function strrchr, behavior default: postcondition got status valid.
[value] Recording results for strrchr
[value] Done for function strrchr
tests/libc/string_c.c:196:[value] assertion got status valid.
[value] computing for function strrchr <- test_strrchr <- main.
        Called from tests/libc/string_c.c:197.
tests/libc/string_c.c:197:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] computing for function strlen <- strrchr <- test_strrchr <- main.
        Called from share/libc/string.c:200.
[value] Recording results for strlen
[value] Done for function strlen
share/libc/string.h:144:[value] warning: function strrchr, behavior found: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:145:[value] warning: function strrchr, behavior found: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:146:[value] warning: function strrchr, behavior found: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:149:[value] function strrchr, behavior not_found: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] Recording results for strrchr
[value] Done for function strrchr
tests/libc/string_c.c:198:[value] assertion got status valid.
[value] computing for function strrchr <- test_strrchr <- main.
        Called from tests/libc/string_c.c:199.
tests/libc/string_c.c:199:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] computing for function strlen <- strrchr <- test_strrchr <- main.
        Called from share/libc/string.c:200.
[value] Recording results for strlen
[value] Done for function strlen
[value] Recording results for strrchr
[value] Done for function strrchr
tests/libc/string_c.c:200:[value] assertion got status valid.
[value] computing for function strrchr <- test_strrchr <- main.
        Called from tests/libc/string_c.c:201.
tests/libc/string_c.c:201:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] computing for function strlen <- strrchr <- test_strrchr <- main.
        Called from share/libc/string.c:200.
[value] Recording results for strlen
[value] Done for function strlen
[value] Recording results for strrchr
[value] Done for function strrchr
tests/libc/string_c.c:202:[value] assertion got status valid.
[value] Recording results for test_strrchr
[value] Done for function test_strrchr
[value] computing for function test_memchr <- main.
        Called from tests/libc/string_c.c:275.
[value] computing for function memchr <- test_memchr <- main.
        Called from tests/libc/string_c.c:208.
share/libc/string.h:42:[value] function memchr: precondition got status valid.
tests/libc/string_c.c:208:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:46:[value] function memchr, behavior found: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:47:[value] function memchr, behavior found: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:48:[value] warning: function memchr, behavior found: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:53:[value] warning: function memchr, behavior not_found: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] Recording results for memchr
[value] Done for function memchr
tests/libc/string_c.c:209:[value] assertion got status valid.
[value] computing for function memchr <- test_memchr <- main.
        Called from tests/libc/string_c.c:210.
tests/libc/string_c.c:210:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:46:[value] warning: function memchr, behavior found: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:47:[value] warning: function memchr, behavior found: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
share/libc/string.h:53:[value] function memchr, behavior not_found: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] Recording results for memchr
[value] Done for function memchr
tests/libc/string_c.c:211:[value] assertion got status valid.
[value] computing for function memchr <- test_memchr <- main.
        Called from tests/libc/string_c.c:212.
tests/libc/string_c.c:212:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] Recording results for memchr
[value] Done for function memchr
tests/libc/string_c.c:213:[value] assertion got status valid.
[value] computing for function memchr <- test_memchr <- main.
        Called from tests/libc/string_c.c:214.
tests/libc/string_c.c:214:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] Recording results for memchr
[value] Done for function memchr
tests/libc/string_c.c:215:[value] assertion got status valid.
[value] computing for function memchr <- test_memchr <- main.
        Called from tests/libc/string_c.c:216.
tests/libc/string_c.c:216:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] Recording results for memchr
[value] Done for function memchr
tests/libc/string_c.c:217:[value] assertion got status valid.
[value] computing for function memchr <- test_memchr <- main.
        Called from tests/libc/string_c.c:218.
tests/libc/string_c.c:218:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] Recording results for memchr
[value] Done for function memchr
tests/libc/string_c.c:219:[value] assertion got status valid.
[value] Recording results for test_memchr
[value] Done for function test_memchr
[value] computing for function test_memrchr <- main.
        Called from tests/libc/string_c.c:276.
[value] computing for function memrchr <- test_memrchr <- main.
        Called from tests/libc/string_c.c:225.
[value] Recording results for memrchr
[value] Done for function memrchr
tests/libc/string_c.c:226:[value] assertion got status valid.
[value] computing for function memrchr <- test_memrchr <- main.
        Called from tests/libc/string_c.c:227.
[value] Recording results for memrchr
[value] Done for function memrchr
tests/libc/string_c.c:228:[value] assertion got status valid.
[value] computing for function memrchr <- test_memrchr <- main.
        Called from tests/libc/string_c.c:229.
[value] Recording results for memrchr
[value] Done for function memrchr
tests/libc/string_c.c:230:[value] assertion got status valid.
[value] computing for function memrchr <- test_memrchr <- main.
        Called from tests/libc/string_c.c:231.
[value] Recording results for memrchr
[value] Done for function memrchr
tests/libc/string_c.c:232:[value] assertion got status valid.
[value] computing for function memrchr <- test_memrchr <- main.
        Called from tests/libc/string_c.c:233.
[value] Recording results for memrchr
[value] Done for function memrchr
tests/libc/string_c.c:234:[value] assertion got status valid.
[value] computing for function memrchr <- test_memrchr <- main.
        Called from tests/libc/string_c.c:235.
[value] Recording results for memrchr
[value] Done for function memrchr
tests/libc/string_c.c:236:[value] assertion got status valid.
[value] Recording results for test_memrchr
[value] Done for function test_memrchr
[value] computing for function test_strstr <- main.
        Called from tests/libc/string_c.c:277.
[value] computing for function strstr <- test_strstr <- main.
        Called from tests/libc/string_c.c:242.
share/libc/string.h:176:[value] function strstr: precondition 'valid_string_haystack' got status valid.
share/libc/string.h:177:[value] function strstr: precondition 'valid_string_needle' got status valid.
share/libc/string.c:234:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
share/libc/string.h:179:[value] warning: function strstr: postcondition got status unknown.
[value] Recording results for strstr
[value] Done for function strstr
tests/libc/string_c.c:243:[value] assertion got status valid.
[value] computing for function strstr <- test_strstr <- main.
        Called from tests/libc/string_c.c:244.
[value] Recording results for strstr
[value] Done for function strstr
tests/libc/string_c.c:245:[value] assertion got status valid.
[value] computing for function strstr <- test_strstr <- main.
        Called from tests/libc/string_c.c:246.
share/libc/string.h:179:[value] function strstr: postcondition got status valid.
[value] Recording results for strstr
[value] Done for function strstr
tests/libc/string_c.c:247:[value] assertion got status valid.
[value] computing for function strstr <- test_strstr <- main.
        Called from tests/libc/string_c.c:248.
[value] Recording results for strstr
[value] Done for function strstr
tests/libc/string_c.c:249:[value] assertion got status valid.
[value] computing for function strstr <- test_strstr <- main.
        Called from tests/libc/string_c.c:250.
[value] Recording results for strstr
[value] Done for function strstr
tests/libc/string_c.c:251:[value] assertion got status valid.
[value] computing for function strstr <- test_strstr <- main.
        Called from tests/libc/string_c.c:252.
[value] Recording results for strstr
[value] Done for function strstr
tests/libc/string_c.c:253:[value] assertion got status valid.
[value] computing for function strstr <- test_strstr <- main.
        Called from tests/libc/string_c.c:254.
[value] Recording results for strstr
[value] Done for function strstr
tests/libc/string_c.c:255:[value] assertion got status valid.
[value] computing for function strstr <- test_strstr <- main.
        Called from tests/libc/string_c.c:256.
[value] Recording results for strstr
[value] Done for function strstr
tests/libc/string_c.c:257:[value] assertion got status valid.
[value] Recording results for test_strstr
[value] Done for function test_strstr
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function memchr:
  ch ∈ {1; 2; 5}
  ss ∈ {{ (unsigned char const *)&s }}
  __retres ∈ {{ NULL ; (void *)&s{[0], [1]} }}
[value:final-states] Values at end of function memcmp:
  p1 ∈ {{ "hallo" ; "hallo" ; "a\000b" ; "a\000b" }}
  p2 ∈ {{ (unsigned char const *)&hello ; "a\000c" ; "a\000c" }}
  __retres ∈ {-4; -1; 0}
[value:final-states] Values at end of function memmove:
  s ∈ {{ &buf{[0], [2]} }}
  buf[0] ∈ {1; 3}
     [1] ∈ {2; 4}
     [2] ∈ {1; 5}
     [3] ∈ {2; 6}
     [4] ∈ {3; 5}
     [5] ∈ {4; 6}
  __retres ∈ {{ (void *)&buf{[0], [2]} }}
[value:final-states] Values at end of function memrchr:
  ch ∈ {1; 2; 5}
  ss ∈ {{ (unsigned char const *)&s }}
  __retres ∈ {{ NULL ; (void *)&s{[0], [3], [4]} }}
[value:final-states] Values at end of function memset:
  p ∈ {{ (unsigned char *)&dest }}
  dest[0..2] ∈ {42}
      [3] ∈ {0}
[value:final-states] Values at end of function strchr:
  ch ∈ {0; 72; 104; 108}
  i ∈ {0; 2; 5}
  __retres ∈ {{ NULL ; "hello" + {0; 2; 5} }}
[value:final-states] Values at end of function strcmp:
  i ∈ {0; 1; 4; 5}
  __retres ∈ {-111; -104; -32; 0; 111}
[value:final-states] Values at end of function strcpy:
  i ∈ {0; 5; 6}
  s[0] ∈ {0; 54; 104}
   [1] ∈ {53; 101}
   [2] ∈ {52; 108}
   [3] ∈ {51; 108}
   [4] ∈ {50; 111}
   [5] ∈ {0; 49}
   [6] ∈ {0} or UNINITIALIZED
[value:final-states] Values at end of function strlen:
  i ∈ {0; 2; 4; 5; 7}
[value:final-states] Values at end of function strcat:
  i ∈ {0; 1; 3; 5}
  n ∈ {0; 4; 7}
  s[0] ∈ {104}
   [1] ∈ {101}
   [2..3] ∈ {108}
   [4] ∈ {104; 111}
   [5] ∈ {0; 101}
   [6] ∈ {108} or UNINITIALIZED
   [7] ∈ {0; 120} or UNINITIALIZED
   [8] ∈ {0} or UNINITIALIZED
   [9] ∈ UNINITIALIZED
[value:final-states] Values at end of function strncmp:
  __retres ∈ {-104; -4; 0; 111}
[value:final-states] Values at end of function strncpy:
  i ∈ {0; 3; 5; 7}
  s[0] ∈ {97; 98; 104}
   [1] ∈ {98; 101; 121}
   [2] ∈ {0; 101; 108}
   [3] ∈ {0; 108}
   [4] ∈ {0; 111}
   [5..6] ∈ {0}
[value:final-states] Values at end of function strrchr:
  ch ∈ {0; 72; 104; 108}
  __retres ∈ {{ NULL ; "hello" + {0; 3; 5} }}
[value:final-states] Values at end of function strstr:
  __retres ∈ {{ NULL ; "hello" + {0; 2; 3} }}
[value:final-states] Values at end of function test_memchr:
  s[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {1}
   [4] ∈ {2}
   [5] ∈ {4}
  p ∈ {{ &s[0] }}
[value:final-states] Values at end of function test_memcmp:
  hello[0] ∈ {104}
       [1] ∈ {101}
       [2..3] ∈ {108}
       [4] ∈ {111}
       [5] ∈ {0}
  res1 ∈ {-4}
  res2 ∈ {0}
  res3 ∈ {0}
  res4 ∈ {-1}
[value:final-states] Values at end of function test_memcpy:
  dest[bits 0 to 31] ∈ {302594113}
      [4..5] ∈ {0}
  src[0] ∈ {104}
     [1] ∈ {101}
     [2..3] ∈ {108}
     [4] ∈ {111}
     [5] ∈ {0}
  p ∈ {0}
  src2[0] ∈ {97}
      [1] ∈ {0}
      [2] ∈ {98}
      [3..4] ∈ {0}
  x ∈ {302594113}
[value:final-states] Values at end of function test_memmove:
  buf[0] ∈ {3}
     [1] ∈ {4}
     [2] ∈ {5}
     [3] ∈ {6}
     [4] ∈ {5}
     [5] ∈ {6}
  s ∈ {{ &buf[2] }}
  d ∈ {{ &buf[0] }}
  p ∈ {{ &buf[2] }}
[value:final-states] Values at end of function test_memrchr:
  s[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {1}
   [4] ∈ {2}
   [5] ∈ {4}
  p ∈ {{ &s[0] }}
[value:final-states] Values at end of function test_memset:
  dest[0..2] ∈ {42}
      [3] ∈ {0}
  p ∈ {{ &dest[0] }}
[value:final-states] Values at end of function test_strcat:
  s[0] ∈ {104}
   [1] ∈ {101}
   [2..3] ∈ {108}
   [4] ∈ {104}
   [5] ∈ {101}
   [6] ∈ {108}
   [7] ∈ {120}
   [8] ∈ {0}
   [9] ∈ UNINITIALIZED
  p ∈ {{ &s[0] }}
[value:final-states] Values at end of function test_strchr:
  s ∈ {{ "hello" }}
  p ∈ {{ "hello" + {5} }}
[value:final-states] Values at end of function test_strcmp:
  hello[0] ∈ {104}
       [1] ∈ {97}
       [2..3] ∈ {108}
       [4] ∈ {111}
       [5] ∈ {0}
  res ∈ {0}
  res2 ∈ {-111}
  res3 ∈ {111}
  res4 ∈ {-32}
  res5 ∈ {-104}
  res6 ∈ {0}
  res7 ∈ {0}
[value:final-states] Values at end of function test_strcpy:
  s[0] ∈ {0}
   [1] ∈ {53}
   [2] ∈ {52}
   [3] ∈ {51}
   [4] ∈ {50}
   [5] ∈ {49}
   [6] ∈ {0}
  p ∈ {{ &s[0] }}
[value:final-states] Values at end of function test_strlen:
  s ∈ {{ "hello" }}
  n ∈ {0}
[value:final-states] Values at end of function test_strncmp:
  hello[0] ∈ {104}
       [1] ∈ {97}
       [2..3] ∈ {108}
       [4] ∈ {111}
       [5] ∈ {0}
  res1 ∈ {-4}
  res2 ∈ {0}
  res3 ∈ {0}
  res4 ∈ {111}
  res5 ∈ {0}
  res6 ∈ {-104}
  res7 ∈ {0}
  res8 ∈ {0}
[value:final-states] Values at end of function test_strncpy:
  s[0] ∈ {97}
   [1] ∈ {98}
   [2..6] ∈ {0}
  p ∈ {{ &s[0] }}
[value:final-states] Values at end of function test_strrchr:
  s ∈ {{ "hello" }}
  p ∈ {{ "hello" + {5} }}
[value:final-states] Values at end of function test_strstr:
  s ∈ {{ "hello" }}
  p ∈ {{ "hello" }}
[value:final-states] Values at end of function main:
  __retres ∈ {0}