qsym

 1mod error;
 2mod interp;
 3mod memory;
 4mod state;
 5mod value;
 6
 7use qbe_reader as qbe;
 8use std::env;
 9use z3::{Config, Context};
10
11use interp::*;
12
13fn run_qbe(fname: &str, source: Vec<qbe::Definition>) {
14    let mut cfg = Config::new();
15    cfg.set_model_generation(true);
16    let ctx = Context::new(&cfg);
17
18    let mut interp = Interp::new(&ctx, &source).unwrap();
19    interp.exec_symbolic(&fname.to_string()).unwrap();
20}
21
22fn main() {
23    let mut args = env::args();
24    let prog = args.next().unwrap();
25
26    if args.len() <= 1 {
27        eprintln!("Usage: {} FILE FUNC", prog);
28    } else {
29        let path = args.next().unwrap();
30        let func = args.next().unwrap();
31
32        let defs = qbe::parse_file(path).unwrap();
33        run_qbe(&func, defs);
34    }
35}