suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fixes a bug in model verifier's handling of `let-one'

Browse Source
This commit is contained in:
Casey Klein 2010-07-28 18:49:54 -05:00
parent 4cd2e8b01b
commit a858138843
2 changed files with 8 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
collects/redex/examples/racket-machine/verification-test.rkt
View File

@ -383,6 +383,13 @@
void) void)
(application (loc 2))))) (application (loc 2)))))
(test-predicate
bytecode-ok?
'(let-one 'x
(branch #f
(let-one (loc-noclr 1) void)
(loc-clr 0))))
; let-rec ; let-rec
(test-predicate (test-predicate
bytecode-ok? bytecode-ok?

2
collects/redex/examples/racket-machine/verification.rkt
View File

@ -65,7 +65,7 @@
; let-one ; let-one
[(verify (let-one e_r e_b) (ṽ_1 ...) n_l b γ η f) [(verify (let-one e_r e_b) (ṽ_1 ...) n_l b γ η f)
(verify e_b (imm ṽ_1* ...) ,(add1 (term n_l)) b γ η (shift 1 f)) (verify e_b (imm ṽ_1* ...) ,(add1 (term n_l)) b γ_1 η_1 (shift 1 f))
(where s_0 (uninit ṽ_1 ...)) (where s_0 (uninit ṽ_1 ...))
(where (s_1 γ_1 η_1) (verify e_r s_0 ,(add1 (term n_l)) #f γ η ∅)) (where (s_1 γ_1 η_1) (verify e_r s_0 ,(add1 (term n_l)) #f γ η ∅))
(where (uninit ṽ_1* ...) (trim s_1 s_0))] (where (uninit ṽ_1* ...) (trim s_1 s_0))]