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

deflateEnd

释放压缩器,丢弃任何未完成工作。

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

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

int ZEXPORT deflateEnd(z_streamp strm);

释放压缩器,丢弃任何未完成工作。

定义域 受限定义域。影响: 释放拥有的状态。

前置条件 任意阶段的有效流,默认释放例程保持完整。

返回与保证 对全部五项拥有的分配恰好释放一次,并将 state 置为 NULL。调用者输入/输出及头部存储不变,仍归调用者所有。保存的状态为尚未完成普通压缩的 BUSY_STATE 时返回 Z_DATA_ERROR,否则返回 Z_OK。两种结果都释放全部资源:Z_DATA_ERROR 报告未完成压缩,不表示清理失败。重新初始化前,后续压缩调用均无效。

聚焦范围之外: 流检查失败,包括第二次结束,返回 Z_STREAM_ERROR,不释放任何内容。返回状态取决于内部压缩阶段,而不只是是否已交付每个产生的字节。

本组共同前提与范围

API 手册 · 共享流规则 · 流式解压

输入分批到达、输出空间有限,或需要选择封装、字典、刷新边界时,使用 z_stream 压缩器。封装是在 DEFLATE 压缩数据之外增加的头部、尾部和完整性信息;raw DEFLATE 则不带这些封装。初始化一次,使用连续的缓冲区调用 deflate,即使放弃压缩也要结束流。单个缓冲区的操作见 compress 和 compress2。

任务 条目
开始或复用 初始化、配置初始化、重置、保留历史的重置
提供元数据或历史 字典、读取历史、gzip 头
压缩与输出大小 压缩、上界、待输出数据、最近刷新位数
调整或分支 参数、调优、位预置、复制
释放存储 结束

这些聚焦契约遵循固定版本的 deflate.c、已应用补丁和 zlib.h,采用默认 LP64 Linux 构建。它们不改变范围更广的已登记公开目标。定义域/影响标签见契约约定,证明状态和剩余工作见进度。

共享约定

在每条所述前置条件下,都要求执行无运行时故障地终止,并满足所述后置条件。调用若保留有效流,就保持其表示不变量。

先看一次调用的数据交接。next_in 指向本轮尚未读取的输入起点,avail_in 是从这里开始可读的字节数;next_out 指向本轮下一个可写位置,avail_out 是剩余输出容量,也以字节计。一次调用可以只消耗部分输入、只交付部分输出。调用者应读取更新后的指针和计数,接走已交付字节,再为同一个流补充输入或输出空间。

  • 有效流: 可写的 z_stream,其压缩器状态由成功初始化或复制建立,经过合法调用保持,且尚未结束。调用者不改变其内部状态或分配器字段。同一个流的调用按顺序执行。
  • 缓冲区: 输入覆盖 avail_in 个可读字节;输出覆盖 avail_out 个可写字节。它们彼此不重叠,也不与流或流拥有的状态重叠。非 NULL 标量结果指向可写单元,与其他结果及流内存分离。这些分离条件是聚焦契约的显式假设;见 safety.md。
  • 分配器: 使用默认分配/释放函数对,或在初始化前将两个字段都置为 NULL。任意一次分配尝试都可能失败。自定义分配器回调不在本页范围内。
  • 帧性质与所有权: 调用只改变自己的流、其拥有的状态和所述输出区域。调用者输入只读。调用者缓冲区和头部记录仍归调用者所有。只有初始化和复制会分配;只有它们失败时的清理与 deflateEnd 会释放内存。其他调用保持流的分配集合。
  • 头部生命周期: 保留的 gzip 头及其可选字段在使用期间保持可读且不变。非 NULL 的 name 和 comment 以零终止;extra 覆盖所述长度。聚焦格式契约使用 extra_len <= 65535。
  • 检查后的拒绝: 除初始化和上界查询外,流检查失败会在正常操作之前返回 Z_STREAM_ERROR,不发生写入。deflateCopy 还会清空非 NULL 目标的状态。这种拒绝不修改查询输出单元。
  • 受限定义域指这些显式内存、生命周期和调用顺序条件,加上条目自身的前置条件。它不意味着接受每个可表示的指针或整数。错误概述覆盖可读、可检查的状态,不覆盖任意无效地址。

形式化约定

ZlibF.Spec.Public.Goal.deflateEnd

证明状态:已登记证明 · 证明记录与剩余工作

/-- `int deflateEnd(z_streamp strm)`.
Free all five owned blocks. An unfinished busy stream returns `Z_DATA_ERROR` after freeing. -/
def Goal.deflateEnd : Prop :=
  ∀ h r i z s, Zlib.Deflate.Spec.DGood h r i z s → z.zfree = .fn "zcfree" →
    ∃ after, C.run (Zlib.Deflate.deflateEnd (some r)) h =
      .ok ((if s.status = BUSY_STATE then Z_DATA_ERROR else Z_OK), after) ∧
      r.get after = some { z with state := none } ∧
      LiveChange h after (fun _ => False) (DeflateOwned i s) ∧
      Frame h after (fun b => StreamRoot r b ∨ DeflateOwned i s b) ∧
      after.nalloc = h.nalloc ∧ after.nextBlk = h.nextBlk
相关定义与源码 ↗
ZLIB × LEAN

全局目录

当前位置deflateEnd