emina
commented
1 year ago Rosette doesn't support unstructured control flow (such as returns and call/cc).
But you can implement it with the existing constructs.
See here for an example that uses a shallow embedding, and here for an example that uses a deep embedding.
A shallow embedding is easier to implement, but a deep embedding gives you better control over the performance of the symbolic evaluator (merging/splitting with for/all).
jnear
I'm interested in modeling control-flow constructs like switch and return in C. This is easy to do with call/cc, but it's not clear that call/cc is supported (at least in Rosette/safe). Is call/cc supported in Rosette, or is there some other trick for implementing operators that affect control flow? Thanks!