From dd4767e17235adb5de922626ed1fea15f4eb9e3b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 6 Apr 2021 23:37:22 +0200 Subject: Important commit on expansions' mini CSE, and a draft for addptrofs --- riscV/Asm.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'riscV/Asm.v') diff --git a/riscV/Asm.v b/riscV/Asm.v index 5d3518f2..a16f57b5 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -982,6 +982,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | Pbuiltin ef args res => Stuck (**r treated specially below *) + | Pnop => Next (nextinstr rs) m (**r Pnop is used by an oracle during expansion *) (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) @@ -1002,7 +1003,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfmsubd _ _ _ _ | Pfnmaddd _ _ _ _ | Pfnmsubd _ _ _ _ - | Pnop => Stuck end. -- cgit