6.1 Exported Racket Libraries
Input and Output | current-input-port, current-output-port, current-error-port, eof, read, read-syntax, write, display, print, displayln, fprintf, printf, eprintf, format, pretty-print, pretty-write, pretty-display, pretty-format |
Operating System |
These facilities are safe to use in Rosette programs, even in the presence of symbolic values, assertions, and solver-aided queries. They are not, however, lifted: if their Racket implementation expects a concrete value of a given type, they will fail when given a symbolic value. These constructs are safe to use in the sense that they will fail in a predictable fashion, according to their concrete Racket specification, instead of causing the enclosing Rosette program to exhibit unexpected behavior.
The rosette/safe language allows programs to import arbitrary Racket code using the standard require mechanism. This is strongly discouraged, however, unless the use of such code obeys the restrictions outlined in the Chapter 8. Violating these restrictions may lead to incorrect program behavior, crashes, and loss of data (for programs that perform external side-effects, such as writing to files). In other words, arbitrary Racket code is, by default, unsafe to use.