Project

General

Profile

« Previous | Next » 

Revision 75c459f4

Added by LĂ©lio Brun 9 months ago

start with Spec AST generation

View differences:

src/backends/Ada/ada_backend_adb.ml
127 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
          { instr_desc = MStateAssign (ident, value);
131
            lustre_eq= instr.lustre_eq }
130
        { instr with instr_desc = MStateAssign (ident, value) }
132 131
      | _ -> instr
133 132
    in
134 133
    let pp_local_ghost_list, spec_instrs = match m_spec_opt with
......
150 149
  **)
151 150
  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
152 151
    let build_assign = function var ->
153
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
152
      mkinstr Spec_types.True (MStateAssign (var, mk_default_value var.var_type))
154 153
    in
155 154
    let env, memory = match m_spec_opt with
156 155
      | None -> env, m.mmemory

Also available in: Unified diff