From 5c36e9dcb5ec1213b6d0a42971afabaa789f20ac Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 18 Jun 2026 17:25:56 -0700 Subject: [PATCH 1/3] REGR: add regression tests --- .../fold_search_index_upper_bound.c | 81 +++++++++++++++ .../imagick-pointer-plus-index-global-po.c | 27 +++++ .../regression/initialized_range_from_init.c | 64 ++++++++++++ tests/regression/no_overlap_disjoint_allocs.c | 57 +++++++++++ .../not_zero_static_const_divisor.c | 66 +++++++++++++ .../null_terminated_argv_after_guard.c | 54 ++++++++++ .../regression/pointer_plus_int_upper_bound.c | 30 ++++++ .../regression/signed_to_signed_cast_bitor.c | 26 +++++ .../stack_address_escape_scratch_buffer.c | 20 ++++ tests/regression/struct_heap_invariant.c | 68 +++++++++++++ tests/regression/tests.json | 98 +++++++++++++++++++ .../uint16_swap_intermediate_cast.c | 72 ++++++++++++++ 12 files changed, 663 insertions(+) create mode 100644 tests/regression/fold_search_index_upper_bound.c create mode 100644 tests/regression/imagick-pointer-plus-index-global-po.c create mode 100644 tests/regression/initialized_range_from_init.c create mode 100644 tests/regression/no_overlap_disjoint_allocs.c create mode 100644 tests/regression/not_zero_static_const_divisor.c create mode 100644 tests/regression/null_terminated_argv_after_guard.c create mode 100644 tests/regression/pointer_plus_int_upper_bound.c create mode 100644 tests/regression/signed_to_signed_cast_bitor.c create mode 100644 tests/regression/stack_address_escape_scratch_buffer.c create mode 100644 tests/regression/struct_heap_invariant.c create mode 100644 tests/regression/uint16_swap_intermediate_cast.c diff --git a/tests/regression/fold_search_index_upper_bound.c b/tests/regression/fold_search_index_upper_bound.c new file mode 100644 index 0000000..dc737b9 --- /dev/null +++ b/tests/regression/fold_search_index_upper_bound.c @@ -0,0 +1,81 @@ +/* Binary search index-upper-bound precision gap. + + Models fold_search() from u8c (github_rdentato_u8c/u8c/u8c.c) at small + scale to study two CodeHawk analysis phenomena. + + 1. WHY OPEN POs PERSIST EVEN IN THE FIXED VERSION (fold_search_fixed): + The loop invariant that bounds k is relational: i <= j <= N-1, so + k = (i+j)/2 <= N-1. The interval domain cannot express the + relationship between i and j, so interval widening overestimates the + upper bound of i (beyond N-1), which in turn pushes the computed + upper bound of k above N-1. The PO k <= N-1 remains open. + The same widening gap affects fold_search_buggy (j=N); both functions + produce identical open PO counts. The difference is correctness, not + what CodeHawk can prove. + + 2. WHY THE BUGGY VERSION (fold_search_buggy) IS NOT FLAGGED AS VIOLATED: + A violated PO means CodeHawk proves the constraint is *always* false. + k's abstract value spans [0, k_max] where k_max > N-1, but the lower + end of the interval is within [0, N-1]. Since k can be valid on + early iterations, CodeHawk cannot prove k is always >= N, so the PO + is open (might be violated) rather than violated (always violated). + + 3. WHAT DOES PRODUCE A VIOLATION: + fold_search_oob_step hard-codes the loop state at the step where the + OOB read occurs (i=N, j=N, giving k=N). The constant index k=N is + immediately seen to be >= the array size, so the PO is violated. + This confirms CodeHawk can detect the OOB access; it just cannot + back-propagate that reachable state through the loop abstraction. +*/ + +#define N 5 + +static int arr[N] = {10, 20, 30, 40, 50}; + +/* Buggy: j = N = 5; valid indices are 0..4 (OOB when all arr elements < cp). */ +int fold_search_buggy(int cp) +{ + int i = 0, j = N, k; + while (i <= j) { + k = (i + j) / 2; + if (cp == arr[k]) return 1; + if (cp < arr[k]) j = k - 1; + else i = k + 1; + } + return 0; +} + +/* Fixed: j = N-1 = 4; last valid index. Same open POs as buggy version + because the interval domain cannot exploit the invariant i <= j <= 4. */ +int fold_search_fixed(int cp) +{ + int i = 0, j = N - 1, k; + while (i <= j) { + k = (i + j) / 2; + if (cp == arr[k]) return 1; + if (cp < arr[k]) j = k - 1; + else i = k + 1; + } + return 0; +} + +/* Hard-codes the loop state at the last valid iteration of fold_search_fixed: + i = N-1, j = N-1 => k = (N-1 + N-1) / 2 = N-1, the last valid index. + Produces a concrete safe index-upper-bound PO, confirming the fixed version + is safe when the loop state is known precisely. */ +int fold_search_safe_step(void) +{ + int i = N - 1, j = N - 1; + int k = (i + j) / 2; + return arr[k]; +} + +/* Hard-codes the loop state at the step where fold_search_buggy reads OOB: + i = N, j = N => k = (N + N) / 2 = N, which is >= array size N. + Produces a concrete violated index-upper-bound PO. */ +int fold_search_oob_step(void) +{ + int i = N, j = N; + int k = (i + j) / 2; + return arr[k]; +} diff --git a/tests/regression/imagick-pointer-plus-index-global-po.c b/tests/regression/imagick-pointer-plus-index-global-po.c new file mode 100644 index 0000000..b2e6bc7 --- /dev/null +++ b/tests/regression/imagick-pointer-plus-index-global-po.c @@ -0,0 +1,27 @@ +typedef unsigned short IndexPacket; +typedef long ssize_t; + +static void set_index(IndexPacket *p, IndexPacket value) { + *p = value; +} + +void import_index_alpha(IndexPacket *restrict indexes, ssize_t number_pixels) { + ssize_t x; + ssize_t bit; + + for (x = number_pixels - 3; x > 0; x -= 4) { + for (bit = 0; bit < 8; bit += 2) { + set_index(indexes + x + bit / 2, 1); + } + } +} + + +int main(int argc, char **argv) { + + IndexPacket packets[10]; + + import_index_alpha(packets, 10); + + return 0; +} diff --git a/tests/regression/initialized_range_from_init.c b/tests/regression/initialized_range_from_init.c new file mode 100644 index 0000000..cb994d1 --- /dev/null +++ b/tests/regression/initialized_range_from_init.c @@ -0,0 +1,64 @@ +/* Regression test for R8: initialized-range discharge handler does not derive + from scalar assignment, struct-copy assignment, or memset. + + fwrite generates an initialized-range PO for its buffer argument. + All three patterns below produce open POs even though the memory is + provably initialized by the time fwrite is called. + + Pattern A -- scalar local with constant initializer: + uint16_t val = 42; + fwrite(&val, sizeof(uint16_t), 1, fp); + The scalar initialized(val) would be safe, but initialized-range(&val, 2) + is open because the handler does not derive byte-range initialization + from a scalar assignment fact. + + Pattern B -- struct-copy initialized local: + pair_t p = *src; + fwrite(&(p.a), sizeof(uint32_t), 1, fp); + initialized((*src)) is delegated to the API (caller's guarantee). + The struct copy p = *src initializes all fields, but + initialized-range(&p.a, 4) is open because the handler does not + propagate struct-level initialization to per-field byte ranges. + + Pattern C -- memset-initialized buffer: + char *buf = malloc(n); + memset(buf, 0, n); + fwrite(buf, n, 1, fp); + memset(buf, 0, n) establishes initialized-range(buf, n) semantically, + but the handler has no transfer function for memset, so the PO is open. + + Goal: after adding the three transfer functions, all initialized-range + POs here should become safe (patterns A and B) or safe once buf is + non-null (pattern C). +*/ + +#include +#include +#include +#include + +/* Pattern A */ +void write_scalar(FILE *fp) +{ + uint16_t val = 42; + fwrite(&val, sizeof(uint16_t), 1, fp); +} + +/* Pattern B */ +typedef struct { uint32_t a; uint16_t b; } pair_t; + +void write_struct_fields(pair_t *src, FILE *fp) +{ + pair_t p = *src; + fwrite(&(p.a), sizeof(uint32_t), 1, fp); + fwrite(&(p.b), sizeof(uint16_t), 1, fp); +} + +/* Pattern C */ +void write_memset_buffer(FILE *fp, int n) +{ + char *buf = malloc(n); + memset(buf, 0, n); + fwrite(buf, n, 1, fp); + free(buf); +} diff --git a/tests/regression/no_overlap_disjoint_allocs.c b/tests/regression/no_overlap_disjoint_allocs.c new file mode 100644 index 0000000..d2318cc --- /dev/null +++ b/tests/regression/no_overlap_disjoint_allocs.c @@ -0,0 +1,57 @@ +/* Regression test for R9: no-overlap discharge handler does not use + allocation-site disjointness. + + fwrite generates a no-overlap PO checking that the buffer and FILE pointer + arguments do not point to overlapping memory. When the two pointers come + from provably different allocation origins (stack, malloc, fopen) they + cannot overlap, but the handler does not apply this rule. + + Pattern A -- stack local vs FILE* from fopen: + FILE *fp = fopen(...); + uint16_t val = 42; + fwrite(&val, sizeof(uint16_t), 1, fp); + -- no-overlap(&val, fp): &val is a stack address (addrof_localvar_...), + fp is a heap address from fopen. Stack and heap are disjoint + allocation regions; no-overlap should discharge. + + Pattern B -- malloc buffer vs FILE* from fopen: + FILE *fp = fopen(...); + char *buf = malloc(n); + fwrite(buf, n, 1, fp); + -- no-overlap(buf, fp): buf comes from malloc@this-callsite, + fp comes from fopen@that-callsite. Two allocations from different + call sites produce non-overlapping regions; no-overlap should discharge. + + The investigate output shows the analyzer already has both allocation + origins in each case (different sx/regions fields for the two arguments) + but the handler does not use the mutual-exclusivity rule. + + Goal: with an allocation-site disjointness rule in the no-overlap handler, + all no-overlap POs here should become safe. +*/ + +#include +#include +#include + +/* Pattern A */ +void write_scalar_to_file(const char *path) +{ + FILE *fp = fopen(path, "wb"); + if (fp == NULL) return; + uint16_t val = 42; + fwrite(&val, sizeof(uint16_t), 1, fp); + fclose(fp); +} + +/* Pattern B */ +void write_buffer_to_file(const char *path, int n) +{ + FILE *fp = fopen(path, "wb"); + if (fp == NULL) return; + char *buf = malloc(n); + if (buf == NULL) { fclose(fp); return; } + fwrite(buf, n, 1, fp); + free(buf); + fclose(fp); +} diff --git a/tests/regression/not_zero_static_const_divisor.c b/tests/regression/not_zero_static_const_divisor.c new file mode 100644 index 0000000..35eabe6 --- /dev/null +++ b/tests/regression/not_zero_static_const_divisor.c @@ -0,0 +1,66 @@ +/* Regression test for not-zero false positive on static const divisors. + + Pattern: static const variables initialized with compile-time constant + expressions are not recognized as non-zero by CodeHawk. Any division or + modulo that uses one as a divisor produces an open not-zero PO, even + though all values are provably non-zero. + + Contrast: #define macros ARE treated as integer literals and do discharge + not-zero obligations. + + Root cause: CodeHawk does not propagate constant values through static const + variable initializers. Even a direct literal like `static const int A = 60` + is modelled as an opaque global variable of unknown value. A chain like + `static const int B = A * 60` is even further removed from any concrete + bound. + + Three levels of initialization depth are shown: + depth 0: literal initializer (SECONDS_PER_MINUTE = 60) + depth 1: one-level product (SECONDS_PER_HOUR = MINUTES * SECS) + depth 2: two-level product (SECONDS_PER_DAY = HOURS * SECS_PER_HOUR) + + Both / and % are included because both generate not-zero obligations. + + Goal: with constant-value propagation for static const initializers, all + not-zero POs below should become safe. +*/ + +static const int SECONDS_PER_MINUTE = 60; +static const int MINUTES_PER_HOUR = 60; +static const int HOURS_PER_DAY = 24; + +static const int SECONDS_PER_HOUR = MINUTES_PER_HOUR * SECONDS_PER_MINUTE; +static const int SECONDS_PER_DAY = HOURS_PER_DAY * SECONDS_PER_HOUR; + +/* Depth 0: literal initializer used as divisor. */ +int div_by_literal_const(int seconds) +{ + return seconds / SECONDS_PER_MINUTE; /* not-zero(SECONDS_PER_MINUTE) OPEN */ +} + +int mod_by_literal_const(int seconds) +{ + return seconds % SECONDS_PER_MINUTE; /* not-zero(SECONDS_PER_MINUTE) OPEN */ +} + +/* Depth 1: one-level product used as divisor. */ +int div_by_derived_const(int seconds) +{ + return seconds / SECONDS_PER_HOUR; /* not-zero(SECONDS_PER_HOUR) OPEN */ +} + +int mod_by_derived_const(int seconds) +{ + return seconds % SECONDS_PER_HOUR; /* not-zero(SECONDS_PER_HOUR) OPEN */ +} + +/* Depth 2: two-level product used as divisor. */ +int div_by_chained_const(int seconds) +{ + return seconds / SECONDS_PER_DAY; /* not-zero(SECONDS_PER_DAY) OPEN */ +} + +int mod_by_chained_const(int seconds) +{ + return seconds % SECONDS_PER_DAY; /* not-zero(SECONDS_PER_DAY) OPEN */ +} diff --git a/tests/regression/null_terminated_argv_after_guard.c b/tests/regression/null_terminated_argv_after_guard.c new file mode 100644 index 0000000..99abaf7 --- /dev/null +++ b/tests/regression/null_terminated_argv_after_guard.c @@ -0,0 +1,54 @@ +/* Regression test for R10: argv discharge handler uses argc#init (unconstrained + formal-parameter value) instead of the compound path-constraint interval when + the path to the access point passes through multiple guards. + + The handler uses a parameter-constraint mechanism: "what constraint on argc#init + is implied by the guards that must be passed to reach this statement?" + + For a single guard `if (argc < N) return`, the constraint argc#init >= N is + derived and discharges argv[i] for i < N. But when the path to the access + point has BOTH an outer guard establishing argc >= 1 AND being inside a + branch that implies argc < N, the compound constraint argc#init in [1, N-1] + is not synthesised. The handler reports "Unable to prove index < argc#init" + because it uses argc#init as unconstrained. + + Concretely: + if (argc == 0) --> establishes argc >= 1 + return 1; + if (argc < 3) { --> inside this branch: argc in [1, 2] + printf(argv[0]); --> null-terminated(argv[0]) OPEN + return 1; --> handler needs 0 < argc#init -- true since argc >= 1 + } --> but handler can't prove it from argc#init alone + return atoi(argv[1]) --> null-terminated(argv[1]) SAFE: argc#init >= 3 > 1 + + atoi(argv[2]); --> null-terminated(argv[2]) SAFE: argc#init >= 3 > 2 + + The SAFE cases work because the single guard argc >= 3 gives a direct + parameter constraint for the after-guard accesses. The OPEN cases arise + inside the guard branch where the constraint requires composing two guards. + + Open POs at the argv[0] access (line 13): + null-terminated(argv[0]) Unable to prove index < argc#init + initialized-range(argv[0]) Unable to prove index < argc#init + not-null(argv[0]) Unable to prove index < argc#init + initialized(argv[0]) Unable to prove index < argc#init + ptr-upper-bound(argv[0]) Unable to prove index < argc#init + valid-mem(argv[0]) Unable to prove index < argc#init + + Goal: with a compound-guard parameter constraint (composing outer and inner + guards), all six open POs should become safe. +*/ + +#include +#include + +int main(int argc, char **argv) +{ + if (argc == 0) /* establishes argc in [1, +inf) */ + return 1; + if (argc < 3) { /* inside: argc in [1, 2]; argv[0] should be valid */ + printf("usage: %s a b\n", argv[0]); + return 1; + } + /* argc in [3, +inf): single-guard constraint argc#init >= 3 fires, both safe */ + return atoi(argv[1]) + atoi(argv[2]); +} diff --git a/tests/regression/pointer_plus_int_upper_bound.c b/tests/regression/pointer_plus_int_upper_bound.c new file mode 100644 index 0000000..cdcf35c --- /dev/null +++ b/tests/regression/pointer_plus_int_upper_bound.c @@ -0,0 +1,30 @@ +/* + * Reproducer for a CodeHawk-C expression-reconstruction failure seen in + * perlbench cpan/Digest-MD5/MD5.c:base64_16. + * + * The relevant shape is pointer increment on an output buffer: + * + * *d++ = table[index]; + * + * CH-C can lower pointer arithmetic to abstract XPlus/XMinus expressions. + * In the failing checker path, XPlus over a char pointer and an integer was + * reconstructed as arithmetic PlusA and get_integer_promotion was called on + * (char *) and int, causing a fatal analyzer failure while checking an + * upper-bound obligation. + */ + +static const char table[] = + "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"; + +char *pointer_plus_int_upper_bound(const unsigned char *from, char *to) { + const unsigned char *end = from + 16; + char *d = to; + + while (from < end) { + unsigned char c1 = *from++; + *d++ = table[c1 >> 2]; + } + + *d = '\0'; + return to; +} diff --git a/tests/regression/signed_to_signed_cast_bitor.c b/tests/regression/signed_to_signed_cast_bitor.c new file mode 100644 index 0000000..483f519 --- /dev/null +++ b/tests/regression/signed_to_signed_cast_bitor.c @@ -0,0 +1,26 @@ +/* Reproducer for open signed-to-signed-cast obligations caused by missing + range propagation through bitwise OR. + + When a constant C with the high bit set (C > 127) is OR'd with a + non-negative integer x, the result is provably in [C, INT_MAX], so: + - signed-to-signed-cast-lb (result >= -128) is safe (C >= 0 >= -128) + - signed-to-signed-cast-ub (result <= 127) is a violation (result >= C > 127) + + Both are currently 'open' because xop_2_numexpr in xprUtil.ml (xprlib) + translates XBOr to an unconstrained fresh temporary (RANDOM), so the + abstract interpreter produces no invariant for the OR expression. + + Observed as 18 open obligations (9 lb + 9 ub) in u8encode_() in u8c. + + Recommended fix (Option A) -- no new infrastructure needed: + In cCHPOCheckSignedToSignedCastLB.ml, extend xpr_implies_safe_lb to + recognise XOp(XBOr, [XConst c; _]) and conclude safe when c#geq safelb. + In cCHPOCheckSignedToSignedCastUB.ml, extend xpr_implies_safe_ub to + recognise XOp(XBOr, [XConst c; _]) and conclude violation when c#gt safeub. +*/ + +void encode_lead_byte(int x, char *s) +{ + if (x >= 0) + *s = (char)(0xC0 | x); +} diff --git a/tests/regression/stack_address_escape_scratch_buffer.c b/tests/regression/stack_address_escape_scratch_buffer.c new file mode 100644 index 0000000..a91bd29 --- /dev/null +++ b/tests/regression/stack_address_escape_scratch_buffer.c @@ -0,0 +1,20 @@ +/* Reproducer for false-positive stack-address-escape when a local array is + used as a scratch buffer via a value-parameter pointer. + + Pattern: if the caller passes NULL for the output pointer, the function + falls back to a local buffer so it can still compute and return the length. + Because `s` is a plain `char *` (passed by value), the address of `t` can + never reach the caller -- no escape is possible. The analyzer should + discharge all stack-address-escape obligations here as safe. + + Observed as 13 violations in u8encode_() in github_rdentato_u8c. +*/ + +int encode(int ch, char *s) +{ + char t[8]; + if (s == 0) s = t; + *s++ = (char)ch; + *s = '\0'; + return 1; +} diff --git a/tests/regression/struct_heap_invariant.c b/tests/regression/struct_heap_invariant.c new file mode 100644 index 0000000..c9918dd --- /dev/null +++ b/tests/regression/struct_heap_invariant.c @@ -0,0 +1,68 @@ +/* Open proof obligations on a heap-allocated struct field accessed through + a bounds-guarded setter. + + Pattern: a struct holds a malloc'd array and its size. A "create" + function establishes the invariant; a "set" function accesses the + array after a bounds check. Because the invariant + + not-null(v->data) && size(v->data) == v->size + + is established by ivec_create but not tracked across the function + boundary, the write v->data[i] = val in ivec_set carries open POs + even though the bounds check i < 0 || i >= v->size is correct. + + Open POs in ivec_set at v->data[i] = val: + not-null(v->data) data field came from malloc in another fn + valid-mem(v->data) no cross-function heap model + in-scope(v->data) same + initialized(v->data) data pointer was set in another fn + ptr-upper-bound-deref(v->data, i) i < v->size does not imply + i < size(v->data) without invariant + upper-bound(v->data, i) same + lower-bound(v->data, i) same (though i >= 0 is known from guard) + + The bounds guard is correct -- the access is safe -- but the interval + domain cannot bridge the gap between the runtime value v->size and the + allocated size of v->data without an explicit struct invariant. + + Inspired by bmp_set_pixel() in github_envyen_libbmp, which has 13 open + POs on bmp->pixels[x][y] = pixel for the same reason. The two levels + of indirection there add further not-null, valid-mem, and + ptr-upper-bound-deref obligations for the row pointers, but the root + cause is identical. + + Goal: with data-structure invariant support expressing + not-null(this->data) && size(this->data) >= this->size + as a postcondition of ivec_create and an assumed precondition of + ivec_set, all open POs should be discharged as safe. +*/ + +#include + +typedef struct { + int size; + int *data; +} ivec_t; + +/* Establishes the struct invariant: data is non-null, allocated for + exactly size ints, all initialised to 0. */ +ivec_t *ivec_create(int n) +{ + ivec_t *v = malloc(sizeof(ivec_t)); + v->data = malloc(sizeof(int) * n); + int i; + for (i = 0; i < n; ++i) + v->data[i] = 0; + v->size = n; + return v; +} + +/* Bounds-checked setter. The guard is correct; the open POs arise + because the analyzer has no model connecting size(v->data) to v->size. */ +int ivec_set(ivec_t *v, int i, int val) +{ + if (i < 0 || i >= v->size) + return 0; + v->data[i] = val; + return 1; +} diff --git a/tests/regression/tests.json b/tests/regression/tests.json index be51529..0fd4251 100644 --- a/tests/regression/tests.json +++ b/tests/regression/tests.json @@ -19,6 +19,22 @@ "safe": 37 } }, + { + "filename": "imagick-pointer-plus-index-global-po.c", + "description": "Issue #79, CodeHawk-C", + "expected": { + "safe": 50, + "open": 3 + } + }, + { + "filename": "pointer_plus_int_upper_bound.c", + "description": "Issue #76, CodeHawk-C", + "expected": { + "safe": 66, + "open": 12 + } + }, { "filename": "my_regexec_pointer_diff_cast.c", "expected": { @@ -34,6 +50,88 @@ "open": 5 }, "goal": "improve" + }, + { + "filename": "stack_address_escape_scratch_buffer.c", + "description": "False-positive stack-address-escape: local array used as scratch buffer via value-parameter pointer; address cannot escape since s is passed by value, not char**", + "expected": { + "violation": 2, + "open": 2 + }, + "goal": "improve" + }, + { + "filename": "signed_to_signed_cast_bitor.c", + "description": "Open signed-to-signed-cast obligations due to missing bitwise-OR range propagation: xop_2_numexpr treats XBOr as RANDOM; with Option A fix, lb->safe (C>=safelb), ub->violation (C>safeub)", + "expected": { + "open": 2 + }, + "goal": "improve" + }, + { + "filename": "uint16_swap_intermediate_cast.c", + "description": "False-positive signed-to-unsigned-cast-ub: caste(uint16_t, X) where X > 65535 is not modelled as modular truncation; the un-truncated int value propagates into the OR and exceeds uint16_t max; byte_swap_lo (val=31) is correctly safe because 31<<8=7936 fits in uint16_t without truncation", + "expected": { + "safe": 52, + "violation": 2 + }, + "goal": "improve" + }, + { + "filename": "fold_search_index_upper_bound.c", + "description": "Binary search index-upper-bound precision gap: interval widening overestimates k's range (buggy j=N gives k in [0,6]; fixed j=N-1 gives k in [0,5]); both produce open POs because the relational invariant i<=j cannot be expressed in the interval domain; violation only detectable via direct constant OOB access (fold_search_oob_step)", + "expected": { + "safe": 63, + "open": 4, + "violation": 1 + }, + "goal": "improve" + }, + { + "filename": "struct_heap_invariant.c", + "description": "Cross-function heap invariant gap: ivec_set accesses v->data after a bounds check but carries 6 open POs (not-null, valid-mem, in-scope, lower-bound, upper-bound, ptr-upper-bound-deref) because the analyzer has no model for the postcondition of ivec_create (data is non-null and size(data)==size); inspired by bmp_set_pixel in libbmp with 13 open POs on pixels[x][y] for the same root cause", + "expected": { + "safe": 74, + "open": 18 + }, + "goal": "improve" + }, + { + "filename": "initialized_range_from_init.c", + "description": "R8: initialized-range discharge handler has no transfer functions for (A) scalar assignment -- uint16_t val=42; fwrite(&val,...) -- (B) struct-copy -- pair_t p=*src; fwrite(&p.a,...) -- or (C) memset -- memset(buf,0,n); fwrite(buf,...); in all three cases the byte range is provably initialized but the handler lacks the scalar->range, struct-copy->field-range, and memset->range rules", + "expected": { + "safe": 108, + "open": 15 + }, + "goal": "improve" + }, + { + "filename": "no_overlap_disjoint_allocs.c", + "description": "R9: no-overlap discharge handler does not use allocation-site disjointness; fwrite generates no-overlap(buf, fp) for its two arguments; when buf is a stack variable and fp is from fopen (different allocation origins: stack vs heap), or buf is from malloc and fp is from fopen (two distinct call sites), they cannot overlap but the handler does not apply the disjoint-allocation rule", + "expected": { + "safe": 124, + "open": 16 + }, + "goal": "improve" + }, + { + "filename": "not_zero_static_const_divisor.c", + "description": "R11: not-zero false positive on static const divisors -- CodeHawk models static const variables as opaque globals of unknown value, even when their initializers are compile-time constant expressions; every division or modulo by such a constant produces an open not-zero PO; as a side effect, int-overflow is also open for signed division (INT_MIN / -1 cannot be ruled out when the divisor is unknown); no int-overflow PO is generated for % -- this is consistent with C99 (S6.5.5p6 only says the constraint (a/b)*b+a%b==a holds when the quotient is representable, leaving % behavior unspecified when it is not) but would be a missing PO under C11 (S6.5.5p6 adds: otherwise the behavior of both a/b and a%b is undefined); three depth levels: literal initializer, one-level product, two-level product; contrast: #define macros ARE treated as literals and discharge not-zero", + "expected": { + "safe": 12, + "open": 12 + }, + "goal": "improve" + }, + { + "filename": "null_terminated_argv_after_guard.c", + "description": "R10: argv discharge handler uses argc#init (unconstrained formal-parameter value) when composing multiple path guards; after if(argc==0)return then inside if(argc<3), argc is in [1,2] so argv[0] should be valid, but the handler cannot derive 0 < argc#init from the compound constraint; single-guard paths work (argv[1] and argv[2] after the outer guard are safe); 6 open POs for argv[0] (null-terminated, initialized-range, not-null, initialized, ptr-upper-bound, valid-mem), 2 violations from atoi addition overflow", + "expected": { + "safe": 78, + "open": 6, + "violation": 2 + }, + "goal": "improve" } ] } diff --git a/tests/regression/uint16_swap_intermediate_cast.c b/tests/regression/uint16_swap_intermediate_cast.c new file mode 100644 index 0000000..22f3be1 --- /dev/null +++ b/tests/regression/uint16_swap_intermediate_cast.c @@ -0,0 +1,72 @@ +/* Reproducer for false-positive signed-to-unsigned-cast-ub caused by + missing intermediate narrowing-cast truncation in a byte-swap expression. + + Pattern (from the GLib-style UINT16_SWAP_LE_BE_CONSTANT macro in libbmp): + + (uint16_t) ( + (uint16_t) ((uint16_t)(val) >> 8) | + (uint16_t) ((uint16_t)(val) << 8) ) + + The inner cast (uint16_t)((uint16_t)(val) << 8) truncates the left-shifted + value to 16 bits before the OR. The OR of two uint16_t-bounded operands + is always in [0, 65535], so the outer cast to uint16_t is always safe. + + Root cause: the abstract interpreter does not model caste(uint16_t, X) as + a modular reduction when X > 65535. The abstract value of (uint16_t)(val) + << 8 is kept as the un-truncated int, and the OR is computed with that + large value, giving a lower bound that exceeds 65535. + + This is distinct from R4 (signed_to_signed_cast_bitor.c) where XBOr -> + RANDOM (no range at all). Here the OR IS computed correctly -- but with + the wrong (un-truncated) operand value. + + Three cases: + + (a) byte_swap_hi: val = 63488 (0xF800) + val << 8 = 16252928; (uint16_t)(16252928) = 0 + correct result: 248 | 0 = 248 (safe). + CodeHawk computes: 248 | 16252928 = 16253176 > 65535 -> violation. + + (b) byte_swap_mid: val = 2016 (0x07E0) + val << 8 = 516096; (uint16_t)(516096) = 57344 + correct result: 7 | 57344 = 57351 (safe). + CodeHawk computes: 7 | 516096 = 516103 > 65535 -> violation. + + (c) byte_swap_lo: val = 31 (0x001F) + val << 8 = 7936; (uint16_t)(7936) = 7936 (no truncation needed) + correct result: 0 | 7936 = 7936 (safe). + CodeHawk computes: 0 | 7936 = 7936 <= 65535 -> correctly safe. + + Recommended fix: in the abstract domain's evaluation of caste(uint16_t, X), + when the abstract value of X has an upper bound exceeding 65535, intersect + the result with [0, 65535] (modular-reduction semantics for unsigned casts). + After this fix all three cases should be discharged as safe. + + Observed as 2 violations in bmp_write_palette() in github_envyen_libbmp. +*/ + +#include + +/* (a) val << 8 overflows uint16_t -- intermediate truncation discards high bits */ +uint16_t byte_swap_hi(void) +{ + uint16_t val = 63488; /* 0xF800 */ + return (uint16_t)((uint16_t)((uint16_t)(val) >> 8) | + (uint16_t)((uint16_t)(val) << 8)); +} + +/* (b) val << 8 overflows uint16_t -- intermediate truncation keeps low bits */ +uint16_t byte_swap_mid(void) +{ + uint16_t val = 2016; /* 0x07E0 */ + return (uint16_t)((uint16_t)((uint16_t)(val) >> 8) | + (uint16_t)((uint16_t)(val) << 8)); +} + +/* (c) val << 8 fits in uint16_t -- no truncation, correctly proved safe */ +uint16_t byte_swap_lo(void) +{ + uint16_t val = 31; /* 0x001F */ + return (uint16_t)((uint16_t)((uint16_t)(val) >> 8) | + (uint16_t)((uint16_t)(val) << 8)); +} From 5051ade0da66bc2e1b7020598c4465ee88c03cbe Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 18 Jun 2026 17:29:27 -0700 Subject: [PATCH 2/3] PROOF: handle empty diagnostic invariant (Issue 70) --- chc/app/CHVersion.py | 2 +- chc/proof/CProofDiagnostic.py | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/chc/app/CHVersion.py b/chc/app/CHVersion.py index 95dda84..fbd8d61 100644 --- a/chc/app/CHVersion.py +++ b/chc/app/CHVersion.py @@ -1 +1 @@ -chcversion: str = "0.2.0-2026-06-06" +chcversion: str = "0.2.0-2026-06-18" diff --git a/chc/proof/CProofDiagnostic.py b/chc/proof/CProofDiagnostic.py index e238c5f..41f103e 100644 --- a/chc/proof/CProofDiagnostic.py +++ b/chc/proof/CProofDiagnostic.py @@ -130,7 +130,10 @@ def invsmap(self) -> Dict[int, List[int]]: for n in inode.findall("arg"): xargindex = n.get("a") xarginvs = n.get("i") - if xargindex is not None and xarginvs is not None: + if ( + xargindex is not None + and xarginvs is not None + and not (xarginvs == '')): self._invsmap[int(xargindex)] = [ int(x) for x in xarginvs.split(",")] return self._invsmap From 6869b44cfbd28bba4294541c3f20c2b60fcf236c Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 18 Jun 2026 22:02:24 -0700 Subject: [PATCH 3/3] KENDRA: update POs for change in Mod --- tests/kendra/id259Q/id259Q.json | 326 +++--- tests/kendra/id279Q/id279Q.json | 33 + tests/kendra/id311Q/id311Q.json | 1764 ++++++++++++++++--------------- 3 files changed, 1110 insertions(+), 1013 deletions(-) diff --git a/tests/kendra/id259Q/id259Q.json b/tests/kendra/id259Q/id259Q.json index 9a73d7a..7069ba1 100644 --- a/tests/kendra/id259Q/id259Q.json +++ b/tests/kendra/id259Q/id259Q.json @@ -3,234 +3,266 @@ "id259.c": { "domains": [ "llvis" - ], + ], "functions": { "main": { "ppos": [ { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-lower-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-upper-bound", - "status": "violation", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-upper-bound", + "status": "violation", "tgtstatus": "violation" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "2op:2_index_var_lhs", - "line": 58, - "predicate": "initialized", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_index_var_lhs", + "line": 58, + "predicate": "initialized", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "2op:2_index_var_lhs", - "line": 58, - "predicate": "not-zero", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_index_var_lhs", + "line": 58, + "predicate": "not-zero", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-lb", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-ub", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-ub", + "status": "safe", "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:1_stmt:1", + "expctxt": "index_var_lhs", + "line": 58, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" } ] } } - }, + }, "id260.c": { "domains": [ "llvis" - ], + ], "functions": { "main": { "ppos": [ { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-lower-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-upper-bound", - "status": "violation", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-upper-bound", + "status": "violation", "tgtstatus": "violation" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "2op:2_index_var_lhs", - "line": 58, - "predicate": "initialized", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_index_var_lhs", + "line": 58, + "predicate": "initialized", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "2op:2_index_var_lhs", - "line": 58, - "predicate": "not-zero", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_index_var_lhs", + "line": 58, + "predicate": "not-zero", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-lb", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-ub", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-ub", + "status": "safe", "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:1_stmt:1", + "expctxt": "index_var_lhs", + "line": 58, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" } ] } } - }, + }, "id261.c": { "domains": [ "llvis" - ], + ], "functions": { "main": { "ppos": [ { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-lower-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-upper-bound", - "status": "violation", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-upper-bound", + "status": "violation", "tgtstatus": "violation" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "2op:2_index_var_lhs", - "line": 58, - "predicate": "initialized", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_index_var_lhs", + "line": 58, + "predicate": "initialized", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "2op:2_index_var_lhs", - "line": 58, - "predicate": "not-zero", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_index_var_lhs", + "line": 58, + "predicate": "not-zero", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-lb", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-ub", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-ub", + "status": "safe", "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:1_stmt:1", + "expctxt": "index_var_lhs", + "line": 58, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" } ] } } - }, + }, "id262.c": { "domains": [ "llvis" - ], + ], "functions": { "main": { "ppos": [ { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-lower-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-upper-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "2op:2_index_var_lhs", - "line": 58, - "predicate": "initialized", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_index_var_lhs", + "line": 58, + "predicate": "initialized", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "2op:2_index_var_lhs", - "line": 58, - "predicate": "not-zero", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_index_var_lhs", + "line": 58, + "predicate": "not-zero", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-lb", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-ub", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-ub", + "status": "safe", "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:1_stmt:1", + "expctxt": "index_var_lhs", + "line": 58, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" } ] } diff --git a/tests/kendra/id279Q/id279Q.json b/tests/kendra/id279Q/id279Q.json index 7ecd833..4c57ed4 100644 --- a/tests/kendra/id279Q/id279Q.json +++ b/tests/kendra/id279Q/id279Q.json @@ -190,7 +190,16 @@ "predicate": "signed-to-signed-cast-ub", "status": "safe", "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_2op:1_mem_lhs", + "line": 58, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" } + ] } } @@ -385,6 +394,14 @@ "predicate": "signed-to-signed-cast-ub", "status": "safe", "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_2op:1_mem_lhs", + "line": 58, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" } ] } @@ -580,6 +597,14 @@ "predicate": "signed-to-signed-cast-ub", "status": "safe", "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_2op:1_mem_lhs", + "line": 58, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" } ] } @@ -775,6 +800,14 @@ "predicate": "signed-to-signed-cast-ub", "status": "safe", "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:1_stmt:1", + "expctxt": "2op:2_2op:1_mem_lhs", + "line": 58, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" } ] } diff --git a/tests/kendra/id311Q/id311Q.json b/tests/kendra/id311Q/id311Q.json index 56b0e5f..0d363f1 100644 --- a/tests/kendra/id311Q/id311Q.json +++ b/tests/kendra/id311Q/id311Q.json @@ -3,1104 +3,1136 @@ "id311.c": { "domains": [ "llvis" - ], + ], "functions": { "main": { "ppos": [ { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "not-null", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "not-null", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "ptr-upper-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "ptr-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "pointer-cast", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "pointer-cast", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "valid-mem", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "valid-mem", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "lower-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "upper-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:3", - "line": 57, - "predicate": "signed-to-unsigned-cast-lb", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:3", + "line": 57, + "predicate": "signed-to-unsigned-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:3", - "line": 57, - "predicate": "signed-to-unsigned-cast-ub", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:3", + "line": 57, + "predicate": "signed-to-unsigned-cast-ub", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-lower-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-upper-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-lb", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-ub", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-ub", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "args:1_2", - "line": 62, - "predicate": "no-overlap", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "args:1_2", + "line": 62, + "predicate": "no-overlap", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "not-null", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "not-null", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "ptr-upper-bound", - "status": "violation", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "ptr-upper-bound", + "status": "violation", "tgtstatus": "violation" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "not-null", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "not-null", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "ptr-upper-bound", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "ptr-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "initialized-range", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "initialized-range", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "pointer-cast", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "pointer-cast", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "valid-mem", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "valid-mem", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "lower-bound", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "upper-bound", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "upper-bound", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "pointer-cast", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "valid-mem", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "lower-bound", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "upper-bound", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:3", + "line": 62, + "predicate": "signed-to-unsigned-cast-lb", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:3", + "line": 62, + "predicate": "signed-to-unsigned-cast-ub", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "pointer-cast", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "2op:2_cast_arg:3", + "line": 62, + "predicate": "initialized", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "valid-mem", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "2op:2_cast_arg:3", + "line": 62, + "predicate": "not-zero", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "lower-bound", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "in-scope", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "upper-bound", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "in-scope", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:3", - "line": 62, - "predicate": "signed-to-unsigned-cast-lb", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:3", - "line": 62, - "predicate": "signed-to-unsigned-cast-ub", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "in-scope", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "2op:2_cast_arg:3", - "line": 62, - "predicate": "initialized", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "2op:2_cast_arg:3", - "line": 62, - "predicate": "not-zero", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "in-scope", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "in-scope", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "in-scope", - "status": "safe", - "tgtstatus": "safe" + "cfgctxt": "instr:3_stmt:1", + "expctxt": "cast_arg:3", + "line": 62, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" } ] } } - }, + }, "id312.c": { "domains": [ "llvis" - ], + ], "functions": { "main": { "ppos": [ { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "not-null", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "not-null", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "ptr-upper-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "ptr-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "pointer-cast", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "pointer-cast", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "valid-mem", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "valid-mem", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "lower-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "upper-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:3", - "line": 57, - "predicate": "signed-to-unsigned-cast-lb", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:3", + "line": 57, + "predicate": "signed-to-unsigned-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:3", - "line": 57, - "predicate": "signed-to-unsigned-cast-ub", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:3", + "line": 57, + "predicate": "signed-to-unsigned-cast-ub", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-lower-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-upper-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-lb", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-ub", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-ub", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "args:1_2", - "line": 62, - "predicate": "no-overlap", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "args:1_2", + "line": 62, + "predicate": "no-overlap", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "not-null", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "not-null", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "ptr-upper-bound", - "status": "violation", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "ptr-upper-bound", + "status": "violation", "tgtstatus": "violation" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "not-null", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "not-null", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "ptr-upper-bound", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "ptr-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "initialized-range", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "initialized-range", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "pointer-cast", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "pointer-cast", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "valid-mem", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "valid-mem", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "lower-bound", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "upper-bound", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "pointer-cast", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "valid-mem", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "lower-bound", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "upper-bound", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "lower-bound", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "upper-bound", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "pointer-cast", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "valid-mem", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "lower-bound", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "upper-bound", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:3", + "line": 62, + "predicate": "signed-to-unsigned-cast-lb", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:3", + "line": 62, + "predicate": "signed-to-unsigned-cast-ub", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:3", - "line": 62, - "predicate": "signed-to-unsigned-cast-lb", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "2op:2_cast_arg:3", + "line": 62, + "predicate": "initialized", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:3", - "line": 62, - "predicate": "signed-to-unsigned-cast-ub", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "2op:2_cast_arg:3", + "line": 62, + "predicate": "not-zero", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "2op:2_cast_arg:3", - "line": 62, - "predicate": "initialized", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "in-scope", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "2op:2_cast_arg:3", - "line": 62, - "predicate": "not-zero", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "in-scope", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "in-scope", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "cast_arg:3", + "line": 62, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "in-scope", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "in-scope", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "in-scope", + "status": "safe", "tgtstatus": "safe" } ] } } - }, + }, "id313.c": { "domains": [ "llvis" - ], + ], "functions": { "main": { "ppos": [ { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "not-null", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "not-null", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "ptr-upper-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "ptr-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "pointer-cast", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "pointer-cast", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "valid-mem", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "valid-mem", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "lower-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "upper-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:3", - "line": 57, - "predicate": "signed-to-unsigned-cast-lb", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:3", + "line": 57, + "predicate": "signed-to-unsigned-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:3", - "line": 57, - "predicate": "signed-to-unsigned-cast-ub", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:3", + "line": 57, + "predicate": "signed-to-unsigned-cast-ub", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-lower-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-upper-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-lb", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-ub", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-ub", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "args:1_2", - "line": 62, - "predicate": "no-overlap", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "args:1_2", + "line": 62, + "predicate": "no-overlap", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "not-null", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "not-null", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "ptr-upper-bound", - "status": "violation", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "ptr-upper-bound", + "status": "violation", "tgtstatus": "violation" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "not-null", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "ptr-upper-bound", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "initialized-range", - "status": "safe", - "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "pointer-cast", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "not-null", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "valid-mem", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "ptr-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "lower-bound", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "initialized-range", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "upper-bound", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "pointer-cast", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "pointer-cast", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "valid-mem", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "valid-mem", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "lower-bound", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "upper-bound", - "status": "safe", - "tgtstatus": "safe" - }, - { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:3", - "line": 62, - "predicate": "signed-to-unsigned-cast-lb", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "upper-bound", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "pointer-cast", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "valid-mem", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "lower-bound", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "upper-bound", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:3", + "line": 62, + "predicate": "signed-to-unsigned-cast-lb", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:3", + "line": 62, + "predicate": "signed-to-unsigned-cast-ub", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:3", - "line": 62, - "predicate": "signed-to-unsigned-cast-ub", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "2op:2_cast_arg:3", + "line": 62, + "predicate": "initialized", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "2op:2_cast_arg:3", - "line": 62, - "predicate": "initialized", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "2op:2_cast_arg:3", + "line": 62, + "predicate": "not-zero", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "2op:2_cast_arg:3", - "line": 62, - "predicate": "not-zero", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "in-scope", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "in-scope", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "in-scope", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "in-scope", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "in-scope", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "in-scope", - "status": "safe", - "tgtstatus": "safe" + "cfgctxt": "instr:3_stmt:1", + "expctxt": "cast_arg:3", + "line": 62, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" } ] } } - }, + }, "id314.c": { "domains": [ "llvis" - ], + ], "functions": { "main": { "ppos": [ { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "not-null", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "not-null", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "ptr-upper-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "ptr-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "pointer-cast", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "pointer-cast", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "valid-mem", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "valid-mem", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "lower-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "upper-bound", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:3", - "line": 57, - "predicate": "signed-to-unsigned-cast-lb", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:3", + "line": 57, + "predicate": "signed-to-unsigned-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:3", - "line": 57, - "predicate": "signed-to-unsigned-cast-ub", - "status": "safe", + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:3", + "line": 57, + "predicate": "signed-to-unsigned-cast-ub", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-lower-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "var_lhs", - "line": 58, - "predicate": "index-upper-bound", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "var_lhs", + "line": 58, + "predicate": "index-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-lb", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-lb", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:1_stmt:1", - "expctxt": "rhs", - "line": 58, - "predicate": "signed-to-signed-cast-ub", - "status": "safe", + "cfgctxt": "instr:1_stmt:1", + "expctxt": "rhs", + "line": 58, + "predicate": "signed-to-signed-cast-ub", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "args:1_2", - "line": 62, - "predicate": "no-overlap", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "args:1_2", + "line": 62, + "predicate": "no-overlap", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "not-null", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "not-null", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "ptr-upper-bound", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "ptr-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "not-null", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "not-null", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "ptr-upper-bound", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "ptr-upper-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "initialized-range", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "initialized-range", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "pointer-cast", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "pointer-cast", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "valid-mem", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "valid-mem", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "lower-bound", - "status": "safe", + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "lower-bound", + "status": "safe", "tgtstatus": "safe" - }, + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "upper-bound", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "upper-bound", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "pointer-cast", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "pointer-cast", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "valid-mem", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "valid-mem", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "lower-bound", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "lower-bound", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "upper-bound", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "upper-bound", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:3", - "line": 62, - "predicate": "signed-to-unsigned-cast-lb", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:3", + "line": 62, + "predicate": "signed-to-unsigned-cast-lb", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:3", - "line": 62, - "predicate": "signed-to-unsigned-cast-ub", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:3", + "line": 62, + "predicate": "signed-to-unsigned-cast-ub", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "2op:2_cast_arg:3", - "line": 62, - "predicate": "initialized", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "2op:2_cast_arg:3", + "line": 62, + "predicate": "initialized", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "2op:2_cast_arg:3", - "line": 62, - "predicate": "not-zero", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "2op:2_cast_arg:3", + "line": 62, + "predicate": "not-zero", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:0_stmt:1", - "expctxt": "arg:1", - "line": 57, - "predicate": "in-scope", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:0_stmt:1", + "expctxt": "arg:1", + "line": 57, + "predicate": "in-scope", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:1", - "line": 62, - "predicate": "in-scope", - "status": "safe", - "tgtstatus": "safe" - }, + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:1", + "line": 62, + "predicate": "in-scope", + "status": "safe", + "tgtstatus": "safe" + }, { - "cfgctxt": "instr:3_stmt:1", - "expctxt": "arg:2", - "line": 62, - "predicate": "in-scope", - "status": "safe", - "tgtstatus": "safe" + "cfgctxt": "instr:3_stmt:1", + "expctxt": "arg:2", + "line": 62, + "predicate": "in-scope", + "status": "safe", + "tgtstatus": "safe" + }, + { + "cfgctxt": "instr:3_stmt:1", + "expctxt": "cast_arg:3", + "line": 62, + "predicate": "int-overflow", + "status": "open", + "tgtstatus": "open" } ] } } } - }, + }, "restrictions": [ "linux-only" ]