diff --git a/NewLifetimeRetEscapeTest/App/main.vp b/NewLifetimeRetEscapeTest/App/main.vp index eb3be86..6d75975 100644 --- a/NewLifetimeRetEscapeTest/App/main.vp +++ b/NewLifetimeRetEscapeTest/App/main.vp @@ -4,9 +4,10 @@ from stdint import * # ============================================================================= # 负向工程(**应当编译失败**):A2 `@life(ret(frame))` —— 去向由**调用点**判定 # -# A2 移除了定义端对 `return <本帧地址>` 的 fail-fast:定义端无法区分"交出本帧" -# 与"借出调用方的存储"(后者是 `return <借用形参>`,一律拦会误报)。取而代之: -# 被调者用 `@life(ret(...))` 声明返回值生命期,**调用点**按声明判去向。 +# 定义端的判据是**声明感知**的(§14.3.2):`ret(frame)` / `ret(borrows=<该形参>)` 放行, +# 无声明或声明为非帧才报错 —— 因为定义端分不清"交出本帧"与"借出调用方的存储" +# (后者是 `return <借用形参>`,一律拦会误报)。于是"声明为 frame"之后,去向的判定 +# 就落在**调用点**:谁把这个结果存进了长命存储,谁就报错。 # # 本工程验:声明为 `frame` 的返回值被写进**长命存储**时必须被拒。 # 期望报错:LifetimeError(`a longer-lived field/element`)。 diff --git a/NewLifetimeRetOkTest/App/retdep.vp b/NewLifetimeRetOkTest/App/retdep.vp index e0137eb..b0cafc6 100644 --- a/NewLifetimeRetOkTest/App/retdep.vp +++ b/NewLifetimeRetOkTest/App/retdep.vp @@ -28,9 +28,10 @@ def Fresh() -> int*: return new heap hlife int -# ret(frame):返回值可能指向**本帧**存储 → 去向由调用点负责 -# (A2 已移除定义端对 `return <本帧地址>` 的 fail-fast:定义端无法区分 -# "交出本帧"与"借出调用方的存储",一律拦会误报 `return <借用形参>`。) +# ret(frame):返回值可能指向**本帧**存储 → 去向由调用点负责。 +# 定义端对 `return <本帧存储>` 是**声明感知**的(§14.3.2):声明成 frame(或 +# `borrows=<该形参>`)即放行,否则 fail-fast —— 所以下面 `return l` 合法, +# 而"无声明的 return l"会被拒(见 root/EscapeTest)。 @life(ret(frame)) def FrameRet() -> int*: l: int* = new stack int diff --git a/README.md b/README.md index 966bd84..6ec9f4b 100644 --- a/README.md +++ b/README.md @@ -145,7 +145,7 @@ | NewLifetimeFieldEscapeTest | [Test/NewLifetimeFieldEscapeTest/](NewLifetimeFieldEscapeTest/App/main.vp) | **编译失败**:P3 —— `h.p = &local`(堆对象字段收下本帧栈地址)→ `LifetimeError` | | NewLifetimeAnnFieldEscapeTest | [Test/NewLifetimeAnnFieldEscapeTest/](NewLifetimeAnnFieldEscapeTest/App/main.vp) | **编译失败**:P3 **注解形态** —— `h.p: int* = &local`(AnnAssign 属性目标,同一条规则;也守住"非 Name 目标不得被静默丢弃")→ `LifetimeError` | | NewLifetimeRetOkTest | [Test/NewLifetimeRetOkTest/](NewLifetimeRetOkTest/App/main.vp) | **编译成功 + 退出码 0**:A2(§14)`@life(ret(...))` 契约**不得误报** —— `ret(heap)`/`ret(static)`/`ret(borrows=none)` 的结果存进堆对象字段;`ret(frame)`/`ret(borrows=x)` 的结果只在本帧内使用;同模块(契约表)与跨模块(`retdep.vp`,经 `.vpi` 的 `escr=`)两条取用路径都走一遍 | -| NewLifetimeRetEscapeTest | [Test/NewLifetimeRetEscapeTest/](NewLifetimeRetEscapeTest/App/main.vp) | **编译失败**:A2 —— 同模块 `@life(ret(frame))` 的返回值被写进**堆对象字段**(长命左值)→ `LifetimeError`(A2 已移除定义端 `return <本帧地址>` 的 fail-fast,去向改由调用点按契约判定) | +| NewLifetimeRetEscapeTest | [Test/NewLifetimeRetEscapeTest/](NewLifetimeRetEscapeTest/App/main.vp) | **编译失败**:A2 —— 同模块 `@life(ret(frame))` 的返回值被写进**堆对象字段**(长命左值)→ `LifetimeError`(定义端按声明放行 `ret(frame)`,去向由**调用点**判定) | | NewLifetimeRetXmodTest | [Test/NewLifetimeRetXmodTest/](NewLifetimeRetXmodTest/App/main.vp) | **编译失败**:A2 **跨模块** —— 被调者(`retdep2.vp`)声明 `@life(noescape(x), ret(borrows=x))`,结果(生命期 = 实参 = 本帧)写进堆对象字段 → `LifetimeError`(契约经对方 `.vpi` 的 `escr=` 传来) | 单独运行(`regression_test.py` 与 `SequentialRegressionTest.py` 都支持):