test(lifetime): 同步 A2 定义端'声明感知'的措辞
定义端不再'整体移除' return 本帧存储的检查,而是按被调者 @life(ret(...)) 声明 放行/报错(§14.3.2 方案 A)。更新 NewLifetimeRetEscapeTest / NewLifetimeRetOkTest 的注释与 README 描述,去掉'已移除 fail-fast'的旧说法。
This commit is contained in:
1 parent
66ebd75dec
commit
e8a61473b2
3 files changed
+9
-7
No files matched your search
@@ -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`)。
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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` 都支持):
|
||||
|
||||
Reference in new issue
Block a user