Skip to content
Snippets Groups Projects
Commit fcf1fd96 authored by Temesghen Kahsai's avatar Temesghen Kahsai
Browse files

Fixed horn backend to make query for properties. More work needed for cex

parent 15787c5b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/horn_backend.ml
+ 140
− 142
View file @ fcf1fd96
......@@ -18,10 +18,10 @@ let pp_type fmt t =
| Types.Tstatic _
| Types.Tconst _
| Types.Tarrow _
| _ -> Format.eprintf "internal error: pp_type %a@."
| _ -> Format.eprintf "internal error: pp_type %a@."
Types.print_ty t; assert false
let pp_decl_var fmt id =
let pp_decl_var fmt id =
Format.fprintf fmt "(declare-var %s %a)"
id.var_id
pp_type id.var_type
......@@ -29,52 +29,52 @@ let pp_decl_var fmt id =
let pp_var fmt id = Format.pp_print_string fmt id.var_id
let pp_conj pp fmt l =
match l with
let pp_conj pp fmt l =
match l with
[] -> assert false
| [x] -> pp fmt x
| _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
let rename f = (fun v -> {v with var_id = f v.var_id } )
let rename_machine p = rename (fun n -> concat p n)
let rename_machine_list p = List.map (rename_machine p)
let rename_current = rename (fun n -> n ^ "_c")
let rename_current_list = List.map rename_current
let rename_next = rename (fun n -> n ^ "_x")
let rename_next_list = List.map rename_next
let get_machine machines node_name =
List.find (fun m -> m.mname.node_id = node_name) machines
let get_machine machines node_name =
List.find (fun m -> m.mname.node_id = node_name) machines
let full_memory_vars machines machine =
let rec aux fst prefix m =
(rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
List.fold_left (fun accu (id, (n, _)) ->
let name = node_name n in
List.fold_left (fun accu (id, (n, _)) ->
let name = node_name n in
if name = "_arrow" then accu else
let machine_n = get_machine machines name in
( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
) [] (m.minstances)
) [] (m.minstances)
in
aux true machine.mname.node_id machine
let stateless_vars machines m =
let stateless_vars machines m =
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@
(rename_machine_list m.mname.node_id m.mstep.step_outputs)
let step_vars machines m =
let step_vars machines m =
(stateless_vars machines m)@
(rename_current_list (full_memory_vars machines m)) @
(rename_next_list (full_memory_vars machines m))
let init_vars machines m =
(stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m))
(rename_current_list (full_memory_vars machines m)) @
(rename_next_list (full_memory_vars machines m))
let init_vars machines m =
(stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m))
(********************************************************************************************)
(* Instruction Printing functions *)
(********************************************************************************************)
......@@ -107,13 +107,13 @@ let rec pp_horn_const fmt c =
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
match v with
| Cst c -> pp_horn_const fmt c
| Array _
| Array _
| Access _ -> assert false (* no arrays *)
| Power (v, n) -> assert false
| LocalVar v -> pp_var fmt (rename_machine self v)
| StateVar v ->
if Types.is_array_type v.var_type
then assert false
then assert false
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
| Fun (n, vl) -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
......@@ -133,10 +133,10 @@ let rec pp_value_suffix self pp_value fmt value =
*)
let pp_assign m self pp_var fmt var_type var_name value =
fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
let pp_instance_call
let pp_instance_call
machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
try (* stateful node instance *)
try (* stateful node instance *)
begin
let (n,_) = List.assoc i m.minstances in
match node_name n, inputs, outputs with
......@@ -145,65 +145,65 @@ let pp_instance_call
pp_assign
m
self
(pp_horn_var m)
(pp_horn_var m)
fmt
o.var_type (LocalVar o) i1
else
pp_assign
m self (pp_horn_var m) fmt
o.var_type (LocalVar o) i2
end
| name, _, _ ->
| name, _, _ ->
begin
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in
if init then
Format.fprintf fmt "(%a %a%t%a%t%a)"
pp_machine_init_name (node_name n)
pp_machine_init_name (node_name n)
(* inputs *)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
inputs
(Utils.pp_final_char_if_non_empty " " inputs)
(Utils.pp_final_char_if_non_empty " " inputs)
(* outputs *)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
(List.map (fun v -> LocalVar v) outputs)
(Utils.pp_final_char_if_non_empty " " outputs)
(* memories (next) *)
(Utils.fprintf_list ~sep:" " pp_var) (
rename_machine_list
(concat m.mname.node_id i)
rename_machine_list
(concat m.mname.node_id i)
(rename_next_list (full_memory_vars machines target_machine)
)
)
)
else
Format.fprintf fmt "(%a %a%t%a%t%a)"
pp_machine_step_name (node_name n)
pp_machine_step_name (node_name n)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
(Utils.pp_final_char_if_non_empty " " inputs)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
(Utils.pp_final_char_if_non_empty " " inputs)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
(List.map (fun v -> LocalVar v) outputs)
(Utils.pp_final_char_if_non_empty " " outputs)
(Utils.fprintf_list ~sep:" " pp_var) (
(rename_machine_list
(concat m.mname.node_id i)
(rename_machine_list
(concat m.mname.node_id i)
(rename_current_list (full_memory_vars machines target_machine))
) @
(rename_machine_list
(concat m.mname.node_id i)
) @
(rename_machine_list
(concat m.mname.node_id i)
(rename_next_list (full_memory_vars machines target_machine))
)
)
)
end
end
with Not_found -> ( (* stateless node instance *)
let (n,_) = List.assoc i m.mcalls in
Format.fprintf fmt "(%s %a%t%a)"
(node_name n)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
inputs
(Utils.pp_final_char_if_non_empty " " inputs)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
(Utils.pp_final_char_if_non_empty " " inputs)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
(List.map (fun v -> LocalVar v) outputs)
)
......@@ -225,7 +225,7 @@ let rec pp_conditional machines ?(init=false) (m: machine_t) self fmt c tl el =
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) el
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
match instr with
match instr with
| MReset i ->
pp_machine_init m self fmt i
| MLocalAssign (i,v) ->
......@@ -236,7 +236,7 @@ and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
pp_assign
m self (pp_horn_var m) fmt
i.var_type (StateVar i) v
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
assert false (* This should not happen anymore *)
| MStep (il, i, vl) ->
pp_instance_call machines ~init:init m self fmt i vl il
......@@ -251,44 +251,44 @@ and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
(**************************************************************)
let is_stateless m = m.minstances = [] && m.mmemory = []
(* Print the machine m:
let is_stateless m = m.minstances = [] && m.mmemory = []
(* Print the machine m:
two functions: m_init and m_step
- m_init is a predicate over m memories
- m_step is a predicate over old_memories, inputs, new_memories, outputs
We first declare all variables then the two /rules/.
*)
let print_machine machines fmt m =
let print_machine machines fmt m =
let pp_instr init = pp_machine_instr machines ~init:init m in
if m.mname.node_id = arrow_id then
if m.mname.node_id = arrow_id then
(* We don't print arrow function *)
()
else
begin
else
begin
Format.fprintf fmt "; %s@." m.mname.node_id;
(* Printing variables *)
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
((step_vars machines m)@
(rename_machine_list m.mname.node_id m.mstep.step_locals));
Format.pp_print_newline fmt ();
if is_stateless m then
begin
(* Declaring single predicate *)
Format.fprintf fmt "(declare-rel %a (%a))@."
pp_machine_stateless_name m.mname.node_id
(Utils.fprintf_list ~sep:" " pp_type)
(Utils.fprintf_list ~sep:" " pp_type)
(List.map (fun v -> v.var_type) (stateless_vars machines m));
(* Rule for single predicate *)
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
(pp_conj (pp_instr
true (* In this case, the boolean init can be set to true or false.
(pp_conj (pp_instr
true (* In this case, the boolean init can be set to true or false.
The node is stateless. *)
m.mname.node_id)
)
......@@ -296,19 +296,19 @@ let print_machine machines fmt m =
pp_machine_stateless_name m.mname.node_id
(Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
end
else
else
begin
(* Declaring predicate *)
Format.fprintf fmt "(declare-rel %a (%a))@."
pp_machine_init_name m.mname.node_id
(Utils.fprintf_list ~sep:" " pp_type)
(Utils.fprintf_list ~sep:" " pp_type)
(List.map (fun v -> v.var_type) (init_vars machines m));
Format.fprintf fmt "(declare-rel %a (%a))@."
pp_machine_step_name m.mname.node_id
(Utils.fprintf_list ~sep:" " pp_type)
(Utils.fprintf_list ~sep:" " pp_type)
(List.map (fun v -> v.var_type) (step_vars machines m));
Format.pp_print_newline fmt ();
(* Rule for init *)
......@@ -328,19 +328,19 @@ let print_machine machines fmt m =
| [] -> ()
| assertsl -> begin
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
Format.fprintf fmt "; Asserts@.";
Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@."
(pp_conj pp_val) assertsl;
(** TEME: the following code is the one we described. But it generates a segfault in z3
(** TEME: the following code is the one we described. But it generates a segfault in z3
Format.fprintf fmt "; Asserts for init@.";
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@."
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
pp_machine_init_name m.mname.node_id
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m)
(pp_conj pp_val) assertsl;
(pp_conj pp_val) assertsl;
Format.fprintf fmt "; Asserts for step@.";
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@."
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
......@@ -351,18 +351,18 @@ let print_machine machines fmt m =
*)
end
);
(*
match m.mspec with
None -> () (* No node spec; we do nothing *)
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
(
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
(
(* For the moment, we only deal with simple case: single ensures, no other parameters *)
()
)
| _ -> () (* Other cases give nothing *)
*)
*)
end
end
......@@ -374,20 +374,20 @@ let collecting_semantics machines fmt node machine =
let main_output =
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
in
let main_output_dummy =
let main_output_dummy =
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
in
let main_memory_next =
let main_memory_next =
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
main_output
in
let main_memory_current =
let main_memory_current =
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
main_output_dummy
in
(* Special case when the main node is stateless *)
let init_name, step_name =
let init_name, step_name =
if is_stateless machine then
pp_machine_stateless_name, pp_machine_stateless_name
else
......@@ -395,9 +395,9 @@ let collecting_semantics machines fmt node machine =
in
Format.fprintf fmt "(declare-rel MAIN (%a))@."
(Utils.fprintf_list ~sep:" " pp_type)
(Utils.fprintf_list ~sep:" " pp_type)
(List.map (fun v -> v.var_type) main_memory_next);
Format.fprintf fmt "; Initial set@.";
Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
Format.fprintf fmt "(rule INIT_STATE)@.";
......@@ -408,18 +408,18 @@ let collecting_semantics machines fmt node machine =
Format.fprintf fmt "; Inductive def@.";
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
Format.fprintf fmt
Format.fprintf fmt
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current
step_name node
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next
let check_prop machines fmt node machine =
let main_output =
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
in
let main_memory_next =
let main_memory_next =
(rename_next_list (full_memory_vars machines machine)) @ main_output
in
Format.fprintf fmt "; Property def@.";
......@@ -428,8 +428,7 @@ let check_prop machines fmt node machine =
(pp_conj pp_var) main_output
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next
;
if !Options.horn_queries then
Format.fprintf fmt "(query ERR)@."
Format.fprintf fmt "(query ERR)@."
let cex_computation machines fmt node machine =
......@@ -438,24 +437,24 @@ let cex_computation machines fmt node machine =
let cex_input =
rename_machine_list machine.mname.node_id machine.mstep.step_inputs
in
let cex_input_dummy =
let cex_input_dummy =
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
in
let cex_output =
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
in
let cex_output_dummy =
let cex_output_dummy =
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
in
let cex_memory_next =
let cex_memory_next =
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
in
let cex_memory_current =
let cex_memory_current =
cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
in
(* Special case when the cex node is stateless *)
let init_name, step_name =
let init_name, step_name =
if is_stateless machine then
pp_machine_stateless_name, pp_machine_stateless_name
else
......@@ -463,9 +462,9 @@ let cex_computation machines fmt node machine =
in
Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
(Utils.fprintf_list ~sep:" " pp_type)
(Utils.fprintf_list ~sep:" " pp_type)
(List.map (fun v -> v.var_type) cex_memory_next);
Format.fprintf fmt "; Initial set@.";
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
init_name node
......@@ -476,12 +475,12 @@ let cex_computation machines fmt node machine =
(* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
Format.fprintf fmt "(declare-var cexcpt Int)@.";
Format.fprintf fmt
Format.fprintf fmt
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
step_name node
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
let get_cex machines fmt node machine =
let cex_input =
......@@ -490,7 +489,7 @@ let get_cex machines fmt node machine =
let cex_output =
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
in
let cex_memory_next =
let cex_memory_next =
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
in
Format.fprintf fmt "; Property def@.";
......@@ -499,12 +498,11 @@ let get_cex machines fmt node machine =
(pp_conj pp_var) cex_output
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
;
if !Options.horn_queries then
Format.fprintf fmt "(query CEXTRACE)@."
Format.fprintf fmt "(query CEXTRACE)@."
let main_print machines fmt =
if !Options.main_node <> "" then
let main_print machines fmt =
if !Options.main_node <> "" then
begin
let node = !Options.main_node in
let machine = get_machine machines node in
......@@ -512,43 +510,43 @@ if !Options.main_node <> "" then
collecting_semantics machines fmt node machine;
check_prop machines fmt node machine;
cex_computation machines fmt node machine;
get_cex machines fmt node machine
if !Options.horn_cex then(
cex_computation machines fmt node machine;
get_cex machines fmt node machine)
end
let translate fmt basename prog machines =
List.iter (print_machine machines fmt) (List.rev machines);
main_print machines fmt
main_print machines fmt
let traces_file fmt basename prog machines =
Format.fprintf fmt
Format.fprintf fmt
"; Horn code traceability generated by %s@.; SVN version number %s@.@."
(Filename.basename Sys.executable_name)
(Filename.basename Sys.executable_name)
Version.number;
(* We extract the annotation dealing with traceability *)
let machines_traces = List.map (fun m ->
let traces : (ident * expr) list=
let machines_traces = List.map (fun m ->
let traces : (ident * expr) list=
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
let filtered =
List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots
let filtered =
List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots
in
let content = List.map snd filtered in
(* Elements are supposed to be a pair (tuple): variable, expression *)
List.map (fun ee ->
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
List.map (fun ee ->
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
| [], Expr_tuple [v;e] -> (
match v.expr_desc with
| Expr_ident vid -> vid, e
match v.expr_desc with
| Expr_ident vid -> vid, e
| _ -> assert false )
| _ -> assert false)
content
in
m, traces
) machines
......@@ -558,22 +556,22 @@ let traces_file fmt basename prog machines =
let compute_mems m =
let rec aux fst prefix m =
(List.map (fun mem -> (prefix, mem)) m.mmemory) @
List.fold_left (fun accu (id, (n, _)) ->
let name = node_name n in
List.fold_left (fun accu (id, (n, _)) ->
let name = node_name n in
if name = "_arrow" then accu else
let machine_n = get_machine machines name in
( aux false ((id,machine_n)::prefix) machine_n )
( aux false ((id,machine_n)::prefix) machine_n )
@ accu
) [] m.minstances
) [] m.minstances
in
aux true [] m
in
List.iter (fun m ->
Format.fprintf fmt "; Node %s@." m.mname.node_id;
let memories_old =
List.map (fun (p, v) ->
let memories_old =
List.map (fun (p, v) ->
let machine = match p with | [] -> m | (_,m')::_ -> m' in
let traces = List.assoc machine machines_traces in
if List.mem_assoc v.var_id traces then
......@@ -582,20 +580,20 @@ let traces_file fmt basename prog machines =
else
(* We keep the variable as is: we create an expression v *)
p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
) (compute_mems m)
) (compute_mems m)
in
let memories_next = (* We remove the topest pre in each expression *)
List.map
(fun (prefix, ee) ->
match ee.expr_desc with
| Expr_pre e -> prefix, e
| _ -> Format.eprintf
"Mem Failure: (prefix: %a, eexpr: %a)@.@?"
(Utils.fprintf_list ~sep:","
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
(List.rev prefix)
Printers.pp_expr ee;
List.map
(fun (prefix, ee) ->
match ee.expr_desc with
| Expr_pre e -> prefix, e
| _ -> Format.eprintf
"Mem Failure: (prefix: %a, eexpr: %a)@.@?"
(Utils.fprintf_list ~sep:","
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
(List.rev prefix)
Printers.pp_expr ee;
assert false)
memories_old
in
......@@ -631,9 +629,9 @@ let traces_file fmt basename prog machines =
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
(Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
Format.pp_print_newline fmt ();
Format.pp_print_newline fmt ();
) (List.rev machines);
(* Local Variables: *)
(* compile-command:"make -C .." *)
......
src/options.ml
+ 4
− 3
View file @ fcf1fd96
......@@ -37,7 +37,8 @@ let global_inline = ref false
let witnesses = ref false
let optimization = ref 2
let horntraces = ref false
let horn_queries = ref false
let horn_cex = ref false
let options =
[ "-d", Arg.Set_string dest_dir,
......@@ -54,7 +55,7 @@ let options =
"-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
"-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
"-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
"-horn-queries", Arg.Set horn_queries, "add the queries instructions at the end of the generated horn files";
"-horn-cex", Arg.Set horn_cex, "generate cex enumeration. Enable the horn backend (work in progress)";
"-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";
......@@ -74,7 +75,7 @@ let get_witness_dir filename =
)
with Sys_error _ -> Unix.mkdir dir 0o750
in
dir
dir
(* Local Variables: *)
(* compile-command:"make -C .." *)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment