Project

General

Profile

« Previous | Next » 

Revision c4780a6a

Added by LĂ©lio Brun 7 months ago

work on new reset functions generation

View differences:

src/backends/Horn/horn_backend_printers.ml
163 163
       pp_var fmt (rename_machine self v)
164 164
    
165 165
  | Fun (n, vl)   -> fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val m self pp_var)) vl
166
  | ResetFlag ->
167
    (* TODO: handle reset flag *)
168
    assert false
166 169

  
167 170
(* Prints a [value] indexed by the suffix list [loop_vars] *)
168 171
let rec pp_value_suffix m self pp_value fmt value =
......
295 298
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
296 299
  match get_instr_desc instr with
297 300
  | MSpec _ | MComment _ -> reset_instances
301
  (* TODO: handle reset flag *)
302
  | MResetAssign _ -> reset_instances
298 303
  (* TODO: handle clear_reset *)
299 304
  | MClearReset -> reset_instances
300 305
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)

Also available in: Unified diff