Revision 86ae18b7 src/backends/Horn/horn_backend_printers.ml
src/backends/Horn/horn_backend_printers.ml | ||
---|---|---|
21 | 21 |
open Machine_code |
22 | 22 |
|
23 | 23 |
open Horn_backend_common |
24 |
|
|
24 |
open Types |
|
25 | 25 |
|
26 | 26 |
(********************************************************************************************) |
27 | 27 |
(* Instruction Printing functions *) |
28 | 28 |
(********************************************************************************************) |
29 | 29 |
|
30 | 30 |
let pp_horn_var m fmt id = |
31 |
if Types.is_array_type id.var_type |
|
31 |
(*if Types.is_array_type id.var_type
|
|
32 | 32 |
then |
33 | 33 |
assert false (* no arrays in Horn output *) |
34 |
else |
|
34 |
else*)
|
|
35 | 35 |
fprintf fmt "%s" id.var_id |
36 | 36 |
|
37 | 37 |
(* Used to print boolean constants *) |
... | ... | |
46 | 46 |
| Const_tag t -> pp_horn_tag fmt t |
47 | 47 |
| _ -> assert false |
48 | 48 |
|
49 |
(* PL comment 2017/01/03: Useless code, the function existed before in typing.ml *) |
|
50 |
(* let rec get_type_cst c = *) |
|
51 |
(* match c with *) |
|
52 |
(* | Const_int(n) -> new_ty Tint *) |
|
53 |
(* | Const_real _ -> new_ty Treal *) |
|
54 |
(* (\* | Const_float _ -> new_ty Treal *\) *) |
|
55 |
(* | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), *) |
|
56 |
(* get_type_cst (List.hd l))) *) |
|
57 |
(* | Const_tag(tag) -> new_ty Tbool *) |
|
58 |
(* | Const_string(str) -> assert false(\* used only for annotations *\) *) |
|
59 |
(* | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) *) |
|
60 |
|
|
61 |
(* PL comment 2017/01/03: the following function get_type seems useless to me: it looks like computing the type of a machine code expression v while v.value_type should contain this information. The code is kept for the moment in case I missed something *) |
|
62 |
|
|
63 |
(* |
|
64 |
let rec get_type v = |
|
65 |
match v with |
|
66 |
| Cst c -> Typing.type_const Location.dummy_loc c (* get_type_cst c*) |
|
67 |
| Access(tab, index) -> begin |
|
68 |
let rec remove_link ltype = |
|
69 |
match (dynamic_type ltype).tdesc with |
|
70 |
| Tlink t -> t |
|
71 |
| _ -> ltype |
|
72 |
in |
|
73 |
match (dynamic_type (remove_link (get_type tab))).tdesc with |
|
74 |
| Tarray(size, t) -> remove_link t |
|
75 |
| Tvar -> Format.eprintf "Type of access is a variable... "; assert false |
|
76 |
| Tunivar -> Format.eprintf "Type of access is a variable... "; assert false |
|
77 |
| _ -> Format.eprintf "Type of access is not an array "; assert false |
|
78 |
end |
|
79 |
| Power(v, n) -> assert false |
|
80 |
| LocalVar v -> v.var_type |
|
81 |
| StateVar v -> v.var_type |
|
82 |
| Fun(n, vl) -> begin match n with |
|
83 |
| "+" |
|
84 |
| "-" |
|
85 |
| "*" -> get_type (List.hd vl) |
|
86 |
| _ -> Format.eprintf "Function undealt with : %s" n ;assert false |
|
87 |
end |
|
88 |
| Array(l) -> new_ty (Tarray(Dimension.mkdim_int |
|
89 |
(Location.dummy_loc) |
|
90 |
(List.length l), |
|
91 |
get_type (List.hd l))) |
|
92 |
| _ -> assert false |
|
93 |
*) |
|
94 |
|
|
95 |
(* Default value for each type, used when building arrays. Eg integer array |
|
96 |
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value |
|
97 |
for the type integer (arrays). |
|
98 |
*) |
|
99 |
let rec pp_default_val fmt t = |
|
100 |
match (dynamic_type t).tdesc with |
|
101 |
| Tint -> fprintf fmt "0" |
|
102 |
| Treal -> fprintf fmt "0" |
|
103 |
| Tbool -> fprintf fmt "true" |
|
104 |
| Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *) |
|
105 |
let valt = array_element_type t in |
|
106 |
fprintf fmt "((as const (Array Int %a)) %a)" |
|
107 |
pp_type valt |
|
108 |
pp_default_val valt |
|
109 |
| Tstruct(l) -> assert false |
|
110 |
| Ttuple(l) -> assert false |
|
111 |
|_ -> assert false |
|
112 |
|
|
113 |
|
|
49 | 114 |
(* Prints a value expression [v], with internal function calls only. |
50 | 115 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
51 | 116 |
but an offset suffix may be added for array variables |
52 | 117 |
*) |
53 | 118 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
54 | 119 |
match v.value_desc with |
55 |
| Cst c -> pp_horn_const fmt c |
|
56 |
| Array _ |
|
57 |
| Access _ -> assert false (* no arrays *) |
|
58 |
| Power (v, n) -> assert false |
|
59 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
|
60 |
| StateVar v -> |
|
61 |
if Types.is_array_type v.var_type |
|
62 |
then assert false |
|
63 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
|
64 |
| Fun (n, vl) -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
|
120 |
| Cst c -> pp_horn_const fmt c |
|
121 |
|
|
122 |
(* Code specific for arrays *) |
|
123 |
| Array il -> |
|
124 |
(* An array definition: |
|
125 |
(store ( |
|
126 |
... |
|
127 |
(store ( |
|
128 |
store ( |
|
129 |
default_val |
|
130 |
) |
|
131 |
idx_n val_n |
|
132 |
) |
|
133 |
idx_n-1 val_n-1) |
|
134 |
... |
|
135 |
idx_1 val_1 |
|
136 |
) *) |
|
137 |
let rec print fmt (tab, x) = |
|
138 |
match tab with |
|
139 |
| [] -> pp_default_val fmt v.value_type(* (get_type v) *) |
|
140 |
| h::t -> |
|
141 |
fprintf fmt "(store %a %i %a)" |
|
142 |
print (t, (x+1)) |
|
143 |
x |
|
144 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) h |
|
145 |
in |
|
146 |
print fmt (il, 0) |
|
147 |
|
|
148 |
| Access(tab,index) -> |
|
149 |
fprintf fmt "(select %a %a)" |
|
150 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) tab |
|
151 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) index |
|
152 |
|
|
153 |
(* Code specific for arrays *) |
|
154 |
|
|
155 |
| Power (v, n) -> assert false |
|
156 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
|
157 |
| StateVar v -> |
|
158 |
if Types.is_array_type v.var_type |
|
159 |
then assert false |
|
160 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
|
161 |
| Fun (n, vl) -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
|
65 | 162 |
|
66 | 163 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
67 | 164 |
let rec pp_value_suffix self pp_value fmt value = |
... | ... | |
79 | 176 |
*) |
80 | 177 |
let pp_assign m pp_var fmt var_name value = |
81 | 178 |
let self = m.mname.node_id in |
82 |
fprintf fmt "(= %a %a)"
|
|
179 |
fprintf fmt "(= %a %a)" |
|
83 | 180 |
(pp_horn_val ~is_lhs:true self pp_var) var_name |
84 | 181 |
(pp_value_suffix self pp_var) value |
85 |
|
|
182 |
|
|
86 | 183 |
|
87 | 184 |
(* In case of no reset call, we define mid_mem = current_mem *) |
88 | 185 |
let pp_no_reset machines m fmt i = |
89 | 186 |
let (n,_) = List.assoc i m.minstances in |
90 | 187 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
91 | 188 |
|
92 |
let m_list =
|
|
189 |
let m_list = |
|
93 | 190 |
rename_machine_list |
94 | 191 |
(concat m.mname.node_id i) |
95 | 192 |
(rename_mid_list (full_memory_vars machines target_machine)) |
... | ... | |
104 | 201 |
fprintf fmt "(= %a %a)" |
105 | 202 |
(pp_horn_var m) mhd |
106 | 203 |
(pp_horn_var m) chd |
107 |
|
|
204 |
|
|
108 | 205 |
| _ -> ( |
109 | 206 |
fprintf fmt "@[<v 0>(and @[<v 0>"; |
110 |
List.iter2 (fun mhd chd ->
|
|
207 |
List.iter2 (fun mhd chd -> |
|
111 | 208 |
fprintf fmt "(= %a %a)@ " |
112 | 209 |
(pp_horn_var m) mhd |
113 | 210 |
(pp_horn_var m) chd |
... | ... | |
120 | 217 |
let pp_instance_reset machines m fmt i = |
121 | 218 |
let (n,_) = List.assoc i m.minstances in |
122 | 219 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
123 |
|
|
220 |
|
|
124 | 221 |
fprintf fmt "(%a @[<v 0>%a)@]" |
125 | 222 |
pp_machine_reset_name (node_name n) |
126 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
223 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
127 | 224 |
( |
128 | 225 |
(rename_machine_list |
129 | 226 |
(concat m.mname.node_id i) |
130 | 227 |
(rename_current_list (full_memory_vars machines target_machine)) |
131 |
)
|
|
228 |
) |
|
132 | 229 |
@ |
133 | 230 |
(rename_machine_list |
134 | 231 |
(concat m.mname.node_id i) |
... | ... | |
146 | 243 |
if not (List.mem i reset_instances) then |
147 | 244 |
(* If not, declare mem_m = mem_c *) |
148 | 245 |
pp_no_reset machines m fmt i; |
149 |
|
|
246 |
|
|
150 | 247 |
let mems = full_memory_vars machines target_machine in |
151 | 248 |
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in |
152 | 249 |
let mid_mems = rename_mems rename_mid_list in |
... | ... | |
157 | 254 |
fprintf fmt "@[<v 5>(and "; |
158 | 255 |
fprintf fmt "(= %a (ite %a %a %a))" |
159 | 256 |
(pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *) |
160 |
(pp_horn_var m) mem_m
|
|
257 |
(pp_horn_var m) mem_m |
|
161 | 258 |
(pp_horn_val self (pp_horn_var m)) i1 |
162 | 259 |
(pp_horn_val self (pp_horn_var m)) i2 |
163 | 260 |
; |
... | ... | |
175 | 272 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs) |
176 | 273 |
(Utils.pp_final_char_if_non_empty "@ " outputs) |
177 | 274 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems) |
178 |
|
|
275 |
|
|
179 | 276 |
end |
180 | 277 |
end |
181 | 278 |
with Not_found -> ( (* stateless node instance *) |
... | ... | |
188 | 285 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
189 | 286 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs) |
190 | 287 |
) |
191 |
|
|
192 |
|
|
288 |
|
|
289 |
|
|
193 | 290 |
(* Print the instruction and update the set of reset instances *) |
194 | 291 |
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list = |
195 | 292 |
match instr with |
... | ... | |
230 | 327 |
statement. *) |
231 | 328 |
let self = m.mname.node_id in |
232 | 329 |
let pp_branch fmt (tag, instrs) = |
233 |
fprintf fmt
|
|
234 |
"@[<v 3>(or (not (= %a %s))@ "
|
|
330 |
fprintf fmt |
|
331 |
"@[<v 3>(or (not (= %a %s))@ " |
|
235 | 332 |
(*"@[<v 3>(=> (= %a %s)@ "*) (* Issues with some versions of Z3. It |
236 | 333 |
seems that => within Horn predicate |
237 | 334 |
may cause trouble. I have hard time |
... | ... | |
244 | 341 |
() (* rs *) |
245 | 342 |
in |
246 | 343 |
pp_conj pp_branch fmt hl; |
247 |
reset_instances
|
|
344 |
reset_instances |
|
248 | 345 |
|
249 |
and pp_machine_instrs machines reset_instances m fmt instrs =
|
|
346 |
and pp_machine_instrs machines reset_instances m fmt instrs = |
|
250 | 347 |
let ppi rs fmt i = pp_machine_instr machines rs m fmt i in |
251 | 348 |
match instrs with |
252 |
| [x] -> ppi reset_instances fmt x
|
|
349 |
| [x] -> ppi reset_instances fmt x |
|
253 | 350 |
| _::_ -> |
254 | 351 |
fprintf fmt "(and @[<v 0>"; |
255 |
let rs = List.fold_left (fun rs i ->
|
|
352 |
let rs = List.fold_left (fun rs i -> |
|
256 | 353 |
let rs = ppi rs fmt i in |
257 | 354 |
fprintf fmt "@ "; |
258 | 355 |
rs |
259 | 356 |
) |
260 |
reset_instances instrs
|
|
357 |
reset_instances instrs |
|
261 | 358 |
in |
262 | 359 |
fprintf fmt "@])"; |
263 | 360 |
rs |
... | ... | |
269 | 366 |
fprintf fmt "@[<v 5>(and @ "; |
270 | 367 |
|
271 | 368 |
(* print "x_m = x_c" for each local memory *) |
272 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v ->
|
|
369 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v -> |
|
273 | 370 |
fprintf fmt "(= %a %a)" |
274 | 371 |
(pp_horn_var m) (rename_mid v) |
275 | 372 |
(pp_horn_var m) (rename_current v) |
... | ... | |
281 | 378 |
*) |
282 | 379 |
(Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) -> |
283 | 380 |
let name = node_name n in |
284 |
if name = "_arrow" then (
|
|
381 |
if name = "_arrow" then ( |
|
285 | 382 |
fprintf fmt "(= %s._arrow._first_m true)" |
286 |
(concat m.mname.node_id id)
|
|
383 |
(concat m.mname.node_id id) |
|
287 | 384 |
) else ( |
288 |
let machine_n = get_machine machines name in
|
|
289 |
fprintf fmt "(%s_reset @[<hov 0>%a@])"
|
|
385 |
let machine_n = get_machine machines name in |
|
386 |
fprintf fmt "(%s_reset @[<hov 0>%a@])" |
|
290 | 387 |
name |
291 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
388 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
292 | 389 |
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) |
293 | 390 |
) |
294 | 391 |
)) fmt m.minstances; |
... | ... | |
314 | 411 |
else |
315 | 412 |
begin |
316 | 413 |
fprintf fmt "; %s@." m.mname.node_id; |
317 |
|
|
414 |
|
|
318 | 415 |
(* Printing variables *) |
319 | 416 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
320 | 417 |
( |
... | ... | |
358 | 455 |
|
359 | 456 |
(* Rule for reset *) |
360 | 457 |
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." |
361 |
(pp_machine_reset machines) m
|
|
458 |
(pp_machine_reset machines) m |
|
362 | 459 |
pp_machine_reset_name m.mname.node_id |
363 | 460 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m); |
364 | 461 |
|
... | ... | |
373 | 470 |
pp_machine_step_name m.mname.node_id |
374 | 471 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
375 | 472 |
end |
376 |
| assertsl ->
|
|
473 |
| assertsl -> |
|
377 | 474 |
begin |
378 | 475 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in |
379 | 476 |
(* print_string pp_val; *) |
380 | 477 |
fprintf fmt "; with Assertions @."; |
381 |
|
|
478 |
|
|
382 | 479 |
(*Rule for step*) |
383 | 480 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
384 | 481 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
... | ... | |
386 | 483 |
pp_machine_step_name m.mname.node_id |
387 | 484 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
388 | 485 |
end |
389 |
|
|
390 |
|
|
486 |
|
|
487 |
|
|
391 | 488 |
end |
392 | 489 |
end |
393 | 490 |
|
394 | 491 |
|
492 |
let mk_flags arity = |
|
493 |
let b_range = |
|
494 |
let rec range i j = |
|
495 |
if i > arity then [] else i :: (range (i+1) j) in |
|
496 |
range 2 arity; |
|
497 |
in |
|
498 |
List.fold_left (fun acc x -> acc ^ " false") "true" b_range |
|
499 |
|
|
500 |
|
|
501 |
(*Get sfunction infos from command line*) |
|
502 |
let get_sf_info() = |
|
503 |
let splitted = Str.split (Str.regexp "@") !Options.sfunction in |
|
504 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction); |
|
505 |
let sf_name, flags, arity = match splitted with |
|
506 |
[h;flg;par] -> h, flg, par |
|
507 |
| _ -> failwith "Wrong Sfunction info" |
|
508 |
|
|
509 |
in |
|
510 |
Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity); |
|
511 |
sf_name, flags, arity |
|
512 |
|
|
513 |
|
|
514 |
(*a function to print the rules in case we have an s-function*) |
|
515 |
let print_sfunction machines fmt m = |
|
516 |
if m.mname.node_id = arrow_id then |
|
517 |
(* We don't print arrow function *) |
|
518 |
() |
|
519 |
else |
|
520 |
begin |
|
521 |
Format.fprintf fmt "; SFUNCTION@."; |
|
522 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
|
523 |
Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction; |
|
524 |
|
|
525 |
(* Check if there is annotation for s-function *) |
|
526 |
if m.mannot != [] then( |
|
527 |
Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot; |
|
528 |
); |
|
529 |
|
|
530 |
(* Printing variables *) |
|
531 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
|
532 |
((step_vars machines m)@ |
|
533 |
(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
|
534 |
Format.pp_print_newline fmt (); |
|
535 |
let sf_name, flags, arity = get_sf_info() in |
|
536 |
|
|
537 |
if is_stateless m then |
|
538 |
begin |
|
539 |
(* Declaring single predicate *) |
|
540 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
541 |
pp_machine_stateless_name m.mname.node_id |
|
542 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
543 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
|
544 |
Format.pp_print_newline fmt (); |
|
545 |
(* Rule for single predicate *) |
|
546 |
let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in |
|
547 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@." |
|
548 |
str_flags |
|
549 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m) |
|
550 |
pp_machine_stateless_name m.mname.node_id |
|
551 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m); |
|
552 |
end |
|
553 |
else |
|
554 |
begin |
|
555 |
(* Declaring predicate *) |
|
556 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
557 |
pp_machine_reset_name m.mname.node_id |
|
558 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
559 |
(List.map (fun v -> v.var_type) (inout_vars machines m)); |
|
560 |
|
|
561 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
562 |
pp_machine_step_name m.mname.node_id |
|
563 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
564 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
565 |
|
|
566 |
Format.pp_print_newline fmt (); |
|
567 |
(* Adding assertions *) |
|
568 |
match m.mstep.step_asserts with |
|
569 |
| [] -> |
|
570 |
begin |
|
571 |
|
|
572 |
(* Rule for step*) |
|
573 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
574 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
575 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
576 |
pp_machine_step_name m.mname.node_id |
|
577 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
|
578 |
end |
|
579 |
| assertsl -> |
|
580 |
begin |
|
581 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in |
|
582 |
(* print_string pp_val; *) |
|
583 |
fprintf fmt "; with Assertions @."; |
|
584 |
|
|
585 |
(*Rule for step*) |
|
586 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
587 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
588 |
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
|
589 |
pp_machine_step_name m.mname.node_id |
|
590 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
|
591 |
end |
|
592 |
|
|
593 |
end |
|
594 |
|
|
595 |
end |
|
395 | 596 |
(* Local Variables: *) |
396 | 597 |
(* compile-command:"make -C ../../.." *) |
397 | 598 |
(* End: *) |
Also available in: Unified diff