跳到正文
参考文档 / ZLIB × LEAN

gzopen64

通过大文件入口打开。

完整章节与共同规则 ↗
此页源文件快照 · 2425ced89b926581 · 对应提交的原文 ↗

先看本函数的前置条件和返回结果;可展开下方共同规则,查看整组接口的缓冲区与所有权要求。

通过大文件入口打开。

gzFile ZEXPORT gzopen64(const char *path, const char *mode);

定义域 与 gzopen 相同的受限定义域。效果: 有状态打开。

前置条件 满足 gzopen 的字符串和环境要求。

返回与保证 适用 gzopen 契约,包括所有权、延迟分配和初始位置。 在此构建中,其实现和偏移范围均相同。

错误与边缘情形: 适用相同的 NULL、无效模式、分配和系统失败情形。 若构建的公开头文件对它设置条件,此名称需要相应的大文件声明。

本组共同前提与范围

API 手册 · 契约约定 · 流式压缩 · 流式解压

使用 gzFile 句柄进行带缓冲的 gzip 文件 I/O。打开时取得文件描述符和私有状态; 数据操作按需初始化缓冲区和编解码器状态;即使最终 I/O 失败,关闭也会释放句柄。 读取还可接受透明的未压缩输入:文件中的字节不经解压,直接作为结果交付。

任务 入口
打开或配置 打开路径、打开描述符、缓冲区大小、压缩参数
读取 字节、数据项、字符、回退字节、行
写入 字节、数据项、字符、字符串、格式化文本、刷新
位置 定位、回到起点、未压缩位置、文件偏移
查询或清除状态 文件末尾、透明模式、错误、清除错误
关闭 任意模式、读取句柄、写入句柄

本页按固定版本源码和 zlib.h 组织接口契约。各条目明确列出调用范围, 对应的完整执行要求见已登记公开目标,当前证据见进度。 超出聚焦前提只表示本契约不作保证,不自动等于 C 未定义行为(UB),也不保证一定返回错误码。

通用句柄条件

先分清两种位置。逻辑位置以未压缩字节计数;普通读写按已消费或接受的数量推进,定位还可以登记尚未执行的前移。底层文件另有物理偏移,它以文件中的字节计数。gztell 查询前者,gzoffset 查询后者。库会预读和缓冲,因此两个值通常不同;单次压缩率也不能用来换算它们。

例如,没有额外定位或字节回退时,读取句柄已向应用交付 1000 个解压字节,逻辑位置就是 1000;为了完成这些输出,底层可能已预读更靠后的压缩字节。相反,写入成功表示库接受了输入,不能据此推断这些字节已全部写入描述符。

后面的参数沿用这套单位:len 和缓冲区配置 size 按字节计;数据项接口中的 size 是每项字节数,nitems 是项数,总请求为 size * nitems 字节。offset 是有符号的未压缩字节位移;whence 指定从起点(SEEK_SET)还是当前位置(SEEK_CUR)计算。INT_MAX 是本构建中有符号 int 能表示的最大值,即 2^31 - 1。

本页把可直接重试的非阻塞停顿与其他已记录的“硬错误”分开描述。这个区别说明本次调用怎样返回;它不免除错误后的状态、重试和清理要求。

本页使用默认 x86_64 Linux 构建。int 和 unsigned 为 32 位。 long、z_off_t、z_off64_t 和 z_size_t 为 64 位。大文件声明已启用。 这里普通入口和 *64 入口的偏移范围相同。其他配置需要单独契约。 gzopen_w 仅适用于 Windows,下文另行限定其范围。

受限定义域指满足下列通用要求的普通用法:

  • 非 NULL 句柄由成功打开返回、仍存活且尚未关闭。串行使用它,调用者不修改其私有状态。
  • 读取或写入句柄具有入口指定的访问模式。NULL 和错误模式的拒绝情形分别说明。 已失效或任意指针不在本定义域内;检查模式字段不等于验证指针。
  • 缓冲区覆盖请求的可读或可写范围,并与句柄拥有的内存分离。 字符串具有可读的终止 NUL。调用者保留这些对象的所有权。
  • 位置运算和请求范围能由指定 C 类型表示。下述契约仍包括显式的超大请求和乘法溢出拒绝。
  • 描述符在关闭前属于句柄。调用期间,没有其他操作改变其数据或位置。 操作系统失败和分配失败仍可能发生;成功打开不保证后续 I/O 成功。

