Nischoy — zlib Verification Results

Adler32 Length Bounds

🌳 tree-sitter VERIFIED

Function: adler32_combine_ · Z3 solved in 0.1ms

adler32_combine_() requires len2 ≥ 0. Extracted from adler32.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun len2 () Int)
(assert
 (>= len2 0))
(assert
 (< len2 0))
(check-sat)

CRC32 Combine Length Bounds

🌳 tree-sitter VERIFIED

Function: crc32_combine_gen64 · Z3 solved in 0.0ms

crc32_combine_gen64() requires len2 ≥ 0. Extracted from crc32.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun len2 () Int)
(assert
 (>= len2 0))
(assert
 (< len2 0))
(check-sat)

Deflate Window Bits Bounds (8-15)

🌳 tree-sitter VERIFIED

Function: deflateInit2_ · Z3 solved in 0.0ms

deflateInit2_() windowBits must be 8-15 after normalization. Code accepts raw -1..-15 (negated to 1..15) and gzip 16..31 (subtract 16). Extracted from deflate.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun windowBits () Int)
(assert
 (<= windowBits 15))
(assert
 (>= windowBits 8))
(assert
 (or (< windowBits 8) (> windowBits 15)))
(check-sat)

Deflate Memory Level Bounds (1-9)

🌳 tree-sitter VERIFIED

Function: deflateInit2_ · Z3 solved in 0.0ms

deflateInit2_() memLevel must be 1-MAX_MEM_LEVEL(9). Extracted from deflate.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun memLevel () Int)
(assert
 (<= memLevel 9))
(assert
 (>= memLevel 1))
(assert
 (or (< memLevel 1) (> memLevel 9)))
(check-sat)

Deflate Compression Level Bounds (0-9)

🌳 tree-sitter VERIFIED

Function: deflateInit2_ · Z3 solved in 0.0ms

deflateInit2_() compression level must be 0-9 (with Z_DEFAULT_COMPRESSION normalized to 6). Extracted from deflate.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun level () Int)
(assert
 (<= level 9))
(assert
 (>= level 0))
(assert
 (or (< level 0) (> level 9)))
(check-sat)

Deflate Method Allowed Set {8}

🌳 tree-sitter VERIFIED

Function: deflateInit2_ · Z3 solved in 0.0ms

deflateInit2_() only accepts method Z_DEFLATED(8), preventing unsupported algorithm selection.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun method () Int)
(assert
 (let (($x8 (= method 8)))
 (or $x8)))
(assert
 (let (($x8 (= method 8)))
(not $x8)))
(check-sat)

DeflateParams Compression Level Bounds (0-9)

🌳 tree-sitter VERIFIED

Function: deflateParams · Z3 solved in 0.0ms

deflateParams() compression level must be 0-9 after Z_DEFAULT_COMPRESSION normalization, preventing invalid configuration_table indexing.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun level () Int)
(assert
 (<= level 9))
(assert
 (>= level 0))
(assert
 (or (< level 0) (> level 9)))
(check-sat)

DeflateParams Strategy Bounds (0-4)

🌳 tree-sitter VERIFIED

Function: deflateParams · Z3 solved in 0.0ms

deflateParams() strategy must be in zlib enum range 0..4 (Z_DEFAULT_STRATEGY..Z_FIXED), preventing invalid mode switches during live stream reconfiguration.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun strategy () Int)
(assert
 (<= strategy 4))
(assert
 (>= strategy 0))
(assert
 (or (< strategy 0) (> strategy 4)))
(check-sat)

Deflate Strategy Bounds (0-4)

🌳 tree-sitter VERIFIED

Function: deflateInit2_ · Z3 solved in 0.0ms

deflateInit2_() strategy must be in zlib enum range 0..4 (Z_DEFAULT_STRATEGY..Z_FIXED). Extracted from deflate.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun strategy () Int)
(assert
 (<= strategy 4))
(assert
 (>= strategy 0))
(assert
 (or (< strategy 0) (> strategy 4)))
(check-sat)

Deflate Flush Mode Bounds (0-5)

🌳 tree-sitter VERIFIED

Function: deflate · Z3 solved in 0.0ms

