Project

General

Profile

Revision 173a2a8f src/backends/Ada/ada_backend_adb.ml

View differences:

src/backends/Ada/ada_backend_adb.ml
124 124
     @param fmt the formater to print on
125 125
     @param machine the machine
126 126
  **)
127
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt) =
127
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
128 128
    let transform_local_to_state_assign instr = match instr.instr_desc with
129 129
      | MLocalAssign (ident, value) -> 
130 130
          { instr_desc = MStateAssign (ident, value);
131 131
            lustre_eq= instr.lustre_eq }
132 132
      | x -> instr
133 133
    in
134
    let spec_instrs = match m_spec_opt with
135
      | None -> []
136
      | Some m_spec -> List.map transform_local_to_state_assign m_spec.mstep.step_instrs
134
    let pp_local_ghost_list, spec_instrs = match m_spec_opt with
135
      | None -> [], []
136
      | Some m_spec ->
137
          List.map (build_pp_var_decl_local (Some (true, [], []))) (List.filter (fun x -> not (List.mem x.var_id guarantees)) m_spec.mstep.step_locals),
138
          List.map transform_local_to_state_assign m_spec.mstep.step_instrs
137 139
    in
138 140
    let pp_local_list = List.map (build_pp_var_decl_local None) (m.mstep.step_locals) in
139 141
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (m.mstep.step_instrs@spec_instrs) in
140
    let content = AdaProcedureContent ((if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
142
    let content = AdaProcedureContent ((if pp_local_ghost_list = [] then [] else [pp_local_ghost_list])@(if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
141 143
    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
142 144

  
143 145
  (** Print the definition of the reset procedure from a machine.
......
146 148
     @param fmt the formater to print on
147 149
     @param machine the machine
148 150
  **)
149
  let pp_reset_definition env typed_submachines fmt m =
151
  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
150 152
    let build_assign = function var ->
151 153
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
152 154
    in
153
    let assigns = List.map build_assign m.mmemory in
155
    let env, memory = match m_spec_opt with
156
      | None -> env, m.mmemory
157
      | Some m_spec ->
158
          env,
159
          (m.mmemory)
160
    in
161
    let assigns = List.map build_assign memory in
154 162
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (assigns@m.minit) in
155 163
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
156 164

  
......
164 172
     @param typed_submachines list of all typed machine instances of this machine
165 173
     @param m the machine
166 174
  **)
167
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
175
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees, past_size), machine)) =
168 176
    let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
169 177
    let pp_reset fmt =
170 178
      if is_machine_statefull machine then
171
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) machine
179
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) (machine, opt_spec_machine)
172 180
      else
173 181
        fprintf fmt ""
174 182
    in
......
188 196
        pp_reset
189 197
        
190 198
        (*Define the step procedure*)
191
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine)
199
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine, guarantees)
192 200
    in
193 201
    fprintf fmt "%a%t%a;@."
194 202
      
195 203
      (* Include all the required packages*)
196
      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) packages
204
      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) packages
197 205
      (Utils.pp_final_char_if_non_empty ";@,@," packages)
198 206
      
199 207
      (*Print package*)

Also available in: Unified diff