1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
|
5
|
(* *)
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
8
|
(* version 2.1. *)
|
9
|
(* *)
|
10
|
(********************************************************************)
|
11
|
|
12
|
open Utils.Format
|
13
|
open Lustre_types
|
14
|
open Machine_code_types
|
15
|
open C_backend_common
|
16
|
open Corelang
|
17
|
open Spec_types
|
18
|
open Machine_code_common
|
19
|
|
20
|
(**************************************************************************)
|
21
|
(* Printing spec for c *)
|
22
|
|
23
|
(**************************************************************************)
|
24
|
|
25
|
(* TODO ACSL Return updates machines (eg with local annotations) and acsl
|
26
|
preamble *)
|
27
|
let preprocess_acsl machines = machines, []
|
28
|
|
29
|
let pp_acsl_basic_type_desc t_desc =
|
30
|
if Types.is_bool_type t_desc then
|
31
|
(* if !Options.cpp then "bool" else "_Bool" *)
|
32
|
"_Bool"
|
33
|
else if Types.is_int_type t_desc then
|
34
|
(* !Options.int_type *)
|
35
|
if t_desc.tid = -1 then "int" else "integer"
|
36
|
else if Types.is_real_type t_desc then
|
37
|
if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
|
38
|
else assert false
|
39
|
(* Not a basic C type. Do not handle arrays or pointers *)
|
40
|
|
41
|
let pp_acsl pp fmt = fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
|
42
|
|
43
|
let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp)
|
44
|
|
45
|
let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp
|
46
|
|
47
|
let pp_acsl_line' pp fmt = fprintf fmt "/*%@ @[<h>%a@] */" pp
|
48
|
|
49
|
let pp_acsl_line_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line pp)
|
50
|
|
51
|
let pp_requires pp_req fmt = fprintf fmt "requires %a;" pp_req
|
52
|
|
53
|
let pp_ensures pp_ens fmt = fprintf fmt "ensures %a;" pp_ens
|
54
|
|
55
|
let pp_assumes pp_asm fmt = fprintf fmt "assumes %a;" pp_asm
|
56
|
|
57
|
let pp_assigns pp =
|
58
|
pp_comma_list
|
59
|
~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
|
60
|
~pp_epilogue:pp_print_semicolon' pp
|
61
|
|
62
|
let pp_ghost pp_gho fmt = fprintf fmt "ghost %a" pp_gho
|
63
|
|
64
|
let pp_assert pp_ast fmt = fprintf fmt "assert %a;" pp_ast
|
65
|
|
66
|
let pp_mem_valid pp_var fmt (name, var) =
|
67
|
fprintf fmt "%s_valid(%a)" name pp_var var
|
68
|
|
69
|
let pp_mem_valid' = pp_mem_valid pp_print_string
|
70
|
|
71
|
let pp_indirect pp_ptr pp_field fmt (ptr, field) =
|
72
|
fprintf fmt "%a->%a" pp_ptr ptr pp_field field
|
73
|
|
74
|
let pp_indirect' = pp_indirect pp_print_string pp_print_string
|
75
|
|
76
|
let pp_access pp_stru pp_field fmt (stru, field) =
|
77
|
fprintf fmt "%a.%a" pp_stru stru pp_field field
|
78
|
|
79
|
let pp_access' = pp_access pp_print_string pp_print_string
|
80
|
|
81
|
let pp_var_decl fmt v = pp_print_string fmt v.var_id
|
82
|
|
83
|
let pp_reg self fmt field =
|
84
|
pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
|
85
|
|
86
|
let pp_true fmt () = pp_print_string fmt "\\true"
|
87
|
|
88
|
let pp_false fmt () = pp_print_string fmt "\\false"
|
89
|
|
90
|
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
|
91
|
|
92
|
let instances machines m =
|
93
|
let open List in
|
94
|
let grow paths i td mems =
|
95
|
match paths with
|
96
|
| [] ->
|
97
|
[ [ i, (td, mems) ] ]
|
98
|
| _ ->
|
99
|
map (cons (i, (td, mems))) paths
|
100
|
in
|
101
|
let rec aux paths m =
|
102
|
map
|
103
|
(fun (i, (td, _)) ->
|
104
|
try
|
105
|
let m = find (fun m -> m.mname.node_id = node_name td) machines in
|
106
|
aux (grow paths i td m.mmemory) m
|
107
|
with Not_found -> grow paths i td [])
|
108
|
m.minstances
|
109
|
|> flatten
|
110
|
in
|
111
|
aux [] m |> map rev
|
112
|
|
113
|
let memories insts =
|
114
|
List.(
|
115
|
map
|
116
|
(fun path ->
|
117
|
let _, (_, mems) = hd (rev path) in
|
118
|
map (fun mem -> path, mem) mems)
|
119
|
insts
|
120
|
|> flatten)
|
121
|
|
122
|
let pp_instance ?(indirect = true) ptr =
|
123
|
pp_print_list
|
124
|
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
|
125
|
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
|
126
|
(fun fmt (i, _) -> pp_print_string fmt i)
|
127
|
|
128
|
let pp_memory ?(indirect = true) ptr fmt (path, mem) =
|
129
|
pp_access
|
130
|
((if indirect then pp_indirect else pp_access)
|
131
|
(pp_instance ~indirect ptr)
|
132
|
pp_print_string)
|
133
|
pp_var_decl fmt
|
134
|
((path, "_reg"), mem)
|
135
|
|
136
|
let prefixes l =
|
137
|
let rec pref acc = function
|
138
|
| x :: l ->
|
139
|
pref ([ x ] :: List.map (List.cons x) acc) l
|
140
|
| [] ->
|
141
|
acc
|
142
|
in
|
143
|
pref [] (List.rev l)
|
144
|
|
145
|
let powerset_instances paths = List.map prefixes paths |> List.flatten
|
146
|
|
147
|
let pp_separated self mem fmt (paths, ptrs) =
|
148
|
fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])" self mem
|
149
|
(pp_comma_list ~pp_prologue:pp_print_comma' (pp_instance self))
|
150
|
paths
|
151
|
(pp_comma_list ~pp_prologue:pp_print_comma' pp_var_decl)
|
152
|
ptrs
|
153
|
|
154
|
let pp_separated' =
|
155
|
pp_comma_list
|
156
|
~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
|
157
|
~pp_epilogue:pp_print_cpar pp_var_decl
|
158
|
|
159
|
let pp_par pp fmt = fprintf fmt "(%a)" pp
|
160
|
|
161
|
let pp_forall pp_l pp_r fmt (l, r) =
|
162
|
fprintf fmt "@[<v 2>\\forall %a;@,%a@]" pp_l l pp_r r
|
163
|
|
164
|
let pp_exists pp_l pp_r fmt (l, r) =
|
165
|
fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r
|
166
|
|
167
|
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
|
168
|
|
169
|
let pp_different pp_l pp_r fmt (l, r) = fprintf fmt "%a != %a" pp_l l pp_r r
|
170
|
|
171
|
let pp_implies pp_l pp_r fmt (l, r) =
|
172
|
fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
|
173
|
|
174
|
let pp_and pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ && %a@]" pp_l l pp_r r
|
175
|
|
176
|
let pp_and_l pp_v fmt =
|
177
|
pp_print_list ~pp_open_box:pp_open_vbox0
|
178
|
~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
|
179
|
pp_v fmt
|
180
|
|
181
|
let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ || %a@]" pp_l l pp_r r
|
182
|
|
183
|
let pp_or_l pp_v fmt =
|
184
|
pp_print_list ~pp_open_box:pp_open_vbox0
|
185
|
~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
|
186
|
pp_v fmt
|
187
|
|
188
|
let pp_not pp fmt = fprintf fmt "!%a" pp
|
189
|
|
190
|
let pp_valid pp =
|
191
|
pp_and_l
|
192
|
(* pp_print_list *)
|
193
|
(* ~pp_sep:pp_print_cut *)
|
194
|
(fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
|
195
|
|
196
|
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
|
197
|
|
198
|
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
|
199
|
fprintf fmt "(%a @[<hov>? %a@ : %a)@]" pp_c c pp_t t pp_f f
|
200
|
|
201
|
let pp_paren pp fmt v = fprintf fmt "(%a)" pp v
|
202
|
|
203
|
let pp_initialization pp_mem fmt (name, mem) =
|
204
|
fprintf fmt "%s_initialization(%a)" name pp_mem mem
|
205
|
|
206
|
let pp_initialization' = pp_initialization pp_print_string
|
207
|
|
208
|
let pp_local m =
|
209
|
pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
|
210
|
|
211
|
let pp_locals m =
|
212
|
pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)
|
213
|
|
214
|
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
|
215
|
|
216
|
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
|
217
|
if Types.is_real_type typ && !Options.mpfr then assert false
|
218
|
(* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
|
219
|
else pp_equal pp_l pp_r fmt (var_name, value)
|
220
|
|
221
|
let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
|
222
|
(var_type, var_name, value) =
|
223
|
let depth = expansion_depth value in
|
224
|
let loop_vars = mk_loop_variables m var_type depth in
|
225
|
let reordered_loop_vars = reorder_loop_variables loop_vars in
|
226
|
let aux typ fmt vars =
|
227
|
match vars with
|
228
|
| [] ->
|
229
|
pp_basic_assign_spec
|
230
|
(pp_value_suffix ~indirect:indirect_l m self_l var_type loop_vars
|
231
|
pp_var_l)
|
232
|
(pp_value_suffix ~indirect:indirect_r m self_r var_type loop_vars
|
233
|
pp_var_r)
|
234
|
fmt typ var_name value
|
235
|
| (_d, LVar _i) :: _q ->
|
236
|
assert false
|
237
|
(* let typ' = Types.array_element_type typ in
|
238
|
* fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
239
|
* i i i pp_c_dimension d i
|
240
|
* (aux typ') q *)
|
241
|
| (_d, LInt _r) :: _q ->
|
242
|
assert false
|
243
|
(* let typ' = Types.array_element_type typ in
|
244
|
* let szl = Utils.enumerate (Dimension.size_const_dimension d) in
|
245
|
* fprintf fmt "@[<v 2>{@,%a@]@,}"
|
246
|
* (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
|
247
|
| _ ->
|
248
|
assert false
|
249
|
in
|
250
|
reset_loop_counter ();
|
251
|
aux var_type fmt reordered_loop_vars
|
252
|
|
253
|
let pp_nothing fmt () = pp_print_string fmt "\\nothing"
|
254
|
|
255
|
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
|
256
|
fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])" name
|
257
|
(pp_print_option pp_print_int)
|
258
|
i pp_mem mem pp_self self
|
259
|
|
260
|
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
|
261
|
pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt
|
262
|
(mp.mpname.node_id, mem, self)
|
263
|
|
264
|
let pp_memory_pack_aux' ?i fmt =
|
265
|
pp_memory_pack_aux ?i pp_print_string pp_print_string fmt
|
266
|
|
267
|
let pp_memory_pack' fmt = pp_memory_pack pp_print_string pp_print_string fmt
|
268
|
|
269
|
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt
|
270
|
(name, inputs, locals, outputs, mem_in, mem_out) =
|
271
|
let stateless = fst (get_stateless_status m) in
|
272
|
fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])" name
|
273
|
(pp_print_option pp_print_int)
|
274
|
i
|
275
|
(fun fmt -> if not stateless then pp_mem_in fmt mem_in)
|
276
|
(pp_comma_list
|
277
|
~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
|
278
|
pp_input)
|
279
|
inputs
|
280
|
(pp_print_option (fun fmt _ ->
|
281
|
pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
|
282
|
i
|
283
|
(fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
|
284
|
(pp_comma_list ~pp_prologue:pp_print_comma pp_output)
|
285
|
outputs
|
286
|
|
287
|
let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt
|
288
|
(t, mem_in, mem_out) =
|
289
|
pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_input pp_output fmt
|
290
|
(t.tname.node_id, t.tinputs, t.tlocals, t.toutputs, mem_in, mem_out)
|
291
|
|
292
|
let pp_transition_aux' ?i m =
|
293
|
pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl
|
294
|
|
295
|
let pp_transition_aux'' ?i m =
|
296
|
pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
|
297
|
|
298
|
let pp_transition' m =
|
299
|
pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl
|
300
|
|
301
|
let pp_transition'' m =
|
302
|
pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
|
303
|
|
304
|
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
|
305
|
fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in
|
306
|
pp_mem_out mem_out
|
307
|
|
308
|
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
|
309
|
|
310
|
let pp_functional_update mems fmt mem =
|
311
|
let rec aux fmt mems =
|
312
|
match mems with
|
313
|
| [] ->
|
314
|
pp_print_string fmt mem
|
315
|
| x :: mems ->
|
316
|
fprintf fmt "{ @[<hov>%a@ \\with ._reg.%s = %s@] }" aux mems x x
|
317
|
in
|
318
|
aux fmt
|
319
|
(* if Utils.ISet.is_empty mems then
|
320
|
* pp_print_string fmt mem
|
321
|
* else
|
322
|
* fprintf fmt "{ %s @[<hov>\\with %a@] }"
|
323
|
* mem
|
324
|
* (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
|
325
|
* (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
|
326
|
(Utils.ISet.elements mems)
|
327
|
|
328
|
module PrintSpec = struct
|
329
|
type mode =
|
330
|
| MemoryPackMode
|
331
|
| TransitionMode
|
332
|
| TransitionFootprintMode
|
333
|
| ResetIn
|
334
|
| ResetOut
|
335
|
| InstrMode of ident
|
336
|
|
337
|
let pp_reg mem fmt = function
|
338
|
| ResetFlag ->
|
339
|
fprintf fmt "%s.%s" mem reset_flag_name
|
340
|
| StateVar x ->
|
341
|
fprintf fmt "%s.%a" mem pp_var_decl x
|
342
|
|
343
|
let pp_expr :
|
344
|
type a.
|
345
|
?output:bool ->
|
346
|
machine_t ->
|
347
|
ident ->
|
348
|
formatter ->
|
349
|
(value_t, a) expression_t ->
|
350
|
unit =
|
351
|
fun ?(output = false) m mem fmt -> function
|
352
|
| Val v ->
|
353
|
pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v
|
354
|
| Tag t ->
|
355
|
pp_print_string fmt t
|
356
|
| Var v ->
|
357
|
pp_var_decl fmt v
|
358
|
| Memory r ->
|
359
|
pp_reg mem fmt r
|
360
|
|
361
|
let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
|
362
|
let output, mem_update =
|
363
|
match mode with
|
364
|
| InstrMode _ ->
|
365
|
true, false
|
366
|
| TransitionFootprintMode ->
|
367
|
false, true
|
368
|
| _ ->
|
369
|
false, false
|
370
|
in
|
371
|
let pp_expr :
|
372
|
type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
|
373
|
fun ?output fmt e -> pp_expr ?output m mem_out fmt e
|
374
|
in
|
375
|
match p with
|
376
|
| Transition (f, inst, i, inputs, locals, outputs, r, mems) ->
|
377
|
let pp_mem_in, pp_mem_out =
|
378
|
match inst with
|
379
|
| None ->
|
380
|
( pp_print_string,
|
381
|
if mem_update then pp_functional_update mems else pp_print_string )
|
382
|
| Some inst ->
|
383
|
( (fun fmt mem_in ->
|
384
|
if r then pp_print_string fmt mem_in
|
385
|
else pp_access' fmt (mem_in, inst)),
|
386
|
fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
|
387
|
in
|
388
|
pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output) fmt
|
389
|
(f, inputs, locals, outputs, mem_in', mem_out')
|
390
|
| Reset (_f, inst, r) ->
|
391
|
pp_ite
|
392
|
(pp_c_val m mem_in (pp_c_var_read m))
|
393
|
(pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
|
394
|
(pp_equal pp_print_string pp_access')
|
395
|
fmt
|
396
|
(r, (mem_out, 1), (mem_out, (mem_in, inst)))
|
397
|
| MemoryPack (f, inst, i) ->
|
398
|
let pp_mem, pp_self =
|
399
|
match inst with
|
400
|
| None ->
|
401
|
pp_print_string, pp_print_string
|
402
|
| Some inst ->
|
403
|
( (fun fmt mem -> pp_access' fmt (mem, inst)),
|
404
|
fun fmt self -> pp_indirect' fmt (self, inst) )
|
405
|
in
|
406
|
pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
|
407
|
| ResetCleared f ->
|
408
|
pp_reset_cleared' fmt (f, mem_in, mem_out)
|
409
|
(* fprintf fmt "ResetCleared_%a" pp_print_string f *)
|
410
|
| Initialization ->
|
411
|
()
|
412
|
|
413
|
let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
|
414
|
|
415
|
let val_of_expr : type a. (value_t, a) expression_t -> value_t = function
|
416
|
| Val v ->
|
417
|
v
|
418
|
| Tag t ->
|
419
|
id_to_tag t
|
420
|
| Var v ->
|
421
|
vdecl_to_val v
|
422
|
| Memory (StateVar v) ->
|
423
|
vdecl_to_val v
|
424
|
| Memory ResetFlag ->
|
425
|
vdecl_to_val reset_flag
|
426
|
|
427
|
let find_arrow m =
|
428
|
try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
|
429
|
with Not_found ->
|
430
|
eprintf "Internal error: arrow not found";
|
431
|
raise Not_found
|
432
|
|
433
|
let pp_spec mode m fmt f =
|
434
|
let rec pp_spec mode fmt f =
|
435
|
let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
|
436
|
let self = mk_self m in
|
437
|
let mem = mk_mem m in
|
438
|
let mem_in = mk_mem_in m in
|
439
|
let mem_out = mk_mem_out m in
|
440
|
let mem_reset = mk_mem_reset m in
|
441
|
match mode with
|
442
|
| MemoryPackMode ->
|
443
|
self, self, true, mem, mem, false
|
444
|
| TransitionMode ->
|
445
|
mem_in, mem_in, false, mem_out, mem_out, false
|
446
|
| TransitionFootprintMode ->
|
447
|
mem_in, mem_in, false, mem_out, mem_out, false
|
448
|
| ResetIn ->
|
449
|
mem_reset, mem_reset, false, mem_out, mem_out, false
|
450
|
| ResetOut ->
|
451
|
mem_in, mem_in, false, mem_reset, mem_reset, false
|
452
|
| InstrMode self ->
|
453
|
let mem = "*" ^ mem in
|
454
|
fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
|
455
|
self, flush_str_formatter (), false, mem, mem, false
|
456
|
in
|
457
|
let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
|
458
|
fun fmt e -> pp_expr m mem_out fmt e
|
459
|
in
|
460
|
let pp_spec' = pp_spec mode in
|
461
|
match f with
|
462
|
| True ->
|
463
|
pp_true fmt ()
|
464
|
| False ->
|
465
|
pp_false fmt ()
|
466
|
| Equal (a, b) ->
|
467
|
pp_assign_spec m mem_out
|
468
|
(pp_c_var_read ~test_output:false m)
|
469
|
indirect_l mem_in
|
470
|
(pp_c_var_read ~test_output:false m)
|
471
|
indirect_r fmt
|
472
|
(type_of_l_value a, val_of_expr a, val_of_expr b)
|
473
|
| And fs ->
|
474
|
pp_and_l pp_spec' fmt fs
|
475
|
| Or fs ->
|
476
|
pp_or_l pp_spec' fmt fs
|
477
|
| Imply (a, b) ->
|
478
|
pp_par (pp_implies pp_spec' pp_spec') fmt (a, b)
|
479
|
| Exists (xs, a) ->
|
480
|
pp_exists (pp_locals m) pp_spec' fmt (xs, a)
|
481
|
| Forall (xs, a) ->
|
482
|
pp_forall (pp_locals m) pp_spec' fmt (xs, a)
|
483
|
| Ternary (e, a, b) ->
|
484
|
pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
|
485
|
| Predicate p ->
|
486
|
pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
|
487
|
| StateVarPack ResetFlag ->
|
488
|
let r = vdecl_to_val reset_flag in
|
489
|
pp_assign_spec m mem_out
|
490
|
(pp_c_var_read ~test_output:false m)
|
491
|
indirect_l mem_in
|
492
|
(pp_c_var_read ~test_output:false m)
|
493
|
indirect_r fmt
|
494
|
(Type_predef.type_bool, r, r)
|
495
|
| StateVarPack (StateVar v) ->
|
496
|
let v' = vdecl_to_val v in
|
497
|
let inst = find_arrow m in
|
498
|
pp_par
|
499
|
(pp_implies
|
500
|
(pp_not (pp_initialization pp_access'))
|
501
|
(pp_assign_spec m mem_out
|
502
|
(pp_c_var_read ~test_output:false m)
|
503
|
indirect_l mem_in
|
504
|
(pp_c_var_read ~test_output:false m)
|
505
|
indirect_r))
|
506
|
fmt
|
507
|
((Arrow.arrow_id, (mem_out, inst)), (v.var_type, v', v'))
|
508
|
| ExistsMem (f, rc, tr) ->
|
509
|
pp_exists
|
510
|
(pp_machine_decl' ~ghost:true)
|
511
|
(pp_and (pp_spec ResetOut) (pp_spec ResetIn))
|
512
|
fmt
|
513
|
((f, mk_mem_reset m), (rc, tr))
|
514
|
in
|
515
|
match mode with
|
516
|
| TransitionFootprintMode ->
|
517
|
let mem_in = mk_mem_in m in
|
518
|
let mem_out = mk_mem_out m in
|
519
|
pp_forall
|
520
|
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
|
521
|
(pp_spec mode) fmt
|
522
|
((m.mname.node_id, [ mem_in; mem_out ]), f)
|
523
|
| _ ->
|
524
|
pp_spec mode fmt f
|
525
|
end
|
526
|
|
527
|
let pp_predicate pp_l pp_r fmt (l, r) =
|
528
|
fprintf fmt "@[<v 2>predicate %a =@,%a;@]" pp_l l pp_r r
|
529
|
|
530
|
let pp_lemma pp_l pp_r fmt (l, r) =
|
531
|
fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r
|
532
|
|
533
|
let pp_mem_valid_def fmt m =
|
534
|
if not (fst (get_stateless_status m)) then
|
535
|
let name = m.mname.node_id in
|
536
|
let self = mk_self m in
|
537
|
pp_acsl
|
538
|
(pp_predicate
|
539
|
(pp_mem_valid (pp_machine_decl pp_ptr))
|
540
|
(pp_and
|
541
|
(pp_and_l (fun fmt (inst, (td, _)) ->
|
542
|
if Arrow.td_is_arrow td then
|
543
|
pp_valid pp_indirect' fmt [ self, inst ]
|
544
|
else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
|
545
|
(pp_valid pp_print_string)))
|
546
|
fmt
|
547
|
((name, (name, self)), (m.minstances, [ self ]))
|
548
|
|
549
|
let pp_memory_pack_def m fmt mp =
|
550
|
let name = mp.mpname.node_id in
|
551
|
let self = mk_self m in
|
552
|
let mem = mk_mem m in
|
553
|
pp_acsl
|
554
|
(pp_predicate
|
555
|
(pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
|
556
|
(PrintSpec.pp_spec MemoryPackMode m))
|
557
|
fmt
|
558
|
((mp, (name, mem), (name, self)), mp.mpformula)
|
559
|
|
560
|
let print_machine_ghost_struct fmt m =
|
561
|
pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
|
562
|
|
563
|
let pp_memory_pack_defs fmt m =
|
564
|
if not (fst (get_stateless_status m)) then
|
565
|
fprintf fmt "%a@,%a" print_machine_ghost_struct m
|
566
|
(pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
|
567
|
(pp_memory_pack_def m))
|
568
|
m.mspec.mmemory_packs
|
569
|
|
570
|
let pp_transition_def m fmt t =
|
571
|
let name = t.tname.node_id in
|
572
|
let mem_in = mk_mem_in m in
|
573
|
let mem_out = mk_mem_out m in
|
574
|
pp_acsl
|
575
|
(pp_predicate
|
576
|
(pp_transition m
|
577
|
(pp_machine_decl' ~ghost:true)
|
578
|
(pp_machine_decl' ~ghost:true)
|
579
|
(pp_local m) (pp_local m))
|
580
|
(PrintSpec.pp_spec TransitionMode m))
|
581
|
fmt
|
582
|
((t, (name, mem_in), (name, mem_out)), t.tformula)
|
583
|
|
584
|
let pp_transition_defs fmt m =
|
585
|
pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
|
586
|
(pp_transition_def m) fmt m.mspec.mtransitions
|
587
|
|
588
|
let pp_transition_footprint fmt t =
|
589
|
fprintf fmt "%s_transition%a_footprint" t.tname.node_id
|
590
|
(pp_print_option pp_print_int)
|
591
|
t.tindex
|
592
|
|
593
|
let pp_transition_footprint_lemma m fmt t =
|
594
|
let open Utils.ISet in
|
595
|
let name = t.tname.node_id in
|
596
|
let mems =
|
597
|
diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint
|
598
|
in
|
599
|
let memories =
|
600
|
List.map
|
601
|
(fun v -> { v with var_type = { v.var_type with tid = -1 } })
|
602
|
(List.filter (fun v -> not (mem v.var_id t.tfootprint)) m.mmemory)
|
603
|
in
|
604
|
if not (is_empty mems) then
|
605
|
pp_acsl
|
606
|
(pp_lemma pp_transition_footprint
|
607
|
(PrintSpec.pp_spec TransitionFootprintMode m))
|
608
|
fmt
|
609
|
( t,
|
610
|
Forall
|
611
|
( memories @ t.tinputs @ t.tlocals @ t.toutputs,
|
612
|
Imply
|
613
|
( Spec_common.mk_transition ?i:t.tindex name
|
614
|
(vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
|
615
|
(vdecls_to_vals t.toutputs),
|
616
|
Spec_common.mk_transition ~mems ?i:t.tindex name
|
617
|
(vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
|
618
|
(vdecls_to_vals t.toutputs) ) ) )
|
619
|
|
620
|
let pp_transition_footprint_lemmas fmt m =
|
621
|
pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
|
622
|
(pp_transition_footprint_lemma m)
|
623
|
fmt
|
624
|
(List.filter
|
625
|
(fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
|
626
|
m.mspec.mtransitions)
|
627
|
|
628
|
let pp_initialization_def fmt m =
|
629
|
if not (fst (get_stateless_status m)) then
|
630
|
let name = m.mname.node_id in
|
631
|
let mem_in = mk_mem_in m in
|
632
|
pp_acsl
|
633
|
(pp_predicate
|
634
|
(pp_initialization (pp_machine_decl' ~ghost:true))
|
635
|
(pp_and_l (fun fmt (i, (td, _)) ->
|
636
|
if Arrow.td_is_arrow td then
|
637
|
pp_initialization pp_access' fmt (node_name td, (mem_in, i))
|
638
|
else
|
639
|
pp_equal
|
640
|
(pp_reset_flag ~indirect:false pp_access')
|
641
|
pp_print_int fmt
|
642
|
((mem_in, i), 1))))
|
643
|
fmt
|
644
|
((name, (name, mem_in)), m.minstances)
|
645
|
|
646
|
let pp_reset_cleared_def fmt m =
|
647
|
if not (fst (get_stateless_status m)) then
|
648
|
let name = m.mname.node_id in
|
649
|
let mem_in = mk_mem_in m in
|
650
|
let mem_out = mk_mem_out m in
|
651
|
pp_acsl
|
652
|
(pp_predicate
|
653
|
(pp_reset_cleared
|
654
|
(pp_machine_decl' ~ghost:true)
|
655
|
(pp_machine_decl' ~ghost:true))
|
656
|
(pp_ite
|
657
|
(pp_reset_flag' ~indirect:false)
|
658
|
(pp_and
|
659
|
(pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
|
660
|
pp_initialization')
|
661
|
(pp_equal pp_print_string pp_print_string)))
|
662
|
fmt
|
663
|
( (name, (name, mem_in), (name, mem_out)),
|
664
|
(mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
|
665
|
|
666
|
let pp_at pp_p fmt (p, l) = fprintf fmt "\\at(%a, %s)" pp_p p l
|
667
|
|
668
|
let label_pre = "Pre"
|
669
|
|
670
|
let pp_at_pre pp_p fmt p = pp_at pp_p fmt (p, label_pre)
|
671
|
|
672
|
let pp_register_chain ?(indirect = true) ptr =
|
673
|
pp_print_list
|
674
|
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
|
675
|
~pp_epilogue:(fun fmt () ->
|
676
|
fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
|
677
|
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
|
678
|
(fun fmt (i, _) -> pp_print_string fmt i)
|
679
|
|
680
|
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
|
681
|
pp_print_list
|
682
|
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
|
683
|
~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
|
684
|
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
|
685
|
(fun fmt (i, _) -> pp_print_string fmt i)
|
686
|
fmt mems
|
687
|
|
688
|
let pp_arrow_reset_ghost mem fmt inst =
|
689
|
fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
|
690
|
|
691
|
module GhostProto : MODIFIERS_GHOST_PROTO = struct
|
692
|
let pp_ghost_parameters ?(cut = true) fmt vs =
|
693
|
fprintf fmt "%a%a"
|
694
|
(if cut then pp_print_cut else pp_print_nothing)
|
695
|
()
|
696
|
(pp_acsl_line'
|
697
|
(pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
|
698
|
vs
|
699
|
end
|
700
|
|
701
|
module HdrMod = struct
|
702
|
module GhostProto = GhostProto
|
703
|
|
704
|
let print_machine_decl_prefix _ _ = ()
|
705
|
|
706
|
let pp_import_arrow fmt () =
|
707
|
fprintf fmt "#include \"%s/arrow_spec.h%s\""
|
708
|
(Arrow.arrow_top_decl ()).top_decl_owner
|
709
|
(if !Options.cpp then "pp" else "")
|
710
|
end
|
711
|
|
712
|
module SrcMod = struct
|
713
|
module GhostProto = GhostProto
|
714
|
|
715
|
let pp_predicates (* dependencies *) fmt machines =
|
716
|
let pp_preds comment pp =
|
717
|
pp_print_list ~pp_open_box:pp_open_vbox0
|
718
|
~pp_prologue:(pp_print_endcut comment) pp ~pp_epilogue:pp_print_cutcut
|
719
|
in
|
720
|
fprintf fmt "%a%a%a%a%a%a"
|
721
|
(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
|
722
|
machines
|
723
|
(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
|
724
|
machines
|
725
|
(pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
|
726
|
machines
|
727
|
(pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
|
728
|
machines
|
729
|
(pp_preds "/* ACSL transition annotations */" pp_transition_defs)
|
730
|
machines
|
731
|
(pp_preds "/* ACSL transition memory footprints lemmas */"
|
732
|
pp_transition_footprint_lemmas)
|
733
|
machines
|
734
|
|
735
|
let pp_clear_reset_spec fmt self mem m =
|
736
|
let name = m.mname.node_id in
|
737
|
let arws, narws =
|
738
|
List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
|
739
|
in
|
740
|
let mk_insts = List.map (fun x -> [ x ]) in
|
741
|
pp_acsl_cut
|
742
|
(fun fmt () ->
|
743
|
fprintf fmt
|
744
|
"%a@,\
|
745
|
%a@,\
|
746
|
%a@,\
|
747
|
%a@,\
|
748
|
%a@,\
|
749
|
%a@,\
|
750
|
%a@,\
|
751
|
%a@,\
|
752
|
%a@,\
|
753
|
%a@,\
|
754
|
@[<v 2>behavior reset:@;\
|
755
|
%a@,\
|
756
|
%a@]@,\
|
757
|
@[<v 2>behavior no_reset:@;\
|
758
|
%a@,\
|
759
|
%a@]@,\
|
760
|
complete behaviors;@,\
|
761
|
disjoint behaviors;"
|
762
|
(pp_requires pp_mem_valid')
|
763
|
(name, self)
|
764
|
(pp_requires (pp_separated self mem))
|
765
|
(mk_insts m.minstances, [])
|
766
|
(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
|
767
|
(name, mem, self)
|
768
|
(pp_ensures
|
769
|
(pp_memory_pack_aux
|
770
|
~i:(List.length m.mspec.mmemory_packs - 2)
|
771
|
pp_ptr pp_print_string))
|
772
|
(name, mem, self)
|
773
|
(pp_assigns pp_reset_flag')
|
774
|
[ self ]
|
775
|
(pp_assigns (pp_register_chain self))
|
776
|
(mk_insts arws)
|
777
|
(pp_assigns (pp_reset_flag_chain self))
|
778
|
(mk_insts narws)
|
779
|
(pp_assigns pp_reset_flag')
|
780
|
[ mem ]
|
781
|
(pp_assigns (pp_register_chain ~indirect:false mem))
|
782
|
(mk_insts arws)
|
783
|
(pp_assigns (pp_reset_flag_chain ~indirect:false mem))
|
784
|
(mk_insts narws)
|
785
|
(pp_assumes (pp_equal pp_reset_flag' pp_print_int))
|
786
|
(mem, 1)
|
787
|
(pp_ensures (pp_initialization pp_ptr))
|
788
|
(name, mem)
|
789
|
(pp_assumes (pp_equal pp_reset_flag' pp_print_int))
|
790
|
(mem, 0)
|
791
|
(pp_ensures (pp_equal pp_ptr (pp_old pp_ptr)))
|
792
|
(mem, mem))
|
793
|
fmt ()
|
794
|
|
795
|
let pp_set_reset_spec fmt self mem m =
|
796
|
let name = m.mname.node_id in
|
797
|
pp_acsl_cut
|
798
|
(fun fmt () ->
|
799
|
fprintf fmt "%a@,%a@,%a"
|
800
|
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
|
801
|
(name, mem, self)
|
802
|
(pp_ensures (pp_equal pp_reset_flag' pp_print_int))
|
803
|
(mem, 1)
|
804
|
(pp_assigns pp_reset_flag')
|
805
|
[ self; mem ])
|
806
|
fmt ()
|
807
|
|
808
|
let pp_step_spec fmt machines self mem m =
|
809
|
let name = m.mname.node_id in
|
810
|
let insts = instances machines m in
|
811
|
let insts' = powerset_instances insts in
|
812
|
let insts'' =
|
813
|
List.(
|
814
|
filter
|
815
|
(fun l -> l <> [])
|
816
|
(map (filter (fun (_, (td, _)) -> not (Arrow.td_is_arrow td))) insts))
|
817
|
in
|
818
|
let inputs = m.mstep.step_inputs in
|
819
|
let outputs = m.mstep.step_outputs in
|
820
|
pp_acsl_cut
|
821
|
(fun fmt () ->
|
822
|
if fst (get_stateless_status m) then
|
823
|
fprintf fmt "%a@,%a@,%a@,%a"
|
824
|
(pp_requires (pp_valid pp_var_decl))
|
825
|
outputs
|
826
|
(pp_requires pp_separated')
|
827
|
outputs (pp_assigns pp_ptr_decl) outputs
|
828
|
(pp_ensures (pp_transition_aux'' m))
|
829
|
(name, inputs, [], outputs, "", "")
|
830
|
else
|
831
|
fprintf fmt
|
832
|
"%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
|
833
|
(pp_requires (pp_valid pp_var_decl))
|
834
|
outputs
|
835
|
(pp_requires pp_mem_valid')
|
836
|
(name, self)
|
837
|
(pp_requires (pp_separated self mem))
|
838
|
(insts', outputs)
|
839
|
(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
|
840
|
(name, mem, self)
|
841
|
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
|
842
|
(name, mem, self)
|
843
|
(pp_ensures
|
844
|
(pp_transition_aux m (pp_old pp_ptr) pp_ptr pp_var_decl
|
845
|
pp_ptr_decl))
|
846
|
(name, inputs, [], outputs, mem, mem)
|
847
|
(pp_assigns pp_ptr_decl) outputs
|
848
|
(pp_assigns (pp_reg self))
|
849
|
m.mmemory
|
850
|
(pp_assigns pp_reset_flag')
|
851
|
[ self ]
|
852
|
(pp_assigns (pp_memory self))
|
853
|
(memories insts')
|
854
|
(pp_assigns (pp_register_chain self))
|
855
|
insts
|
856
|
(pp_assigns (pp_reset_flag_chain self))
|
857
|
insts''
|
858
|
(pp_assigns (pp_reg mem))
|
859
|
m.mmemory
|
860
|
(pp_assigns pp_reset_flag')
|
861
|
[ mem ]
|
862
|
(pp_assigns (pp_memory ~indirect:false mem))
|
863
|
(memories insts')
|
864
|
(pp_assigns (pp_register_chain ~indirect:false mem))
|
865
|
insts
|
866
|
(pp_assigns (pp_reset_flag_chain ~indirect:false mem))
|
867
|
insts'')
|
868
|
fmt ()
|
869
|
|
870
|
let pp_ghost_instr_code m self fmt instr =
|
871
|
match instr.instr_desc with
|
872
|
| MStateAssign (x, v) ->
|
873
|
fprintf fmt "@,%a"
|
874
|
(pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m))))
|
875
|
(x, v)
|
876
|
| MResetAssign b ->
|
877
|
fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b
|
878
|
| MSetReset inst ->
|
879
|
let td, _ = List.assoc inst m.minstances in
|
880
|
if Arrow.td_is_arrow td then
|
881
|
fprintf fmt "@,%a;"
|
882
|
(pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self)))
|
883
|
inst
|
884
|
| _ ->
|
885
|
()
|
886
|
|
887
|
let pp_step_instr_spec m self mem fmt instr =
|
888
|
fprintf fmt "%a%a"
|
889
|
(pp_ghost_instr_code m mem)
|
890
|
instr
|
891
|
(pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
|
892
|
(pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
|
893
|
instr.instr_spec
|
894
|
|
895
|
let pp_ghost_parameter mem fmt inst =
|
896
|
GhostProto.pp_ghost_parameters ~cut:false fmt
|
897
|
(match inst with
|
898
|
| Some inst ->
|
899
|
[ (inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)) ]
|
900
|
| None ->
|
901
|
[ mem, pp_print_string ])
|
902
|
end
|
903
|
|
904
|
(**************************************************************************)
|
905
|
(* MAKEFILE *)
|
906
|
(**************************************************************************)
|
907
|
|
908
|
module MakefileMod = struct
|
909
|
let other_targets fmt basename _nodename dependencies =
|
910
|
fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
|
911
|
(* EACSL version of library file . c *)
|
912
|
fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
|
913
|
fprintf fmt
|
914
|
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
|
915
|
e-acsl -print -ocode %s_eacsl.c@."
|
916
|
basename basename;
|
917
|
fprintf fmt "@.";
|
918
|
fprintf fmt "@.";
|
919
|
|
920
|
(* EACSL version of library file . c + main .c *)
|
921
|
fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename
|
922
|
basename basename;
|
923
|
fprintf fmt
|
924
|
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
|
925
|
-then-on e-acsl -print -ocode %s_main_eacsl.i@."
|
926
|
basename basename basename;
|
927
|
(* Ugly hack to deal with eacsl bugs *)
|
928
|
fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
|
929
|
basename basename;
|
930
|
fprintf fmt "@.";
|
931
|
fprintf fmt "@.";
|
932
|
|
933
|
(* EACSL version of binary *)
|
934
|
fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
|
935
|
fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
|
936
|
basename;
|
937
|
(* compiling instrumented lib + main *)
|
938
|
C_backend_makefile.fprintf_dependencies fmt dependencies;
|
939
|
fprintf fmt
|
940
|
"\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
|
941
|
%s_main_eacsl.o %a@."
|
942
|
basename
|
943
|
(Utils.fprintf_list ~sep:" " (fun fmt dep ->
|
944
|
Format.fprintf fmt "%s.o" dep.name))
|
945
|
(C_backend_makefile.compiled_dependencies dependencies)
|
946
|
("${FRAMACEACSL}/e_acsl.c "
|
947
|
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
|
948
|
^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
|
949
|
basename
|
950
|
(Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
|
951
|
(C_backend_makefile.lib_dependencies dependencies);
|
952
|
fprintf fmt "@."
|
953
|
end
|
954
|
|
955
|
(* Local Variables: *)
|
956
|
(* compile-command:"make -C ../../.." *)
|
957
|
(* End: *)
|