Project

General

Profile

« Previous | Next » 

Revision e164af45

Added by LĂ©lio Brun almost 3 years ago

working version with additional asserts to make the axiom work

View differences:

src/backends/C/c_backend_spec.ml
107 107

  
108 108
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
109 109

  
110
let pp_at_pre pp_v fmt v = pp_at pp_v fmt (v, "Pre")
111

  
110 112
let find_machine f =
111 113
  List.find (fun m -> m.mname.node_id = f)
112 114

  
......
1460 1462
      | None ->
1461 1463
        [ mem, pp_print_string ])
1462 1464

  
1463
  let pp_contract fmt machines _self m =
1464
    match m.mspec.mnode_spec with
1465
    | Some (NodeSpec f) ->
1466
      let m_f = find_machine f machines in
1467
      pp_acsl_line'_cut
1468
        (pp_ghost
1469
           (fun fmt () ->
1470
              fprintf
1471
                fmt
1472
                "%a(%a%a);"
1473
                pp_machine_step_name
1474
                m_f.mname.node_id
1475
                (pp_comma_list ~pp_eol:pp_print_comma (pp_c_var_read m))
1476
                m_f.mstep.step_inputs
1477
                (pp_comma_list (pp_c_var_write m))
1478
                m_f.mstep.step_outputs))
1479
        fmt ()
1480
    | _ -> ()
1465
  let pp_contract fmt machines _self mem m =
1466
    let pp_vars ?pp_eol = pp_comma_list ?pp_eol (pp_c_var_read m) in
1467
    match contract_of machines m with
1468
    | Some c, Some m_c ->
1469
      fprintf fmt "%a%a"
1470
        (pp_acsl_line'_cut
1471
           (pp_ghost
1472
              (fun fmt () ->
1473
                 fprintf
1474
                   fmt
1475
                   "%a(%a%a);"
1476
                   pp_machine_step_name
1477
                   m_c.mname.node_id
1478
                   (pp_vars ~pp_eol:pp_print_comma)
1479
                   m_c.mstep.step_inputs
1480
                   (pp_comma_list (pp_c_var_write m))
1481
                   m_c.mstep.step_outputs)))
1482
        ()
1483
        (pp_acsl_cut
1484
           (pp_print_option
1485
              (fun fmt -> function
1486
                 | Kinduction k ->
1487
                   let l = List.init k (fun n -> n + 1) in
1488
                   let pp_mem_in = pp_at_pre pp_ptr in
1489
                   let pp_mem_out = pp_ptr in
1490
                   pp_assert
1491
                     (pp_and
1492
                        (pp_and_l
1493
                           (fun fmt n ->
1494
                              (if n = k then
1495
                                 pp_k_induction_inductive_case
1496
                               else
1497
                                 pp_k_induction_base_case)
1498
                                m
1499
                                pp_mem_in
1500
                                pp_mem_out
1501
                                pp_vars
1502
                                fmt
1503
                                (n, mem, mem)))
1504
                        (pp_transition_aux m_c pp_print_string pp_print_string (pp_c_var_read m)))
1505
                     fmt
1506
                     (l, (m_c.mname.node_id,
1507
                          m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
1508
                          "", ""))))) c.mc_proof
1509
        | _, _ -> ()
1481 1510

  
1482 1511
end
1483 1512

  
src/backends/C/c_backend_src.ml
35 35

  
36 36
  val pp_ghost_parameter : ident -> formatter -> ident option -> unit
37 37

  
38
  val pp_contract : formatter -> machine_t list -> ident -> machine_t -> unit
38
  val pp_contract : formatter -> machine_t list -> ident -> ident -> machine_t -> unit
39 39
end
40 40

  
41 41
module EmptyMod = struct
......
53 53

  
54 54
  let pp_ghost_parameter _ _ _ = ()
55 55

  
56
  let pp_contract _ _ _ _ = ()
56
  let pp_contract _ _ _ _ _ = ()
57 57
end
58 58

  
59 59
module Main (Mod : MODIFIERS_SRC) = struct
......
618 618
        ~checks:m.mstep.step_checks
619 619
        ~pp_instr:(pp_machine_instr dependencies m self self)
620 620
        ~instrs:m.mstep.step_instrs
621
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self m)
621
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self self m)
622 622
        fmt
623 623
    else
624 624
      (* C90 code *)
......
650 650
        ~checks:m.mstep.step_checks
651 651
        ~pp_instr:(pp_machine_instr dependencies m self self)
652 652
        ~instrs:m.mstep.step_instrs
653
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self m)
653
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self self m)
654 654
        fmt
655 655

  
656 656
  let pp_clear_reset_code dependencies self mem fmt m =
......
742 742
        ~checks:m.mstep.step_checks
743 743
        ~pp_instr:(pp_machine_instr dependencies m self mem)
744 744
        ~instrs:m.mstep.step_instrs
745
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self m)
745
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self mem m)
746 746
        fmt
747 747
    else
748 748
      (* C90 code *)
......
774 774
        ~checks:m.mstep.step_checks
775 775
        ~pp_instr:(pp_machine_instr dependencies m self mem)
776 776
        ~instrs:m.mstep.step_instrs
777
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self m)
777
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self mem m)
778 778
        fmt
779 779

  
780 780
  (********************************************************************************************)
src/backends/C/c_backend_src.mli
21 21

  
22 22
  val pp_ghost_parameter : ident -> formatter -> ident option -> unit
23 23

  
24
  val pp_contract : formatter -> machine_t list -> ident -> machine_t -> unit
24
  val pp_contract : formatter -> machine_t list -> ident -> ident -> machine_t -> unit
25 25
end
26 26

  
27 27
module EmptyMod : MODIFIERS_SRC

Also available in: Unified diff