diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-18 11:23:37 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-18 11:23:37 +0200 |
commit | 52e4d71646c07fe32665696ef27523c48c69f127 (patch) | |
tree | 664d46d350ad90be43f4157dcb452898da1d3192 /arm/Asm.v | |
parent | d8dcf41334d7a6ff2d2eaa53f215c80ef26cd517 (diff) | |
parent | f66711dc06c73adf3dd715c564cb6d27b51c5199 (diff) | |
download | compcert-52e4d71646c07fe32665696ef27523c48c69f127.tar.gz compcert-52e4d71646c07fe32665696ef27523c48c69f127.zip |
Merge remote-tracking branch 'private/master'
Diffstat (limited to 'arm/Asm.v')
-rw-r--r-- | arm/Asm.v | 9 |
1 files changed, 6 insertions, 3 deletions
@@ -199,15 +199,16 @@ Inductive instruction : Type := | Pfsts: freg -> ireg -> int -> instruction (**r float32 store *) (* Pseudo-instructions *) - | Pallocframe: Z -> ptrofs -> instruction (**r allocate new stack frame *) - | Pfreeframe: Z -> ptrofs -> instruction (**r deallocate stack frame and restore previous frame *) - | Plabel: label -> instruction (**r define a code label *) + | Pallocframe: Z -> ptrofs -> instruction (**r allocate new stack frame *) + | Pfreeframe: Z -> ptrofs -> instruction (**r deallocate stack frame and restore previous frame *) + | Plabel: label -> instruction (**r define a code label *) | Ploadsymbol: ireg -> ident -> ptrofs -> instruction (**r load the address of a symbol *) | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *) | Padc: ireg -> ireg -> shift_op -> instruction (**r add with carry *) | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) + | Pcfi_rel_offset: int -> instruction (**r .cfi_rel_offset debug directive *) | Pclz: ireg -> ireg -> instruction (**r count leading zeros. *) | Pfsqrt: freg -> freg -> instruction (**r floating-point square root. *) | Prev: ireg -> ireg -> instruction (**r reverse bytes and reverse bits. *) @@ -757,6 +758,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | _ => Stuck end + | Pcfi_rel_offset ofs => + Next (nextinstr rs) m | Pbuiltin ef args res => Stuck (**r treated specially below *) (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) |