diff options
Diffstat (limited to 'kvx/Asm.v')
-rw-r--r-- | kvx/Asm.v | 7 |
1 files changed, 6 insertions, 1 deletions
@@ -35,12 +35,14 @@ Require Import Smallstep. Require Import Locations. Require Stacklayout. Require Import Conventions. -Require Import Asmvliw. +Require Export Asmvliw. Require Import Linking. Require Import Errors. (** Definitions for OCaml code *) Definition label := positive. + +(* Necessary definition for Asmexpandaux.mli *) Definition preg := preg. Inductive addressing : Type := @@ -102,6 +104,9 @@ Inductive instruction : Type := | Palclrd (dst: ireg) (addr: ireg) | Palclrw (dst: ireg) (addr: ireg) | Pclzll (rd rs: ireg) + | Pclzw (rd rs: ireg) + | Pctzll (rd rs: ireg) + | Pctzw (rd rs: ireg) | Pstsud (rd rs1 rs2: ireg) (** Loads *) |