Project

General

Profile

« Previous | Next » 

Revision e164af45

Added by LĂ©lio Brun over 2 years ago

working version with additional asserts to make the axiom work

View differences:

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
  (********************************************************************************************)

Also available in: Unified diff