phase29ab(p3): fix PromoteDecision contract and add negative smokes
This commit is contained in:
29
apps/tests/phase29ab_pattern2_seg_freeze_min.hako
Normal file
29
apps/tests/phase29ab_pattern2_seg_freeze_min.hako
Normal file
@ -0,0 +1,29 @@
|
||||
// Phase 29ab P3: Pattern2 LoopBodyLocal seg Freeze (read-only violation)
|
||||
//
|
||||
// Goal:
|
||||
// - break condition uses LoopBodyLocal seg
|
||||
// - seg is reassigned in the loop body (read-only contract violation)
|
||||
// - Pattern2 promotion must Freeze (fail-fast)
|
||||
//
|
||||
// Expected: JoinIR freeze error (non-zero exit)
|
||||
|
||||
static box Main {
|
||||
main() {
|
||||
local s = "ab "
|
||||
local i = 0
|
||||
|
||||
loop(i < s.length()) {
|
||||
local seg = s.substring(i, i + 1)
|
||||
|
||||
if seg == " " || seg == "\t" {
|
||||
break
|
||||
}
|
||||
|
||||
seg = "x"
|
||||
i = i + 1
|
||||
}
|
||||
|
||||
print(i)
|
||||
return i
|
||||
}
|
||||
}
|
||||
27
apps/tests/phase29ab_pattern2_seg_notapplicable_min.hako
Normal file
27
apps/tests/phase29ab_pattern2_seg_notapplicable_min.hako
Normal file
@ -0,0 +1,27 @@
|
||||
// Phase 29ab P3: Pattern2 LoopBodyLocal seg NotApplicable (shape mismatch)
|
||||
//
|
||||
// Goal:
|
||||
// - break condition uses no LoopBodyLocal vars
|
||||
// - Pattern2 promotion should be NotApplicable and continue safely
|
||||
//
|
||||
// Expected: prints "2" and returns 2
|
||||
|
||||
static box Main {
|
||||
main() {
|
||||
local s = "ab "
|
||||
local i = 0
|
||||
|
||||
loop(i < s.length()) {
|
||||
local seg = s.substring(i, i + 1)
|
||||
|
||||
if i >= 2 {
|
||||
break
|
||||
}
|
||||
|
||||
i = i + 1
|
||||
}
|
||||
|
||||
print(i)
|
||||
return i
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user