From a85813884397eabefd19f96e15ce60410a34f1a4 Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Wed, 28 Jul 2010 18:49:54 -0500 Subject: [PATCH] Fixes a bug in model verifier's handling of `let-one' --- .../redex/examples/racket-machine/verification-test.rkt | 7 +++++++ collects/redex/examples/racket-machine/verification.rkt | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/collects/redex/examples/racket-machine/verification-test.rkt b/collects/redex/examples/racket-machine/verification-test.rkt index c91a430a83..9ca315320a 100644 --- a/collects/redex/examples/racket-machine/verification-test.rkt +++ b/collects/redex/examples/racket-machine/verification-test.rkt @@ -383,6 +383,13 @@ void) (application (loc 2))))) +(test-predicate + bytecode-ok? + '(let-one 'x + (branch #f + (let-one (loc-noclr 1) void) + (loc-clr 0)))) + ; let-rec (test-predicate bytecode-ok? diff --git a/collects/redex/examples/racket-machine/verification.rkt b/collects/redex/examples/racket-machine/verification.rkt index 23ab03806c..cc98c4a0c2 100644 --- a/collects/redex/examples/racket-machine/verification.rkt +++ b/collects/redex/examples/racket-machine/verification.rkt @@ -65,7 +65,7 @@ ; let-one [(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_1 γ_1 η_1) (verify e_r s_0 ,(add1 (term n_l)) #f γ η ∅)) (where (uninit ṽ_1* ...) (trim s_1 s_0))]