Project

General

Profile

« Previous | Next » 

Revision 61e0c3c4

Added by Guillaume DAVY about 6 years ago

Ada:
- Correct the merge with lustrec-seal
- Improve support for builtin function(still work to do)
- Add generation of a gpr file for lib(without main).
- Add var initialisation in the reset, still work to do.

View differences:

src/backends/Ada/ada_backend_ads.ml
106 106 
  let pp_procedure_prototype_contract pp_prototype fmt opt_contract =
107 107 
    match opt_contract with
108 108 
      | None -> pp_prototype fmt
109 
      | Some contract ->
110 
          fprintf fmt "@[<v 2>%t with@,%a%t%a@]"
109 
      | Some (NodeSpec ident) -> pp_prototype fmt (*TODO*)
110 
      | Some (Contract contract) ->
111 
          fprintf fmt "@[<v 2>%t with@,Global => null;@,%a%t%a@]"
111 112 
            pp_prototype
112 113 
            (Utils.fprintf_list ~sep:",@," pp_pre) contract.assume
113 114 
            (Utils.pp_final_char_if_non_empty ",@," contract.assume)
......
118 119 
     @param machine the machine
119 120 
  **)
120 121 
  let pp_step_prototype_contract fmt m =
121 
    ()
122 
      (* Temporarily disabled while waiting for the code to stabilize
123 
pp_procedure_prototype_contract
124 
        (pp_step_prototype m)
125 
        fmt
126 
        m.mspec
127 
       *)
122 
    pp_procedure_prototype_contract
123 
      (pp_step_prototype m)
124 
      fmt
125 
      m.mspec
126
128 127
129 128 
  (** Remove duplicates from a list according to a given predicate.
130 129 
     @param eq the predicate defining equality

Also available in: Unified diff