Project

General

Profile

« Previous | Next » 

Revision aaa8e454

Added by Lélio Brun 7 months ago

it works

View differences:

src/backends/C/c_backend_spec.ml
16 16
open C_backend_common
17 17
open Corelang
18 18
open Spec_types
19
open Spec_common
20 19
open Machine_code_common
21 20

  
22 21
(**************************************************************************)
......
34 33
    "_Bool"
35 34
  else if Types.is_int_type t_desc then
36 35
    (* !Options.int_type *)
37
    "integer"
36
    if t_desc.tid = -1 then "int" else "integer"
38 37
  else if Types.is_real_type t_desc then
39 38
    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
40 39
  else
......
91 90

  
92 91
let pp_access' = pp_access pp_print_string pp_print_string
93 92

  
94
let pp_inst self fmt (name, _) =
95
  pp_indirect' fmt (self, name)
96

  
97 93
let pp_var_decl fmt v =
98 94
  pp_print_string fmt v.var_id
99 95

  
......
251 247

  
252 248
let pp_initialization' = pp_initialization pp_print_string
253 249

  
250
let pp_local m =
251
  pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
252

  
254 253
let pp_locals m =
255 254
  pp_comma_list
256
    ~pp_open_box:pp_open_hbox
257
    (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
255
    ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0)
256
    (pp_local m)
258 257

  
259 258
let pp_ptr_decl fmt v =
260 259
  pp_ptr fmt v.var_id
......
272 271
  let depth = expansion_depth value in
273 272
  let loop_vars = mk_loop_variables m var_type depth in
274 273
  let reordered_loop_vars = reorder_loop_variables loop_vars in
275
  let rec aux typ fmt vars =
274
  let aux typ fmt vars =
276 275
    match vars with
277 276
    | [] ->
278 277
      pp_basic_assign_spec
......
298 297
    aux var_type fmt reordered_loop_vars;
299 298
  end
300 299

  
301
let pp_c_var_read m fmt id =
302
  (* mpfr_t is a static array, not treated as general arrays *)
303
  if Types.is_address_type id.var_type
304
  then
305
    if is_memory m id
306
    && not (Types.is_real_type id.var_type && !Options.mpfr)
307
    then fprintf fmt "(*%s)" id.var_id
308
    else fprintf fmt "%s" id.var_id
309
  else
310
    fprintf fmt "%s" id.var_id
311

  
312 300
let pp_nothing fmt () =
313 301
  pp_print_string fmt "\\nothing"
314 302

  
......
334 322
  fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])"
335 323
    name
336 324
    (pp_print_option pp_print_int) i
337
    (fun fmt -> if not stateless then fprintf fmt "%a,@ " pp_mem_in mem_in)
338
    (pp_comma_list pp_input) inputs
325
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
326
    (pp_comma_list
327
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
328
       pp_input) inputs
