Project

General

Profile

Download (20.9 KB) Statistics
| Branch: | Tag: | Revision:
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 Machine_code_common
17
open Corelang
18

    
19
(**************************************************************************)
20
(*     Printing spec for c *)
21

    
22
(**************************************************************************)
23
(* OLD STUFF ???
24

    
25

    
26
let pp_acsl_type var fmt t =
27
  let rec aux t pp_suffix =
28
  match (Types.repr t).Types.tdesc with
29
  | Types.Tclock t'       -> aux t' pp_suffix
30
  | Types.Tbool           -> fprintf fmt "int %s%a" var pp_suffix ()
31
  | Types.Treal           -> fprintf fmt "real %s%a" var pp_suffix ()
32
  | Types.Tint            -> fprintf fmt "int %s%a" var pp_suffix ()
33
  | Types.Tarray (d, t')  ->
34
    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
35
    aux t' pp_suffix'
36
  (* | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix *)
37
  (* | Types.Tconst ty       -> fprintf fmt "%s %s" ty var *)
38
  (* | Types.Tarrow (_, _)   -> fprintf fmt "void (\*%s)()" var *)
39
  | _                     -> eprintf "internal error: pp_acsl_type %a@." Types.print_ty t; assert false
40
  in aux t (fun fmt () -> ())
41

    
42
let pp_acsl_var_decl fmt id =
43
  pp_acsl_type id.var_id fmt id.var_type
44

    
45

    
46
let rec pp_eexpr is_output fmt eexpr = 
47
  let pp_eexpr = pp_eexpr is_output in
48
  match eexpr.eexpr_desc with
49
    | EExpr_const c -> Printers.pp_econst fmt c
50
    | EExpr_ident id -> 
51
      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
52
    | EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el
53
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
54
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
55
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
56
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
57
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
58
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
59
    | EExpr_merge (id, e1, e2) -> 
60
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
61
    | EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r
62
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e 
63
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e 
64

    
65

    
66
    (* | EExpr_whennot _ *)
67
    (* | EExpr_uclock _ *)
68
    (* | EExpr_dclock _ *)
69
    (* | EExpr_phclock _ -> assert false *)
70
and pp_eapp is_output fmt id e r =
71
  let pp_eexpr = pp_eexpr is_output in
72
  match r with
73
  | None ->
74
    (match id, e.eexpr_desc with
75
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
76
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
77
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
78
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
79
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
80
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
81
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
82
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
83
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
84
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
85
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
86
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
87
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
88
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
89
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
90
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
91
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
92
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
93
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
94
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
95

    
96
let pp_ensures is_output fmt e =
97
  match e with
98
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e
99
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args
100

    
101
let pp_acsl_spec outputs fmt spec =
102
  let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
103
  let pp_eexpr = pp_eexpr is_output in
104
  fprintf fmt "@[<v 2>/*@@ ";
105
  Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
106
  Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;
107
  fprintf fmt "@ ";
108
  (* fprintf fmt "assigns *self%t%a;@ "  *)
109
  (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
110
  (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
111
  Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
112
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
113
      name
114
      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
115
      (Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires
116
  ) fmt spec.behaviors;
117
  fprintf fmt "@]@ */@.";
118
  ()
119

    
120

    
121

    
122

    
123
let print_machine_decl_prefix fmt m =
124
   (* Print specification if any *)
125
   (match m.mspec with
126
  | None -> ()
127
  | Some spec -> 
128
    pp_acsl_spec m.mstep.step_outputs fmt spec
129
  )
130

    
131
  *)
132

    
133
   (* TODO ACSL
134
   Return updates machines (eg with local annotations) and acsl preamble *)
135
let preprocess_acsl machines = machines, []
136
                          
137
(* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *)
138
let pp_acsl_preamble fmt _preamble =
139
  Format.fprintf fmt "";
140
  ()
141

    
142
let pp_spec pp fmt =
143
  fprintf fmt "@[<v>/*%@@[<v>@,%a@]@,*/@]" pp
144

    
145
let pp_spec_cut pp fmt =
146
  fprintf fmt "%a@," (pp_spec pp)
147

    
148
let pp_spec_line pp fmt =
149
  fprintf fmt "//%@ %a@," pp
150

    
151
let pp_requires pp_req fmt =
152
  fprintf fmt "requires %a;" pp_req
153

    
154
let pp_ensures pp_ens fmt =
155
  fprintf fmt "ensures %a;" pp_ens
156

    
157
let pp_assigns pp_asg fmt =
158
  fprintf fmt "assigns %a;" pp_asg
159

    
160
let pp_ghost pp_gho fmt =
161
  fprintf fmt "ghost %a" pp_gho
162

    
163
let pp_assert pp_ast fmt =
164
  fprintf fmt "assert %a;" pp_ast
165

    
166
let pp_mem_valid pp_var fmt (name, var) =
167
  fprintf fmt "%s_valid(%a)" name pp_var var
168

    
169
let pp_mem_valid' = pp_mem_valid pp_print_string
170

    
171
let pp_indirect pp_field fmt (ptr, field) =
172
  fprintf fmt "%s->%a" ptr pp_field field
173

    
174
let pp_indirect' = pp_indirect pp_print_string
175

    
176
let pp_access pp_field fmt (stru, field) =
177
  fprintf fmt "%s.%a" stru pp_field field
178

    
179
let pp_access' = pp_access pp_print_string
180

    
181
let pp_inst self fmt (name, _) =
182
  pp_indirect' fmt (self, name)
183

    
184
let pp_true fmt () =
185
  pp_print_string fmt "\\true"
186

    
187
let pp_separated self fmt =
188
  fprintf fmt "\\separated(@[<h>%s%a@])"
189
    self
190
    (pp_print_list
191
       ~pp_prologue:pp_print_comma
192
       ~pp_sep:pp_print_comma
193
       (pp_inst self))
194

    
195
let pp_forall pp_l pp_r fmt (l, r) =
196
  fprintf fmt "@[<v 2>\\forall %a;@,%a@]"
197
    pp_l l
198
    pp_r r
199

    
200
let pp_valid =
201
  pp_print_parenthesized
202
    ~pp_nil:pp_true
203
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\valid")
204

    
205
let pp_equal pp_l pp_r fmt (l, r) =
206
  fprintf fmt "%a == %a"
207
    pp_l l
208
    pp_r r
209

    
210
let pp_implies pp_l pp_r fmt (l, r) =
211
  fprintf fmt "%a ==>@ %a"
212
    pp_l l
213
    pp_r r
214

    
215
let pp_and pp_l pp_r fmt (l, r) =
216
  fprintf fmt "%a @ && %a"
217
    pp_l l
218
    pp_r r
219

    
220
let pp_and_l pp_v fmt =
221
  pp_print_list
222
    ~pp_open_box:pp_open_vbox0
223
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
224
    pp_v
225
    fmt
226

    
227
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
228
  fprintf fmt "%a @[<hov>? %a@ : %a@]"
229
    pp_c c
230
    pp_t t
231
    pp_f f
232

    
233
let pp_machine_decl fmt (id, mem_type, var) =
234
  fprintf fmt "struct %s_%s %s" id mem_type var
235

    
236
let pp_mem_ghost pp_mem pp_self ?i fmt (name, mem, self) =
237
  fprintf fmt "%s_ghost%a(@[<hov>%a,@ %a@])"
238
    name
239
    (pp_print_option pp_print_int) i
240
    pp_mem mem
241
    pp_self self
242

    
243
let pp_mem_ghost' = pp_mem_ghost pp_print_string pp_print_string
244

    
245
let pp_mem_init pp_mem fmt (name, mem) =
246
  fprintf fmt "%s_init(%a)" name pp_mem mem
247

    
248
let pp_mem_init' = pp_mem_init pp_print_string
249

    
250
let pp_var_decl fmt v =
251
  pp_print_string fmt v.var_id
252

    
253
let pp_ptr_decl fmt v =
254
  fprintf fmt "*%s" v.var_id
255

    
256
let pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_input pp_output fmt
257
    (name, inputs, outputs, mem_in, mem_out) =
258
  fprintf fmt "%s_trans%a(@[<hov>%a,@ %a%a%a@])"
259
    name
260
    (pp_print_option pp_print_int) i
261
    pp_mem_in mem_in
262
    (pp_print_list
263
       ~pp_epilogue:pp_print_comma
264
       ~pp_sep:pp_print_comma
265
       pp_input) inputs
266
    pp_mem_out mem_out
267
    (pp_print_list
268
       ~pp_prologue:pp_print_comma
269
       ~pp_sep:pp_print_comma
270
       pp_output) outputs
271

    
272
let pp_mem_trans ?i pp_mem_in pp_mem_out fmt (m, mem_in, mem_out) =
273
  pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_var_decl pp_ptr_decl fmt
274
    (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, mem_in, mem_out)
275

    
276
let pp_mem_trans' ?i fmt = pp_mem_trans ?i pp_print_string pp_print_string fmt
277

    
278
let pp_nothing fmt () =
279
  pp_print_string fmt "\\nothing"
280

    
281
let pp_predicate pp_l pp_r fmt (l, r) =
282
  fprintf fmt "@[<v 2>predicate %a =@,%a;@]"
283
    pp_l l
284
    pp_r r
285

    
286
let print_machine_valid_predicate fmt m =
287
  if not (fst (Machine_code_common.get_stateless_status m)) then
288
    let name = m.mname.node_id in
289
    let self = mk_self m in
290
    pp_spec
291
      (pp_predicate
292
         (pp_mem_valid pp_machine_decl)
293
         (pp_and
294
            (pp_and_l (fun fmt (_, (td, _) as inst) ->
295
                 pp_mem_valid (pp_inst self) fmt (node_name td, inst)))
296
            (pp_valid pp_print_string)))
297
      fmt
298
      ((name, (name, "mem", "*" ^ self)),
299
       (m.minstances, [self]))
300

    
301
let print_machine_ghost_simulation_aux ?i m pp fmt v =
302
  let name = m.mname.node_id in
303
  let self = mk_self m in
304
  let mem = mk_mem m in
305
  pp_spec
306
    (pp_predicate
307
       (pp_mem_ghost pp_machine_decl pp_machine_decl ?i)
308
       pp)
309
    fmt
310
    ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
311
     v)
312

    
313
let print_machine_ghost_simulation dependencies m fmt i instr =
314
  let name = m.mname.node_id in
315
  let self = mk_self m in
316
  let mem = mk_mem m in
317
  let prev_ghost fmt () = pp_mem_ghost' ~i fmt (name, mem, self) in
318
  let pred pp v = pp_and prev_ghost pp fmt ((), v) in
319
  print_machine_ghost_simulation_aux m
320
    (fun fmt -> function
321
       | MStateAssign (m, _) ->
322
         pred
323
           (pp_equal
324
              (pp_access (pp_access pp_var_decl))
325
              (pp_indirect (pp_access pp_var_decl)))
326
           ((mem, ("_reg", m)),
327
            (self, ("_reg", m)))
328
       | MStep ([i0], i, vl)
329
         when Basic_library.is_value_internal_fun
330
             (mk_val (Fun (i, vl)) i0.var_type)  ->
331
         prev_ghost fmt ()
332
       | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
333
         prev_ghost fmt ()
334
       | MStep ([_], i, _) when has_c_prototype i dependencies ->
335
         prev_ghost fmt ()
336
       | MStep (_, i, _)
337
       | MReset i ->
338
         begin try
339
             let n, _ = List.assoc i m.minstances in
340
             pred
341
               (pp_mem_ghost pp_access' pp_indirect')
342
               (node_name n, (mem, i), (self, i))
343
           with Not_found -> prev_ghost fmt ()
344
         end
345
       | _ -> prev_ghost fmt ())
346
    ~i:(i+1) fmt instr.instr_desc
347

    
348
let print_machine_ghost_struct fmt m =
349
  pp_spec (pp_ghost (print_machine_struct ~ghost:true)) fmt m
350

    
351
let print_machine_ghost_simulations dependencies fmt m =
352
  if not (fst (Machine_code_common.get_stateless_status m)) then
353
    let name = m.mname.node_id in
354
    let self = mk_self m in
355
    let mem = mk_mem m in
356
    fprintf fmt "%a@,%a@,%a%a"
357
      print_machine_ghost_struct m
358
      (print_machine_ghost_simulation_aux m pp_true ~i:0) ()
359
      (pp_print_list_i
360
        ~pp_epilogue:pp_print_cut
361
        ~pp_open_box:pp_open_vbox0
362
        (print_machine_ghost_simulation dependencies m))
363
      m.mstep.step_instrs
364
      (print_machine_ghost_simulation_aux m
365
         (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
366

    
367
let print_machine_core_annotations dependencies fmt m =
368
  if not (fst (Machine_code_common.get_stateless_status m)) then
369
    let name = m.mname.node_id in
370
    let self = mk_self m in
371
    let mem = mk_mem m in
372
    fprintf fmt "%a@,%a@,%a%a"
373
      print_machine_ghost_struct m
374
      (print_machine_ghost_simulation_aux m pp_true ~i:0) ()
375
      (pp_print_list_i
376
        ~pp_epilogue:pp_print_cut
377
        ~pp_open_box:pp_open_vbox0
378
        (print_machine_ghost_simulation dependencies m))
379
      m.mstep.step_instrs
380
      (print_machine_ghost_simulation_aux m
381
         (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
382

    
383
let pp_at pp_p fmt (p, l) =
384
  fprintf fmt "\\at(%a, %s)" pp_p p l
385

    
386
let label_pre = "Pre"
387

    
388
let pp_at_pre pp_p fmt p =
389
  pp_at pp_p fmt (p, label_pre)
390

    
391
module VarDecl = struct
392
  type t = var_decl
393
  let compare v1 v2 = compare v1.var_id v2.var_id
394
end
395
module VDSet = Set.Make(VarDecl)
396

    
397
let pp_arrow_spec fmt () =
398
  let name = "_arrow" in
399
  let mem_in = "mem_in" in
400
  let mem_out = "mem_out" in
401
  let reg_first = "_reg", "_first" in
402
  let mem_in_first = mem_in, reg_first in
403
  let mem_out_first = mem_out, reg_first in
404
  let mem = "mem" in
405
  let self = "self" in
406
  fprintf fmt "/* ACSL arrow spec */@,%a%a%a%a"
407
    (pp_spec_line (pp_ghost pp_print_string))
408
    "struct _arrow_mem_ghost {struct _arrow_reg _reg;};"
409
    (pp_spec_cut
410
       (pp_predicate
411
          (pp_mem_init pp_machine_decl)
412
          (pp_equal
413
             (pp_access pp_access')
414
             pp_print_string)))
415
    ((name, (name, "mem_ghost", mem_in)),
416
     (mem_in_first, "true"))
417
    (pp_spec_cut
418
       (pp_predicate
419
          (pp_mem_trans_aux
420
             pp_machine_decl pp_machine_decl pp_print_string pp_print_string)
421
          (pp_and
422
             (pp_equal
423
                pp_print_string
424
                (pp_access pp_access'))
425
             (pp_ite
426
                (pp_access pp_access')
427
                (pp_equal
428
                   (pp_access pp_access')
429
                   pp_print_string)
430
                (pp_equal
431
                   (pp_access pp_access')
432
                   (pp_access pp_access'))))))
433
    ((name, [], ["_Bool out"], (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
434
     (("out", mem_in_first),
435
      (mem_in_first, (mem_out_first, "false"), (mem_out_first, mem_in_first))))
436
    (pp_spec_cut
437
       (pp_predicate
438
          (pp_mem_ghost pp_machine_decl pp_machine_decl)
439
          (pp_equal
440
             (pp_access pp_access')
441
             (pp_indirect pp_access'))))
442
    ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
443
    ((mem, reg_first), (self, reg_first)))
444

    
445
module SrcMod = struct
446

    
447
  let pp_predicates dependencies fmt machines =
448
    fprintf fmt
449
      "%a@,%a%a%a"
450
      pp_arrow_spec ()
451
      (pp_print_list
452
         ~pp_open_box:pp_open_vbox0
453
         ~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")
454
         print_machine_valid_predicate
455
         ~pp_epilogue:pp_print_cutcut) machines
456
      (pp_print_list
457
         ~pp_open_box:pp_open_vbox0
458
         ~pp_sep:pp_print_cutcut
459
         ~pp_prologue:(pp_print_endcut "/* ACSL ghost simulations */")
460
         (print_machine_ghost_simulations dependencies)
461
         ~pp_epilogue:pp_print_cutcut) machines
462
      (pp_print_list
463
         ~pp_open_box:pp_open_vbox0
464
         ~pp_sep:pp_print_cutcut
465
         ~pp_prologue:(pp_print_endcut "/* ACSL core annotations */")
466
         (print_machine_core_annotations dependencies)
467
         ~pp_epilogue:pp_print_cutcut) machines
468

    
469
  let pp_reset_spec fmt self m =
470
    let name = m.mname.node_id in
471
    let mem = mk_mem m in
472
    pp_spec_cut (fun fmt () ->
473
        fprintf fmt
474
          "%a@,%a@,%a@,%a"
475
          (pp_requires pp_mem_valid') (name, self)
476
          (pp_requires (pp_separated self)) m.minstances
477
          (pp_assigns
478
             (pp_print_list
479
                ~pp_sep:pp_print_comma
480
                ~pp_nil:pp_nothing
481
                (pp_inst self))) m.minstances
482
          (pp_ensures
483
             (pp_forall
484
                pp_machine_decl
485
                (pp_implies
486
                   pp_mem_ghost'
487
                   pp_mem_init')))
488
          ((name, "mem_ghost", mem),
489
           ((name, mem, self), (name, mem))))
490
      fmt ()
491

    
492
  let pp_step_spec fmt self m =
493
    let name = m.mname.node_id in
494
    let mem_in = mk_mem_in m in
495
    let mem_out = mk_mem_out m in
496
    pp_spec_cut (fun fmt () ->
497
        fprintf fmt
498
          "%a@,%a@,%a@,%a@,%a"
499
          (pp_requires (pp_valid pp_var_decl)) m.mstep.step_outputs
500
          (pp_requires pp_mem_valid') (name, self)
501
          (pp_requires (pp_separated self)) m.minstances
502
          (pp_assigns
503
             (if m.mstep.step_outputs = [] && m.minstances = [] then
504
                pp_nothing
505
              else
506
                fun fmt () ->
507
                  fprintf fmt "@[<h>%a%a@]"
508
                    (pp_print_list
509
                       ~pp_sep:pp_print_comma
510
                       ~pp_epilogue:pp_print_comma
511
                       pp_ptr_decl) m.mstep.step_outputs
512
                    (pp_print_list
513
                       ~pp_sep:pp_print_comma
514
                       (pp_inst self)) m.minstances)) ()
515
          (pp_ensures
516
             (pp_forall
517
                (fun fmt () ->
518
                   fprintf fmt "%a, %s"
519
                     pp_machine_decl (name, "mem_ghost", mem_in)
520
                     mem_out)
521
                (pp_implies
522
                   (pp_at_pre pp_mem_ghost')
523
                   (pp_implies
524
                      pp_mem_ghost'
525
                      pp_mem_trans'))))
526
          ((),
527
           ((name, mem_in, self),
528
            ((name, mem_out, self),
529
             (m, mem_in, mem_out)))))
530
      fmt ()
531

    
532
  let pp_step_instr_spec m self fmt (i, _instr) =
533
    let name = m.mname.node_id in
534
    let mem_in = mk_mem_in m in
535
    let mem_out = mk_mem_out m in
536
    fprintf fmt "@,%a"
537
      (pp_spec
538
         (pp_assert
539
            (pp_forall
540
               (fun fmt () ->
541
                  fprintf fmt "%a, %s"
542
                    pp_machine_decl (name, "mem_ghost", mem_in)
543
                    mem_out)
544
               (pp_implies
545
                  (pp_at_pre pp_mem_ghost')
546
                  (pp_implies
547
                     (pp_mem_ghost' ~i:(i+1))
548
                     (pp_mem_trans' ~i:(i+1)))))))
549
      ((),
550
       ((name, mem_in, self),
551
        ((name, mem_out, self),
552
         (m, mem_in, mem_out))))
553

    
554
end
555

    
556
(**************************************************************************)
557
(*                              MAKEFILE                                  *)
558
(**************************************************************************)
559

    
560
module MakefileMod = struct
561

    
562
  let other_targets fmt basename _nodename dependencies =
563
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
564
    (* EACSL version of library file . c *)
565
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
566
    fprintf fmt
567
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@."
568
      basename basename;
569
    fprintf fmt "@.";
570
    fprintf fmt "@.";
571

    
572
    (* EACSL version of library file . c + main .c  *)
573
    fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;
574
    fprintf fmt "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c -then-on e-acsl -print -ocode %s_main_eacsl.i@."
575
      basename basename basename;
576
    (* Ugly hack to deal with eacsl bugs *)
577
    fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;
578
    fprintf fmt "@.";
579
    fprintf fmt "@.";
580

    
581
    (* EACSL version of binary *)
582
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
583
    fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)
584
    C_backend_makefile.fprintf_dependencies fmt dependencies;
585
    fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@."
586
      basename
587
      (Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name))
588
      (C_backend_makefile.compiled_dependencies dependencies)
589
      ("${FRAMACEACSL}/e_acsl.c "
590
       ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
591
       ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
592
      basename
593
      (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
594
      (C_backend_makefile.lib_dependencies dependencies)
595
    ;
596
    fprintf fmt "@."
597

    
598
end
599

    
600
(* Local Variables: *)
601
(* compile-command:"make -C ../../.." *)
602
(* End: *)
(9-9/10)