From c9d01df3577a23e20abbe934f6f36f17dbbb82cd Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 17 Aug 2017 09:45:44 +0200 Subject: ARM: Generate Pcfi_rel_offset directives directly from Asmgen This is what we do for PowerPC and is more resilient to changes in code generation. We need to give Pcfi_rel_offset a dynamic semantics, but that's just a no-op. --- arm/Asm.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'arm/Asm.v') diff --git a/arm/Asm.v b/arm/Asm.v index 6ba09a8f..7a393139 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -773,13 +773,14 @@ 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. *) | Ppush _ | Padc _ _ _ | Pcfi_adjust _ - | Pcfi_rel_offset _ | Pclz _ _ | Prev _ _ | Prev16 _ _ -- cgit