Project

General

Profile

Revision 9b0432bc lib/options_management.ml

View differences:

lib/options_management.ml
111 111
      "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
112 112
      "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
113 113
      "-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";
114
      "-tiny", Arg.Unit (fun () -> set_backend "tiny"), "generates Tiny output instead of C";
114 115
      (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
115 116
      "-ada", Arg.Unit (fun () -> set_backend "Ada"), "generates Ada encoding output instead of C";
116 117
      "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";

Also available in: Unified diff