Project

General

Profile

« Previous | Next » 

Revision aaa8e454

Added by Lélio Brun 7 months ago

it works

View differences:

src/machine_code_common.ml
54 54
      fun fmt e -> pp_expr m fmt e
55 55
    in
56 56
    match p with
57
    | Transition (f, inst, i, inputs, locals, outputs) ->
57
    | Transition (f, inst, i, inputs, locals, outputs, _r, _mems) ->
58 58
      fprintf fmt "Transition_%a<%a>%a%a"
59 59
        pp_print_string f
60 60
        (pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF")
61 61
           pp_print_string) inst
62 62
        (pp_print_option pp_print_int) i
63 63
        (pp_print_parenthesized pp_expr) (inputs @ locals @ outputs)
64
    | Reset (f, inst, r) ->
65
      fprintf fmt "Reset_%a<%a> on %a"
66
        pp_print_string f
67
        pp_print_string inst
68
        (pp_val m) r
64 69
    | MemoryPack (f, inst, i) ->
65 70
      fprintf fmt "MemoryPack_%a<%a>%a"
66 71
        pp_print_string f
......
102 107
        pp_predicate m fmt p
103 108
      | StateVarPack r ->
104 109
        fprintf fmt "StateVarPack<%a>" pp_reg r
105
      | ExistsMem (rc, tr) ->
106
        fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [rc; tr])
110
      | ExistsMem (_f, a, b) ->
111
        fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [a; b])
107 112
    in
108 113
    pp_spec
109 114

  

Also available in: Unified diff