Project

General

Profile

Revision a6df3992 src/options.ml

View differences:

src/options.ml
75 75
    "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
76 76
    "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
77 77
    "-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
78
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
78
    (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
79 79
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
80 80
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
81 81
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
......
83 83
    "-horn-sfunction", Arg.Set_string sfunction, "Get the endpoint predicate of the sfunction";
84 84
    "-print_reuse", Arg.Set print_reuse, "prints variable reuse policy";
85 85
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
86
    "-emf", Arg.Unit (fun () -> output := "emf"), "generates EMF output, to be used by CocoSim";
86 87
    "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inline all node calls (require a main node). Implies constant unfolding";
87 88
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
88 89
    "-print_types", Arg.Set print_types, "prints node types";

Also available in: Unified diff