TermiNexus
66ebd75dec
新增 3 个工程（均登记进 regression_test.py / SequentialRegressionTest.py / run_lifetime_negative_tests.py 的 escape/负向清单）： - NewLifetimeRetOkTest（正向）：ret(heap)/ret(static)/ret(borrows=none) 的结果 可存进堆对象字段；ret(frame)/ret(borrows=x) 的结果只在本帧内使用； 同模块契约表与跨模块 .vpi(escr=) 两条取用路径都覆盖 → 编译通过 + 退出码 0。 - NewLifetimeRetEscapeTest（负向）：同模块 @life(ret(frame)) 的返回值写进堆对象 字段 → LifetimeError（隔离性：FrameRet 摘要为 0，唯一报错源是 ret 契约）。 - NewLifetimeRetXmodTest（负向）：跨模块 @life(noescape(x), ret(borrows=x)) 的结果 写进堆对象字段 → LifetimeError（契约经对方 .vpi 的 escr= 传来；noescape 清掉了 实参逃逸路径，判据收敛到 ret 契约）。 README.md 的 escape 测试表与负向清单同步。
65 lines
2.4 KiB
Plaintext
65 lines
2.4 KiB
Plaintext
from stdint import *
|
||
import stdio
|
||
import retdep
|
||
|
||
|
||
# =============================================================================
|
||
# 正向工程：A2 `@life(ret(...))` 契约**不得误报**（编译必须成功、运行退出码 0）
|
||
#
|
||
# 对照负向工程：
|
||
# · NewLifetimeRetEscapeTest —— 同模块 `ret(frame)` 的结果存进长命存储 → 必须报；
|
||
# · NewLifetimeRetXmodTest —— 跨模块 `ret(borrows=x)`（经 .vpi 的 escr=）→ 必须报。
|
||
#
|
||
# 本工程覆盖：
|
||
# (1) 非帧契约（heap / static / borrows=none）→ 结果可存进**堆对象字段**（长命左值）；
|
||
# (2) ret(frame) → 结果只在本帧内使用 → 合法（不是"无害"，而是调用点按声明**放行**）；
|
||
# (3) ret(borrows=x) → 结果的生命期 = 实参 x 的生命期（本帧实参 → 帧内使用合法）；
|
||
# (4) 同模块（本文件契约表）与跨模块（retdep.vp，经 .vpi 的 escr=）两条取用路径都走一遍。
|
||
#
|
||
# 注意：本文件**不得**把 `ret(frame)` / `ret(borrows=x)` 的结果写进堆对象字段
|
||
# （`h.p = …`）——那是负向工程负责证明会被拒的写法。
|
||
# =============================================================================
|
||
|
||
|
||
novirtual class Holder:
|
||
p: int*
|
||
c: char*
|
||
|
||
|
||
# ---- 同模块契约（走本文件 EscDirTable，不经 .vpi）----
|
||
|
||
@life(ret(heap))
|
||
def LocalHeap() -> int*:
|
||
return new heap hlife int
|
||
|
||
|
||
@life(ret(frame))
|
||
def LocalFrame() -> int*:
|
||
l: int* = new stack int
|
||
return l
|
||
|
||
|
||
export def main() -> int:
|
||
h: Holder* = new heap hlife Holder()
|
||
|
||
# (1) 非帧契约 → 存进堆对象字段（左值长命、右值非帧）→ 放行
|
||
h.p = retdep.MkHeap() # 跨模块 ret(heap)
|
||
h.c = retdep.MkStatic() # 跨模块 ret(static)
|
||
h.p = retdep.Fresh() # 跨模块 ret(borrows=none)
|
||
h.p = LocalHeap() # 同模块 ret(heap)
|
||
|
||
# (2) ret(frame)：结果只在本帧内使用 → 放行
|
||
pf: int* = retdep.FrameRet() # 跨模块 ret(frame)
|
||
pl: int* = LocalFrame() # 同模块 ret(frame)
|
||
|
||
# (3) ret(borrows=x)：结果生命期 = 实参生命期；实参在本帧 → 结果只在本帧用 → 放行
|
||
base: int* = new stack int
|
||
pb: int* = retdep.IdentBorrow(base)
|
||
|
||
if pf is None: return 1
|
||
if pl is None: return 2
|
||
if pb is None: return 3
|
||
|
||
stdio.printf("RetOkTest OK: @life(ret(...)) contracts accepted\n")
|
||
return 0
|