Project

General

Profile

Revision f6923c9e src/options.ml

View differences:

src/options.ml
30 30
let ansi = ref false
31 31
let check = ref false
32 32
let c_spec = ref false
33
let java = ref false
33
let output = ref "C"
34 34
let dest_dir = ref ""
35 35
let verbose_level = ref 1
36 36

  
......
44 44
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds (default: no check)";
45 45
    "-c-spec", Arg.Set c_spec, 
46 46
    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
47
    "-java", Arg.Set java, "generates Java output instead of C";
47
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
48
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
48 49
    "-print_types", Arg.Set print_types, "prints node types";
49 50
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";
50 51
    "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";

Also available in: Unified diff