Revision 05f85b44
Added by Guillaume DAVY almost 6 years ago
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
Ada: Start cleaning Ada to prepare for why beckend