Contracts for C (Early Stages)
8 months ago
- #contracts
- #C programming
- #optimization
- C++合约提案(P2900)正考虑适配C语言，重点关注函数接口的前置与后置条件验证
- 前置/后置条件是可验证的入口/出口检查机制，既不影响ABI又能提升优化空间与正确性
- 条件表达式支持整型常量，类似static_assert，若验证失败将导致编译终止
- 引入两个原语：contract_assert(类似assert但始终生效)和contract_assume(误用有风险，假定条件成立)
- 示例展示my_malloc函数，通过pre(size)确保非零参数，post(r:r)保证返回非空指针
- 头文件中的内联函数可强制执行合约，defer机制确保所有退出路径都检查后置条件
- 观察发现：编译器能优化掉针对同一条件的冗余断言/假设语句
- 新执行模型用函数调用前的断言和函数体内的假设替代传统的前后置条件检查
- eclipse工具提供EXBINDING/INBINDING宏简化合约表达式，避免代码重复
- 当前局限：需完善接口规范与编译器支持，但已实现C语言合约的概念验证