Project

General

Profile

« Previous | Next » 

Revision 05f85b44

Added by Guillaume DAVY almost 6 years ago

Ada: Start cleaning Ada to prepare for why beckend

View differences:

src/backends/Ada/ada_backend_adb.ml
134 134
    let pp_local_ghost_list, spec_instrs = match m_spec_opt with
135 135
      | None -> [], []
136 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),
137
          List.map (build_pp_var_decl_local (Some (true, false, [], []))) (List.filter (fun x -> not (List.mem x.var_id guarantees)) m_spec.mstep.step_locals),
138 138
          List.map transform_local_to_state_assign m_spec.mstep.step_instrs
139 139
    in
140 140
    let pp_local_list = List.map (build_pp_var_decl_local None) (m.mstep.step_locals) in
......
172 172
     @param typed_submachines list of all typed machine instances of this machine
173 173
     @param m the machine
174 174
  **)
175
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees, past_size), machine)) =
175
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
176 176
    let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
177 177
    let pp_reset fmt =
178 178
      if is_machine_statefull machine then

Also available in: Unified diff