diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff index 6d63097529..8e17e9b466 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff @@ -1,7 +1,7 @@ 3c3 < (define the-error "no-error") --- -> (define the-error "bug 14") +> (define the-error "certain updates to initialized slots could break optimizer assumptions") 142c142,143 < (where uninit (stack-ref n s_2))] --- diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff index d147409970..070f7f78c6 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff @@ -1,7 +1,7 @@ 3c3 < (define the-error "no-error") --- -> (define the-error "bug 15") +> (define the-error "neglected to restict case-lam to accept only 'val' arguments") 125c125,126 < [(verify (case-lam (name l (lam (val ...) (n ...) e)) ...) s n_l b γ η f) --- diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff index eced4bfcf1..f5e2553a8e 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff @@ -1,3 +1,7 @@ +3c3 +< (define the-error "no-error") +--- +> (define the-error "stack offset / pointer confusion") 338c338,339 < (side-condition (< (term n_0) (term n_h)))] --- diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff index b61dc85f56..461413f60a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff @@ -1,7 +1,7 @@ 3c3 < (define the-error "no-error") --- -> (define the-error "bug 3") +> (define the-error "application slots not initialized properly") 100c100 < (where s_1 (abs-push n not s)) --- diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff index 813ab61e5d..bb053f3886 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff @@ -1,7 +1,7 @@ 3c3 < (define the-error "no-error") --- -> (define the-error "bug 4") +> (define the-error "mishandling branches when then branch needs more stack than else branch") 155c155,156 < (side-condition (< (term n_p) (term n_l)))] --- diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff index 246adfd756..987dee05fd 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff @@ -1,3 +1,7 @@ +3c3 +< (define the-error "no-error") +--- +> (define the-error "forgot to implement the case-lam branch in verifier") 127c127,128 < (side-condition (term (AND (lam-verified? l s ?) ...)))] --- diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt index 132aae8dbd..97928eb84c 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt @@ -1,6 +1,6 @@ #lang racket -(define the-error "bug 14") +(define the-error "certain updates to initialized slots could break optimizer assumptions") (require redex/reduction-semantics) (require "../../racket-machine/grammar.rkt" diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt index ab4c8f988f..6c7f3281bb 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt @@ -1,6 +1,6 @@ #lang racket -(define the-error "bug 15") +(define the-error "neglected to restict case-lam to accept only 'val' arguments") (require redex/reduction-semantics) (require "../../racket-machine/grammar.rkt" diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt index 2328e08707..5dbd749933 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt @@ -1,6 +1,6 @@ #lang racket -(define the-error "no-error") +(define the-error "stack offset / pointer confusion") (require redex/reduction-semantics) (require "../../racket-machine/grammar.rkt" diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt index 041d60f417..8b2ca24005 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt @@ -1,6 +1,6 @@ #lang racket -(define the-error "bug 3") +(define the-error "application slots not initialized properly") (require redex/reduction-semantics) (require "../../racket-machine/grammar.rkt" diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt index 3ada4193bf..1ac0d3abb7 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt @@ -1,6 +1,6 @@ #lang racket -(define the-error "bug 4") +(define the-error "mishandling branches when then branch needs more stack than else branch") (require redex/reduction-semantics) (require "../../racket-machine/grammar.rkt" diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt index 12af4369e1..8b373ca55f 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt @@ -1,6 +1,6 @@ #lang racket -(define the-error "no-error") +(define the-error "forgot to implement the case-lam branch in verifier") (require redex/reduction-semantics) (require "../../racket-machine/grammar.rkt"