deflate() rejects flush outside [0,Z_BLOCK(5)], preventing invalid flush-state transitions and stream-state corruption paths.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun flush () Int)
(assert
 (<= flush 5))
(assert
 (>= flush 0))
(assert
 (or (< flush 0) (> flush 5)))
(check-sat)

Inflate Window Bits Bounds (8-15)

🌳 tree-sitter VERIFIED

Function: inflateReset2 · Z3 solved in 0.0ms

inflateReset2() windowBits must be 8-15 after normalization. Code accepts raw -1..-15 (negated) and gzip 16..31 (subtract 16). Extracted from inflate.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun windowBits () Int)
(assert
 (<= windowBits 15))
(assert
 (>= windowBits 8))
(assert
 (or (< windowBits 8) (> windowBits 15)))
(check-sat)

InflateValidate Check Flag Bounds (0-1)

📋 stub VERIFIED

Function: inflateValidate · Z3 solved in 0.0ms

inflateValidate() check flag is modeled as boolean-like 0/1 to keep checksum-mode transitions in a predictable domain.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun check () Int)
(assert
 (<= check 1))
(assert
 (>= check 0))
(assert
 (or (< check 0) (> check 1)))
(check-sat)

Deflate Dictionary Length Bounds (0-32768)

🌳 tree-sitter (partial) VERIFIED

Function: deflateSetDictionary · Z3 solved in 0.0ms

deflateSetDictionary() dictLength ≤ window size (32768 for MAX_WBITS=15). Extracted from deflate.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun dictLength () Int)
(assert
 (<= dictLength 32768))
(assert
 (>= dictLength 0))
(assert
 (or (< dictLength 0) (> dictLength 32768)))
(check-sat)

CompressBound No Overflow

🌳 tree-sitter VERIFIED

Function: compressBound · Z3 solved in 0.4ms

compressBound output must not wrap around for valid input. Extracted from compress.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun sourceLen () Int)
(assert
 (let ((?x7 (div sourceLen 33554432)))
(let ((?x32 (+ (+ (+ sourceLen (div sourceLen 4096)) (div sourceLen 16384)) ?x7)))
(let (($x21 (<= sourceLen 18446744073709551615)))
(let (($x22 (>= sourceLen 0)))
(and $x22 $x21 (< (+ ?x32 13) sourceLen)))))))
(check-sat)

Deflate Dictionary Length Fits uint16

🌳 tree-sitter (partial) VERIFIED

Function: deflateSetDictionary · Z3 solved in 0.0ms

deflateSetDictionary() dictLength must fit in uint16-sized copy counters.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun dictLength () Int)
(assert
 (<= dictLength 65535))
(assert
 (>= dictLength 0))
(assert
 (or (< dictLength 0) (> dictLength 65535)))
(check-sat)

DeflatePrime Bit Count Bounds (0-16)

🌳 tree-sitter VERIFIED

Function: deflatePrime · Z3 solved in 0.0ms

deflatePrime() enforces bits in [0,16] before priming the bit buffer, preventing invalid bit-count writes.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun bits () Int)
(assert
 (<= bits 16))
(assert
 (>= bits 0))
(assert
 (or (< bits 0) (> bits 16)))
(check-sat)

InflatePrime Bit Count Bounds (0-16)

🌳 tree-sitter VERIFIED

Function: inflatePrime · Z3 solved in 0.0ms

inflatePrime() enforces bits in [0,16] before bit-buffer priming, preventing invalid bit-count writes.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun bits () Int)
(assert
 (<= bits 16))
(assert
 (>= bits 0))
(assert
 (or (< bits 0) (> bits 16)))
(check-sat)

InflatePrime Total Bit Buffer Bounds (0-32)

🌳 tree-sitter (partial) VERIFIED

Function: inflatePrime · Z3 solved in 0.0ms

inflatePrime() rejects state->bits + (uInt)bits > 32, bounding aggregate bit-buffer occupancy to 32 bits and preventing hold-register overflow.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun total_bits () Int)
(assert
 (<= total_bits 32))
(assert
 (>= total_bits 0))
(assert
 (or (< total_bits 0) (> total_bits 32)))
(check-sat)