339 329
    (pp_print_option (fun fmt _ ->
340 330
         pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
341 331
    i
......
364 354

  
365 355
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
366 356

  
357
let pp_functional_update mems fmt mem =
358
  let rec aux fmt mems =
359
    match mems with
360
    | [] -> pp_print_string fmt mem
361
    | x :: mems ->
362
      fprintf fmt "{ @[<hov>%a@ \\with ._reg.%s = %s@] }" aux mems x x
363
  in
364
  aux fmt
365
  (* if Utils.ISet.is_empty mems then
366
   *   pp_print_string fmt mem
367
   *     else
368
   *   fprintf fmt "{ %s @[<hov>\\with %a@] }"
369
   *     mem
370
   *     (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
371
   *        (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
372
      (Utils.ISet.elements mems)
373

  
367 374
module PrintSpec = struct
368 375

  
369
  let pp_reg pp_mem fmt = function
376
  type mode =
377
    | MemoryPackMode
378
    | TransitionMode
379
    | TransitionFootprintMode
380
    | ResetIn
381
    | ResetOut
382
    | InstrMode of ident
383

  
384
  let pp_reg mem fmt = function
370 385
    | ResetFlag ->
371
      fprintf fmt "%t%s" pp_mem reset_flag_name
386
      fprintf fmt "%s.%s" mem reset_flag_name
372 387
    | StateVar x ->
373
      fprintf fmt "%t%a" pp_mem pp_var_decl x
388
      fprintf fmt "%s.%a" mem pp_var_decl x
374 389

  
375 390
  let pp_expr:
376
    type a. machine_t -> (formatter -> unit) -> formatter -> (value_t, a) expression_t -> unit =
377
    fun m pp_mem fmt -> function
378
    | Val v -> pp_val m fmt v
391
    type a. ?output:bool -> machine_t -> ident -> formatter
392
    -> (value_t, a) expression_t -> unit =
393
    fun ?(output=false) m mem fmt -> function
394
    | Val v -> pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v
379 395
    | Tag t -> pp_print_string fmt t
380 396
    | Var v -> pp_var_decl fmt v
381
    | Memory r -> pp_reg pp_mem fmt r
397
    | Memory r -> pp_reg mem fmt r
382 398

  
383
  let pp_predicate m mem_in mem_in' mem_out mem_out' fmt p =
384
    let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
385
      fun fmt e -> pp_expr m (fun fmt -> fprintf fmt "%s." mem_out) fmt e
399
  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
400
    let output, mem_update = match mode with
401
      | InstrMode _ -> true, false
402
      | TransitionFootprintMode -> false, true
403
      | _ -> false, false
404
    in
405
    let pp_expr:
406
      type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
407
      fun ?output fmt e -> pp_expr ?output m mem_out fmt e
386 408
    in
387 409
    match p with
388
    | Transition (f, inst, i, inputs, locals, outputs) ->
410
    | Transition (f, inst, i, inputs, locals, outputs, r, mems) ->
389 411
      let pp_mem_in, pp_mem_out = match inst with
390 412
        | None ->
391
          pp_print_string, pp_print_string
413
          pp_print_string,
414
          if mem_update then pp_functional_update mems else pp_print_string
392 415
        | Some inst ->
393
          (fun fmt mem_in -> pp_access' fmt (mem_in, inst)),
416
          (fun fmt mem_in ->
417
             if r then pp_print_string fmt mem_in
418
             else pp_access' fmt (mem_in, inst)),
394 419
          (fun fmt mem_out -> pp_access' fmt (mem_out, inst))
395 420
      in
396
      pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr pp_expr fmt
421
      pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output)
422
        fmt
397 423
        (f, inputs, locals, outputs, mem_in', mem_out')
424
    | Reset (_f, inst, r) ->
425
      pp_ite
426
        (pp_c_val m mem_in (pp_c_var_read m))
427
        (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
428
        (pp_equal pp_print_string pp_access')
429
        fmt
430
        (r, (mem_out, 1), (mem_out, (mem_in, inst)))
398 431
    | MemoryPack (f, inst, i) ->
399 432
      let pp_mem, pp_self = match inst with
400 433
        | None ->
......
418 451
    | Memory (StateVar v) -> vdecl_to_val v
419 452
    | Memory ResetFlag -> vdecl_to_val reset_flag
420 453

  
421
  type mode =
422
    | MemoryPackMode
423
    | TransitionMode
424
    | ResetIn
425
    | ResetOut
426
    | InstrMode of ident
427

  
428 454
  let find_arrow m =
429 455
    try
430 456
      List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
431 457
      |> fst
432 458
    with Not_found -> eprintf "Internal error: arrow not found"; raise Not_found
433 459

  
434
  let pp_spec mode m =
460
  let pp_spec mode m fmt f =
435 461
    let rec pp_spec mode fmt f =
436 462
      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
437 463
        let self = mk_self m in
......
444 470
          self, self, true, mem, mem, false
445 471
        | TransitionMode ->
446 472
          mem_in, mem_in, false, mem_out, mem_out, false
473
        | TransitionFootprintMode ->
474
          mem_in, mem_in, false, mem_out, mem_out, false
447 475
        | ResetIn ->
448
          mem_in, mem_in, false, mem_reset, mem_reset, false
449
        | ResetOut ->
450 476
          mem_reset, mem_reset, false, mem_out, mem_out, false
477
        | ResetOut ->
478
          mem_in, mem_in, false, mem_reset, mem_reset, false
451 479
        | InstrMode self ->
452 480
          let mem = "*" ^ mem in
453 481
          fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
......
455 483
          mem, mem, false
456 484
      in
457 485
      let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
458
        fun fmt e -> pp_expr m (fun fmt -> fprintf fmt "%s." mem_out) fmt e
486
        fun fmt e -> pp_expr m mem_out fmt e
459 487
      in
460 488
      let pp_spec' = pp_spec mode in
461 489
      match f with
......
465 493
        pp_false fmt ()
466 494
      | Equal (a, b) ->
467 495
        pp_assign_spec m
468
          mem_out (pp_c_var_read m) indirect_l
469
          mem_in (pp_c_var_read m) indirect_r
496
          mem_out (pp_c_var_read ~test_output:false m) indirect_l
497
          mem_in (pp_c_var_read ~test_output:false m) indirect_r
470 498
          fmt
471 499
          (type_of_l_value a, val_of_expr a, val_of_expr b)
472 500
      | And fs ->
......
482 510
      | Ternary (e, a, b) ->
483 511
        pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
484 512
      | Predicate p ->
485
        pp_predicate m mem_in mem_in' mem_out mem_out' fmt p
513
        pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
486 514
      | StateVarPack ResetFlag ->
487 515
        let r = vdecl_to_val reset_flag in
488 516
        pp_assign_spec m
489
          mem_out (pp_c_var_read m) indirect_l
490
          mem_in (pp_c_var_read m) indirect_r
517
          mem_out (pp_c_var_read ~test_output:false m) indirect_l
518
          mem_in (pp_c_var_read ~test_output:false m) indirect_r
491 519
          fmt
492 520
          (Type_predef.type_bool, r, r)
493 521
      | StateVarPack (StateVar v) ->
......
496 524
        pp_par (pp_implies
497 525
                  (pp_not (pp_initialization pp_access'))
498 526
                  (pp_assign_spec m
499
                     mem_out (pp_c_var_read m) indirect_l
500
                     mem_in (pp_c_var_read m) indirect_r))
527
                     mem_out (pp_c_var_read ~test_output:false m) indirect_l
528
                     mem_in (pp_c_var_read ~test_output:false m) indirect_r))
501 529
          fmt
502 530
          ((Arrow.arrow_id, (mem_out, inst)),
503 531
           (v.var_type, v', v'))
504
      | ExistsMem (rc, tr) ->
532
      | ExistsMem (f, rc, tr) ->
505 533
        pp_exists
506 534
          (pp_machine_decl' ~ghost:true)
507
          (pp_and (pp_spec ResetIn) (pp_spec ResetOut))
535
          (pp_and (pp_spec ResetOut) (pp_spec ResetIn))
508 536
          fmt
509
          ((m.mname.node_id, mk_mem_reset m),
537
          ((f, mk_mem_reset m),
510 538
           (rc, tr))
511
          (* fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec f *)
512 539
    in
513
    pp_spec mode
540
    match mode with
541
    | TransitionFootprintMode ->
542
      let mem_in = mk_mem_in m in
543
      let mem_out = mk_mem_out m in
544
      pp_forall
545
        (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
546
        (pp_spec mode)
547
        fmt ((m.mname.node_id, [mem_in; mem_out]), f)
548
    | _ ->
549
      pp_spec mode fmt f
514 550

  
515 551
end
516 552

  
......
519 555
    pp_l l
520 556
    pp_r r
521 557

  
522
let print_machine_valid_predicate fmt m =
558
let pp_lemma pp_l pp_r fmt (l, r) =
559
  fprintf fmt "@[<v 2>lemma %a:@,%a;@]"
560
    pp_l l
561
    pp_r r
562

  
563
let pp_mem_valid_def fmt m =
523 564
  if not (fst (get_stateless_status m)) then
524 565
    let name = m.mname.node_id in
525 566
    let self = mk_self m in
......
527 568
      (pp_predicate
528 569
         (pp_mem_valid (pp_machine_decl pp_ptr))
529 570
         (pp_and
530
            (pp_and_l (fun fmt (_, (td, _) as inst) ->
531
                 pp_mem_valid (pp_inst self) fmt (node_name td, inst)))
571
            (pp_and_l (fun fmt (inst, (td, _)) ->
572
                 if Arrow.td_is_arrow td then
573
                   pp_valid pp_indirect' fmt [self, inst]
574
                 else
575
                   pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
532 576
            (pp_valid pp_print_string)))
533 577
      fmt
534 578
      ((name, (name, self)),
535 579
       (m.minstances, [self]))
536 580

  
537

  
538 581
let pp_memory_pack_def m fmt mp =
539 582
  let name = mp.mpname.node_id in
540 583
  let self = mk_self m in
......
567 610
    (pp_predicate
568 611
       (pp_transition m
569 612
          (pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true)
570
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
571
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m))
613
          (pp_local m)
614
          (pp_local m))
572 615
       (PrintSpec.pp_spec TransitionMode m))
573 616
    fmt
574 617
    ((t, (name, mem_in), (name, mem_out)),
575 618
     t.tformula)
576 619

  
577
(* let print_trans_simulation dependencies m fmt (i, instr) =
578
 *   let mem_in = mk_mem_in m in
579
 *   let mem_out = mk_mem_out m in
580
 *   let d = VDSet.(diff (union (live_i m i) (assigned empty instr))
581
 *                    (live_i m (i+1))) in
582
 *   (\* XXX *\)
583
 *   (\* printf "%d : %a\n%d : %a\nocc: %a\n\n"
584
 *    *   i
585
 *    *   (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i))
586
 *    *   (i+1)
587
 *    *   (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)))
588
 *    *   (pp_print_parenthesized pp_var_decl) VDSet.(elements (assigned empty instr)); *\)
589
 *   let prev_trans fmt () = pp_mem_trans' ~i fmt (m, mem_in, mem_out) in
590
 *   let pred pp v =
591
 *     let vars = VDSet.(union (of_list m.mstep.step_locals)
592
 *                         (of_list m.mstep.step_outputs)) in
593
 *     let locals = VDSet.(inter vars d |> elements) in
594
 *     if locals = []
595
 *     then pp_and prev_trans pp fmt ((), v)
596
 *     else pp_exists (pp_locals m) (pp_and prev_trans pp) fmt (locals, ((), v))
597
 *   in
598
 *   let rec aux fmt instr = match instr.instr_desc with
599
 *     | MLocalAssign (x, v)
600
 *     | MStateAssign (x, v) ->
601
 *       pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m) fmt
602
 *         (x.var_type, mk_val (Var x) x.var_type, v)
603
 *     | MStep ([i0], i, vl)
604
 *       when Basic_library.is_value_internal_fun
605
 *           (mk_val (Fun (i, vl)) i0.var_type)  ->
606
 *       pp_true fmt ()
607
 *     | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
608
 *       pp_true fmt ()
609
 *     | MStep ([_], i, _) when has_c_prototype i dependencies ->
610
 *       pp_true fmt ()
611
 *     | MStep (xs, i, ys) ->
612
 *       begin try
613
 *           let n, _ = List.assoc i m.minstances in
614
 *           pp_mem_trans_aux
615
 *             (fst (get_stateless_status_top_decl n))
616
 *             pp_access' pp_access'
617
 *             (pp_c_val m mem_in (pp_c_var_read m))
618
 *             pp_var_decl
619
 *             fmt
620
 *             (node_name n, ys, [], xs, (mem_in, i), (mem_out, i))
621
 *         with Not_found -> pp_true fmt ()
622
 *       end
623
 *     | MReset i ->
624
 *       begin try
625
 *           let n, _ = List.assoc i m.minstances in
626
 *           pp_mem_init' fmt (node_name n, mem_out)
627
 *         with Not_found -> pp_true fmt ()
628
 *       end
629
 *     | MBranch (v, brs) ->
630
 *       if let t = fst (List.hd brs) in t = tag_true || t = tag_false
631
 *       then (\* boolean case *\)
632
 *         pp_ite (pp_c_val m mem_in (pp_c_var_read m))
633
 *           (fun fmt () ->
634
 *              match List.assoc tag_true brs with
635
 *              | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
636
 *              | []
637
 *              | exception Not_found -> pp_true fmt ())
638
 *           (fun fmt () ->
639
 *              match List.assoc tag_false brs with
640
 *              | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
641
 *              | []
642
 *              | exception Not_found -> pp_true fmt ())
643
 *           fmt (v, (), ())
644
 *       else (\* enum type case *\)
645
 *       pp_and_l (fun fmt (l, instrs) ->
646
 *             let pp_val = pp_c_val m mem_in (pp_c_var_read m) in
647
 *             pp_paren (pp_implies
648
 *                         (pp_equal pp_val pp_c_tag)
649
 *                         (pp_and_l aux))
650
 *               fmt
651
 *               ((v, l), instrs))
652
 *         fmt brs
653
 *     | _ -> pp_true fmt ()
654
 *   in
655
 *   pred aux instr *)
656

  
657
(* let print_machine_trans_simulation dependencies m fmt i instr =
658
 *   print_machine_trans_simulation_aux m
659
 *     (print_trans_simulation dependencies m)
660
 *     ~i:(i+1)
661
 *     fmt (i, instr) *)
662

  
663 620
let pp_transition_defs fmt m =
664
  (* set_live_of m; *)
665
  (* let i = List.length m.mstep.step_instrs in *)
666
  (* let mem_in = mk_mem_in m in
667
   * let mem_out = mk_mem_out m in *)
668
  (* let last_trans fmt () =
669
   *   let locals = VDSet.(inter
670
   *                         (of_list m.mstep.step_locals)
671
   *                         (live_i m i)
672
   *                       |> elements) in
673
   *   if locals = []
674
   *   then pp_mem_trans' ~i fmt (m, mem_in, mem_out)
675
   *   else pp_exists (pp_locals m) (pp_mem_trans' ~i) fmt
676
   *       (locals, (m, mem_in, mem_out))
677
   * in *)
678
  fprintf fmt "%a"
679
    (pp_print_list
680
       ~pp_epilogue:pp_print_cut
681
       ~pp_open_box:pp_open_vbox0
682
       (pp_transition_def m)) m.mspec.mtransitions
683

  
684
let print_machine_init_predicate fmt m =
621
  pp_print_list
622
    ~pp_epilogue:pp_print_cut
623
    ~pp_open_box:pp_open_vbox0
624
    (pp_transition_def m) fmt m.mspec.mtransitions
625

  
626
let pp_transition_footprint fmt t =
627
  fprintf fmt "%s_transition%a_footprint"
628
    t.tname.node_id
629
    (pp_print_option pp_print_int) t.tindex
630

  
631
let pp_transition_footprint_lemma m fmt t =
632
  let open Utils.ISet in
633
  let name = t.tname.node_id in
634
  let mems = diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint in
635
  let memories = List.map (fun v ->
636
      { v with var_type = { v.var_type with tid = -1 }})
637
      (List.filter (fun v -> not (mem v.var_id t.tfootprint)) m.mmemory)
638
  in
639
  if not (is_empty mems) then
640
    pp_acsl
641
      (pp_lemma
642
         pp_transition_footprint
643
         (PrintSpec.pp_spec TransitionFootprintMode m))
644
      fmt
645
      (t,
646
       Forall (
647
         memories @ t.tinputs @ t.tlocals @ t.toutputs,
648
         Imply (Spec_common.mk_transition ?i:t.tindex name
649
                  (vdecls_to_vals t.tinputs)
650
                  (vdecls_to_vals t.tlocals)
651
                  (vdecls_to_vals t.toutputs),
652
                Spec_common.mk_transition ~mems ?i:t.tindex name
653
                  (vdecls_to_vals t.tinputs)
654
                  (vdecls_to_vals t.tlocals)
655
                  (vdecls_to_vals t.toutputs))))
656

  
657
let pp_transition_footprint_lemmas fmt m =
658
  pp_print_list
659
    ~pp_epilogue:pp_print_cut
660
    ~pp_open_box:pp_open_vbox0
661
    (pp_transition_footprint_lemma m) fmt
662
    (List.filter (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
663
         m.mspec.mtransitions)
664

  
665
let pp_initialization_def fmt m =
685 666
  if not (fst (get_stateless_status m)) then
686 667
    let name = m.mname.node_id in
687 668
    let mem_in = mk_mem_in m in
......
689 670
      (pp_predicate
690 671
         (pp_initialization (pp_machine_decl' ~ghost:true))
691 672
         (pp_and_l (fun fmt (i, (td, _)) ->
692
              pp_initialization pp_access' fmt (node_name td, (mem_in, i)))))
673
              if Arrow.td_is_arrow td then
674
                pp_initialization pp_access' fmt (node_name td, (mem_in, i))
675
              else
676
                pp_equal (pp_reset_flag ~indirect:false pp_access') pp_print_int
677
                  fmt
678
                  ((mem_in, i), 1))))
693 679
      fmt
694 680
      ((name, (name, mem_in)), m.minstances)
695 681

  
682
let pp_reset_cleared_def fmt m =
683
  if not (fst (get_stateless_status m)) then
684
    let name = m.mname.node_id in
685
    let mem_in = mk_mem_in m in
686
    let mem_out = mk_mem_out m in
687
    pp_acsl
688
      (pp_predicate
689
         (pp_reset_cleared
690
            (pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true))
691
         (pp_ite
692
            (pp_reset_flag' ~indirect:false)
693
            (pp_and
694
               (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
695
               pp_initialization')
696
            (pp_equal pp_print_string pp_print_string)))
697
      fmt
698
      ((name, (name, mem_in), (name, mem_out)),
699
       (mem_in,
700
        ((mem_out, 0), (name, mem_out)),
701
        (mem_out, mem_in)))
702

  
696 703
let pp_at pp_p fmt (p, l) =
697 704
  fprintf fmt "\\at(%a, %s)" pp_p p l
698 705

  
......
712 719
let pp_reset_flag_chain ?(indirect=true) ptr fmt mems =
713 720
  pp_print_list
714 721
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
715
    ~pp_epilogue:(fun fmt () -> pp_reset_flag ~indirect fmt "")
722
    ~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
716 723
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
717 724
    (fun fmt (i, _) -> pp_print_string fmt i)
718 725
    fmt mems
......
736 743

  
737 744
  let print_machine_decl_prefix = fun _ _ -> ()
738 745

  
739
  let pp_import_standard_spec fmt () =
740
    fprintf fmt "@,#include \"%s/arrow_spec.h%s\""
746
  let pp_import_arrow fmt () =
747
    fprintf fmt "#include \"%s/arrow_spec.h%s\""
741 748
      (Arrow.arrow_top_decl ()).top_decl_owner
742 749
      (if !Options.cpp then "pp" else "")
743 750

  
......
748 755
  module GhostProto = GhostProto
749 756

  
750 757
  let pp_predicates (* dependencies *) fmt machines =
758
    let pp_preds comment pp =
759
      pp_print_list
760
        ~pp_open_box:pp_open_vbox0
761
        ~pp_prologue:(pp_print_endcut comment)
762
        pp
763
        ~pp_epilogue:pp_print_cutcut in
751 764
    fprintf fmt
752
      "%a%a%a%a"
753
      (pp_print_list
754
         ~pp_open_box:pp_open_vbox0
755
         ~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")
756
         print_machine_valid_predicate
757
         ~pp_epilogue:pp_print_cutcut) machines
758
      (pp_print_list
759
         ~pp_open_box:pp_open_vbox0
760
         ~pp_sep:pp_print_cutcut
761
         ~pp_prologue:(pp_print_endcut "/* ACSL ghost simulations */")
762
         pp_memory_pack_defs
763
         ~pp_epilogue:pp_print_cutcut) machines
764
      (pp_print_list
765
         ~pp_open_box:pp_open_vbox0
766
         ~pp_sep:pp_print_cutcut
767
         ~pp_prologue:(pp_print_endcut "/* ACSL initialization annotations */")
768
         print_machine_init_predicate
769
         ~pp_epilogue:pp_print_cutcut) machines
770
      (pp_print_list
771
         ~pp_open_box:pp_open_vbox0
772
         ~pp_sep:pp_print_cutcut
773
         ~pp_prologue:(pp_print_endcut "/* ACSL transition annotations */")
774
         pp_transition_defs
775
         ~pp_epilogue:pp_print_cutcut) machines
765
      "%a%a%a%a%a%a"
766
      (pp_preds "/* ACSL `valid` predicates */"
767
         pp_mem_valid_def) machines
768
      (pp_preds "/* ACSL `memory pack` simulations */"
769
         pp_memory_pack_defs) machines
770
      (pp_preds "/* ACSL initialization annotations */"
771
         pp_initialization_def) machines
772
      (pp_preds "/* ACSL reset cleared annotations */"
773
         pp_reset_cleared_def) machines
774
      (pp_preds "/* ACSL transition annotations */"
775
         pp_transition_defs) machines
776
      (pp_preds "/* ACSL transition memory footprints lemmas */"
777
         pp_transition_footprint_lemmas) machines
776 778

  
777 779
  let pp_clear_reset_spec fmt self mem m =
778 780
    let name = m.mname.node_id in
......
796 798
                         ~i:(List.length m.mspec.mmemory_packs - 2)
797 799
                         pp_ptr pp_print_string))
798 800
          (name, mem, self)
799
          (pp_assigns pp_reset_flag) [self]
801
          (pp_assigns pp_reset_flag') [self]
800 802
          (pp_assigns (pp_register_chain self)) (mk_insts arws)
801 803
          (pp_assigns (pp_reset_flag_chain self)) (mk_insts narws)
802
          (pp_assigns pp_reset_flag) [mem]
804
          (pp_assigns pp_reset_flag') [mem]
803 805
          (pp_assigns (pp_register_chain ~indirect:false mem)) (mk_insts arws)
804 806
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) (mk_insts narws)
805
          (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 1)
807
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 1)
806 808
          (pp_ensures (pp_initialization pp_ptr)) (name, mem)
807
          (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 0)
809
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 0)
808 810
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem)
809 811
      )
810 812
      fmt ()
......
815 817
        fprintf fmt
816 818
          "%a@,%a@,%a"
817 819
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) (name, mem, self)
818
          (pp_ensures (pp_equal pp_reset_flag pp_print_string)) (mem, "1")
819
          (pp_assigns pp_reset_flag) [self; mem])
820
          (pp_ensures (pp_equal pp_reset_flag' pp_print_int)) (mem, 1)
821
          (pp_assigns pp_reset_flag') [self; mem])
820 822
      fmt ()
821 823

  
822 824
  let pp_step_spec fmt machines self mem m =
......
839 841
            (name, inputs, [], outputs, "", "")
840 842
        else
841 843
          fprintf fmt
842
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
844
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
843 845
            (pp_requires (pp_valid pp_var_decl)) outputs
844 846
            (pp_requires pp_mem_valid') (name, self)
845 847
            (pp_requires (pp_separated self mem)) (insts', outputs)
846 848
            (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
847 849
            (name, mem, self)
850
            (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
851
            (name, mem, self)
852
            (pp_ensures (pp_transition_aux m (pp_old pp_ptr)
853
                           pp_ptr pp_var_decl pp_ptr_decl))
854
            (name, inputs, [], outputs, mem, mem)
848 855
            (pp_assigns pp_ptr_decl) outputs
849 856
            (pp_assigns (pp_reg self)) m.mmemory
857
            (pp_assigns pp_reset_flag') [self]
850 858
            (pp_assigns (pp_memory self)) (memories insts')
851 859
            (pp_assigns (pp_register_chain self)) insts
852 860
            (pp_assigns (pp_reset_flag_chain self)) insts''
853 861
            (pp_assigns (pp_reg mem)) m.mmemory
862
            (pp_assigns pp_reset_flag') [mem]
854 863
            (pp_assigns (pp_memory ~indirect:false mem)) (memories insts')
855 864
            (pp_assigns (pp_register_chain ~indirect:false mem)) insts
856 865
            (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) insts''
857
            (pp_ensures (pp_transition_aux m (pp_old pp_ptr)
858
                           pp_ptr pp_var_decl pp_ptr_decl))
859
            (name, inputs, [], outputs, mem, mem)
860 866
      )
861 867
      fmt ()
862 868

  
......
876 882
    | MSetReset inst ->
877 883
      let td, _ = List.assoc inst m.minstances in
878 884
      if Arrow.td_is_arrow td then
879
         fprintf fmt "@,%a"
885
         fprintf fmt "@,%a;"
880 886
           (pp_acsl_line
881 887
              (pp_ghost
882 888
                 (pp_arrow_reset_ghost self)))

Also available in: Unified diff