Saturday, September 30, 2006
BrainScan
BrainScan is a source-code model checker for BrainF*ck. Source tar ball and statically-linked x86 linux binary. BrainScan is written by OCaml, so to compile you need OCaml (> =3.09) , findlib and extlib.
BrainScan can check
or --hash options allow to compress the state space using hash values. This makes the check imprecise, but save large amount of memory. should be integer from 1 to 31.
Enjoy!
BrainScan can check
- Underflow of the pointer
- Out-of-range (>255 or <0)>
- Reachability to locations marked '!'
- '.' prints the range of value possibly printed there. (only with -D or --dot option)
Enjoy!