counterexamples
counterexamples copied to clipboard
Counterexample proposal: cross-stage persistence
The following MetaOCaml code, distilled from
Generating code with polymorphic let a ballad of value restriction, copying and sharing Oleg Kiselyov
involves an unsound interaction between three MetaOCaml features:
- polymorphic
let
- mutable references
- cross-stage persistence
let lift x = .<x>.
let foo = Runcode.run
.<let f () = .~(lift (ref None)) in
f () := Some 2;
match !(f ()) with Some x -> x ^ "3" | None -> "" >.
Running it in (the latest versions of) BER MetaOCaml produces a segmentation fault.