Revision 86ae18b7 src/backends/Horn/horn_backend.ml
src/backends/Horn/horn_backend.ml | ||
---|---|---|
48 | 48 |
) |
49 | 49 |
end |
50 | 50 |
|
51 |
|
|
52 |
let load_file f = |
|
53 |
let ic = open_in f in |
|
54 |
let n = in_channel_length ic in |
|
55 |
let s = String.create n in |
|
56 |
really_input ic s 0 n; |
|
57 |
close_in ic; |
|
58 |
(s) |
|
59 |
|
|
51 | 60 |
let print_type_definitions fmt = |
52 | 61 |
let cpt_type = ref 0 in |
53 | 62 |
Hashtbl.iter (fun typ decl -> |
... | ... | |
68 | 77 |
| _ -> ()) type_table |
69 | 78 |
|
70 | 79 |
|
71 |
let translate fmt basename prog machines = |
|
80 |
|
|
81 |
|
|
82 |
let print_dep fmt prog = |
|
83 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting Horn libraries@,"); |
|
84 |
fprintf fmt "; Statically linked libraries@"; |
|
85 |
let dependencies = Corelang.get_dependencies prog in |
|
86 |
List.iter |
|
87 |
(fun dep -> |
|
88 |
let (local, s) = Corelang.dependency_of_top dep in |
|
89 |
let basename = ((if local then !Options.dest_dir else !Options.include_dir)) ^ s ^ ".smt2" in |
|
90 |
Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename); |
|
91 |
let horn = load_file basename in |
|
92 |
fprintf fmt "@.%s@." horn; |
|
93 |
) |
|
94 |
dependencies |
|
95 |
|
|
96 |
let check_sfunction mannot = |
|
97 |
(*Check if its an sfunction*) |
|
98 |
match mannot with |
|
99 |
[] -> false |
|
100 |
| [x] -> |
|
101 |
begin |
|
102 |
match x.annots with |
|
103 |
[] -> false |
|
104 |
|[(key,va)] -> |
|
105 |
begin |
|
106 |
match key with |
|
107 |
[] -> false |
|
108 |
| [x] -> x == "c_code" || x =="matlab" |
|
109 |
| _ -> false |
|
110 |
end |
|
111 |
|(_,_)::_ -> false |
|
112 |
end |
|
113 |
| _::_ -> false |
|
114 |
|
|
115 |
let translate fmt basename prog machines= |
|
72 | 116 |
(* We print typedef *) |
117 |
print_dep fmt prog; (*print static library e.g. math*) |
|
73 | 118 |
print_type_definitions fmt; |
74 |
List.iter (print_machine machines fmt) (List.rev machines); |
|
119 |
(*List.iter (print_machine machines fmt) (List.rev machines);*) |
|
120 |
List.iter(fun m -> |
|
121 |
let is_sfunction = check_sfunction m.mannot in |
|
122 |
if is_sfunction then( |
|
123 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. detected sfunction: %s@," m.mname.node_id); |
|
124 |
print_sfunction machines fmt m |
|
125 |
) else ( |
|
126 |
print_machine machines fmt m) |
|
127 |
) |
|
128 |
(List.rev machines); |
|
75 | 129 |
main_print machines fmt |
76 | 130 |
|
77 | 131 |
(* Local Variables: *) |
Also available in: Unified diff