zError
返回 zlib 结果码对应的文本。
完整章节与共同规则 ↗767fa1407a7fe3d1 · 对应提交的原文 ↗先看本函数的前置条件和返回结果；可展开下方共同规则，查看整组接口的缓冲区与所有权要求。
const char * ZEXPORT zError(int err);
返回 zlib 结果码对应的文本。
定义域 完整类型定义域。
前置条件 完整类型定义域：每个 int，包括最小和最大值。
返回与保证 返回非 NULL 指针，指向下列以 NUL 结尾的文本。
err |
返回的原始文本 | 中文含义 |
|---|---|---|
| 2 | need dictionary |
需要预置字典 |
| 1 | stream end |
流已结束 |
| -1 | file error |
文件错误 |
| -2 | stream error |
流状态或参数错误 |
| -3 | data error |
数据格式或完整性错误 |
| -4 | insufficient memory |
内存不足 |
| -5 | buffer error |
缓冲区条件不足 |
| -6 | incompatible version |
版本不兼容 |
| 0 或任意其他值 | 空字符串 | 无诊断文本 |
内存与状态效果 只读。结果是借用的不可变静态存储；不得写入或释放。 没有分配、堆变化或错误返回。索引计算前会检查 -6–2 范围外的值， 因此两个标量极值均安全返回空文本。
本组共同前提与范围
调用时已知完整输入和输出容量，可使用缓冲区工具。它们在内部管理临时流。 需要增量 I/O、其他包装、字典或显式刷新边界时，应使用流式接口页面。
| 任务 | 入口 |
|---|---|
| 压缩缓冲区 | 选择级别、默认级别、确定目标容量 |
| 解压缓冲区 | 报告已消费输入、仅报告输出 |
| 查询库信息 | 版本、编译标志、错误文本 |
这些聚焦契约对应默认 LP64 Linux 构建中的 compress.c、uncompr.c、zutil.c 和
zlib.h。_z 形式使用 z_size_t；普通形式使用 uLong。这里两者均为 64 位。
本页契约不会缩小
Utilities.lean 和
Queries.lean 中登记的目标。
Calls.lean 固定翻译后的参数和结果。
定义域和效果标签见契约约定；证明状态和剩余工作见进度。
超出聚焦前提只表示本契约不作保证，不自动等于 C 未定义行为（UB），也不保证一定返回错误码。
缓冲区工具使用 zlib 包装和默认设置，创建并释放一个局部流。
先看输入／输出长度的约定：sourceLen 指定可读输入的字节数；*destLen 在调用前是目标数组的可写容量，调用后改为实际写入量。例如目标有 1000 字节容量、最终写入 120 字节，调用前应设置 *destLen = 1000，成功返回后读取到 120。这个长度单元自身也是需要保持存活、可读写的调用者存储。uncompress2_z 的 *sourceLen 同样在调用前给出输入容量，返回后报告已消费量。
查询上界的函数只计算一个数，并不替调用者分配目标数组。
flowchart LR
B["compressBound"] --> C["compress / compress2"]
C --> Z["zlib 流"] --> U["uncompress / uncompress2"]
U --> D["解码字节"]
通用约定
缓冲区调用的定义域限于有效内存：非 NULL 源覆盖指定的可读输入； 非 NULL 目标覆盖指定的可写容量。非 NULL 长度指针指向可读写的标量单元。 输入、输出和长度单元互相分离，包括同时出现的两个长度单元。 调用期间，调用者保持这些对象存活且不修改它们。 各入口分别说明允许的 NULL 情形。其他无效指针不在此范围内。 处理解压错误不要求压缩数据有效。
通用效果。 每个范围内调用都终止且不产生故障。 缓冲区调用保持输入以及输出、长度单元以外的内存不变，写入不超过原始容量。 返回前释放所有内部分配，包括分配失败路径；不返回局部流或其拥有的分配。 返回指针的查询交付借用的不可变存储。 这些要求适用于每一条所述返回路径，包括分配失败和部分输出之后的清理。
形式化约定
ZlibF.Spec.Public.Goal.zError
证明状态：已登记证明 · 证明记录与剩余工作
/-- `const char *zError(int err)`.
Every signed argument returns the public error text as static read-only storage.
Every heap is unchanged; no allocation, leak or runtime fault is permitted. -/
def Goal.zError : Prop :=
∀ (h : Heap) (err : Int32), ∃ p,
C.run (Zlib.Zutil.zError err) h = .ok (p, h) ∧ StaticString h p (errorText err.toInt)