Project

General

Profile

Revision df647a81 src/options.ml

View differences:

src/options.ml
48 48
    "-c-spec", Arg.Set c_spec, 
49 49
    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
50 50
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
51
    "-dot", Arg.Unit (fun () -> output := "dot"), "generates dot graph";
51 52
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
52 53
    "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";
53 54
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";

Also available in: Unified diff