每个入口均带定义域标签。“完整标量范围”仅在上述指针和生存期要求下, 适用于所指明的标量参数。文档中的限制不免除已知失败路径的义务。 特别地,部分读取错误和字节回退形成的负位置仍属于未改变的公开目标。

效果。 读、写、打开、定位、控制和关闭均为有状态操作,包括没有调用者输出缓冲区的操作。 位置查询(gztell、gzoffset)和文件末尾查询(gzeof)读取状态;gzerror 还可能写入可选错误码输出。 gzdirect 可读取文件并分配内存,因此也是有状态操作。

stateDiagram-v2
    state "新建句柄" as Fresh
    state "已开始数据处理" as Active
    state "已关闭" as Closed
    [*] --> Fresh: 成功打开
    Fresh --> Active: 首次 I/O 或格式检查
    Active --> Active: 读、写、定位、控制
    Fresh --> Closed: 关闭
    Active --> Closed: 关闭,包括最终 I/O 失败
    Closed --> [*]

格式与缓冲。 打开时不对载荷执行 I/O。缓冲区和编解码器状态按需分配, 默认请求的缓冲区大小为 8192 字节。请求大小是配置量,实际内部存储还包括下述双倍缓冲区和编解码器状态。首次使用或后续解压期间都可能分配失败。 即使最终 I/O 失败,关闭也释放拥有的分配。

普通读取句柄根据合理的四字节头部识别 gzip;否则原样返回输入。 空输入属于透明输入。非阻塞输入在获得四字节前停顿时,检测保持等待。 一个 gzip 成员是一段带有自身头部、压缩数据和尾部校验信息的完整流;一个文件可以顺序放置多个成员。读取输出按顺序拼接各成员的未压缩数据。若尝试解码下一个成员时,在格式错误前未产生输出, 则忽略尾随的非成员数据。G 要求 gzip;T 选择透明输出,不能用于读取。

读取结果。 读取按已消费字节数推进未压缩位置,包括最终的部分数据项。 已缓冲字节可能在已记录错误被报告之前返回。gzeof 表示曾尝试读取可用数据之后的内容, 而不只是已交付最后一个字节。gzerror 区分 EOF、损坏(Z_DATA_ERROR)、 截断(Z_BUF_ERROR)、分配失败(Z_MEM_ERROR)和系统失败(Z_ERRNO)。 零长度读取不消费输入,也不执行待处理定位。

写入结果。 成功表示句柄已接受输入;数据仍可能在缓冲区内。 后续刷新或关闭仍可能失败。硬错误可能在消费一个前缀后返回失败; 仅凭返回值不总能确定重试偏移。非阻塞停顿则可能返回至今已消费的数量。

错误通常持续到被清除。已记录的非阻塞停顿允许下次数据 I/O 重试。 定位和回到起点仍拒绝该已记录的 Z_ERRNO。构造错误消息本身可能失败, 并将错误码改为 Z_MEM_ERROR。errno 只对关联的系统失败有意义, 不能普遍解释每个失败的 API 调用。

源码为 gzlib.c、gzread.c、 gzwrite.c、gzclose.c 和 zlib.h。抽象契约位于 Api/Gz.lean。 具体目标位于 GzOpen、 GzRead、GzWrite、 GzControl 和 GzClose。翻译在 ZlibF/Zlib/ 中保留 C 名称。

形式化约定

ZlibF.Spec.Public.Goal.gzopen64

证明状态:未完成 · 证明记录与剩余工作

/-- `gzFile gzopen64(const char *path, const char *mode)`.
The LP64 entry uses the same open flags and position range as `gzopen`. -/
def Goal.gzopen64 : Prop := OpenContract Zlib.Gzlib.gzopen64
相关定义与源码 ↗
ZLIB × LEAN

全局目录

当前位置gzopen64