Project

General

Profile

« Previous | Next » 

Revision 6d1693b9

Added by LĂ©lio Brun 7 months ago

work on spec generation almost done

View differences:

src/backends/Horn/horn_backend_printers.ml
295 295
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
296 296
  match get_instr_desc instr with
297 297
  | MSpec _ | MComment _ -> reset_instances
298
  (* TODO: handle clear_reset *)
299
  | MClearReset -> reset_instances
298 300
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
299 301
    pp_no_reset machines m fmt i;
300 302
    i::reset_instances
301
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
303
  | MSetReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
302 304
    pp_instance_reset machines m fmt i;
303 305
    i::reset_instances
304 306
  | MLocalAssign (i,v) ->

Also available in: Unified diff