examples/symbolic/README.md

Rama main · réplica de lectura del repositorio original.

# C\* Code Examples for Symbolic Execution

The purpose of the code in this directory is to demonstrate the capabilities of monster, a symbolic execution engine, beator, a RISC-U symbolic model generator, and rotor, a RISC-V symbolic model generator, which are all part of selfie. Monster as well as beator and rotor translate selfie-compiled RISC-U code to an SMT-LIB or BTOR2 formula, respectively, that is satisfiable if there is input to the code such that it exits with a non-zero exit code, or performs division by zero or an invalid/unsafe memory access. See selfie's Makefile for more details on how to execute the examples symbolically.