diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/AsmToJSON.ml | 3 | ||||
| -rw-r--r-- | powerpc/SelectOp.vp | 1 |
2 files changed, 3 insertions, 1 deletions
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index ee3eaca8..ca79a8a2 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -369,7 +369,8 @@ let pp_instructions pp ic = | EF_memcpy _ | EF_runtime _ | EF_vload _ - | EF_vstore _ -> assert false + | EF_vstore _ + | EF_select _ -> assert false end | Pcfi_adjust _ (* Only debug relevant *) | Pcfi_rel_offset _ -> assert false in (* Only debug relevant *) diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 41bc0efc..cf2c8de4 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -43,6 +43,7 @@ Require Import Integers. Require Import Floats. Require Import Op. Require Import CminorSel. +Require Archi. Local Open Scope cminorsel_scope. |