Project

General

Profile

« Previous | Next » 

Revision 61e0c3c4

Added by Guillaume DAVY about 4 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