CristalCaveGem » LustreC

    "-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";

    "-print_reuse", Arg.Set print_reuse, "prints variable reuse policy";

    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";

    "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";

    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";

    "-print_types", Arg.Set print_types, "prints node types";

  in

  dir

(* Local Variables: *)

(* compile-command:"make -C .." *)

(* End: *)