Project

General

Profile

« Previous | Next » 

Revision 27502d69

Added by LĂ©lio Brun 7 months ago

add memory instances to footprint lemmas

View differences:

src/machine_code_common.ml
58 58
     fun fmt e -> pp_expr m fmt e
59 59
    in
60 60
    match p with
61
    | Transition (f, inst, i, inputs, locals, outputs, _r, _mems) ->
61
    | Transition (f, inst, i, inputs, locals, outputs, _r, _mems, _insts) ->
62 62
      fprintf fmt "Transition_%a<%a>%a%a" pp_print_string f
63 63
        (pp_print_option
64 64
           ~none:(fun fmt () -> pp_print_string fmt "SELF")
......
321 321
  mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
322 322

  
323 323
let mk_conditional ?lustre_eq c t e =
324
  mkinstr ?lustre_eq
325
    (* (Ternary (Val c,
326
     *           And (List.map get_instr_spec t),
327
     *           And (List.map get_instr_spec e))) *)
328
    (MBranch (c, [ tag_true, t; tag_false, e ]))
329

  
330
let mk_branch ?lustre_eq c br =
331
  mkinstr ?lustre_eq
332
    (* (And (List.map (fun (l, instrs) ->
333
     *      Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
334
     *      br)) *)
335
    (MBranch (c, br))
324
  mkinstr ?lustre_eq (MBranch (c, [ tag_true, t; tag_false, e ]))
325

  
326
let mk_branch ?lustre_eq c br = mkinstr ?lustre_eq (MBranch (c, br))
336 327

  
337 328
let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v)
338 329

  
339
let mk_assign ?lustre_eq x v =
340
  mkinstr ?lustre_eq (* (Equal (Var x, Val v)) *) (MLocalAssign (x, v))
330
let mk_assign ?lustre_eq x v = mkinstr ?lustre_eq (MLocalAssign (x, v))
341 331

  
342 332
let arrow_machine =
343 333
  let state = "_first" in
344
  let var_state =
345
    dummy_var_decl state Type_predef.type_bool
346
    (* (Types.new_ty Types.Tbool) *)
347
  in
334
  let var_state = dummy_var_decl state Type_predef.type_bool in
348 335
  let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in
349 336
  let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in
350 337
  let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in

Also available in: Unified diff