diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2021-06-01 14:58:05 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2021-06-01 14:58:05 +0200 |
| commit | 75a2885f610e1d6e91df8e2386a4a4559b615bb9 (patch) | |
| tree | 4456fa4a9876bc73d3d08b6dad1ad8f2f836578c /riscV/Asm.v | |
| parent | 22504b61be43e5d4a97db621ce3c1785618bbaf0 (diff) | |
| parent | c44fc24eb6111c177d1d6fc973a366ebf646202b (diff) | |
| download | compcert-kvx-75a2885f610e1d6e91df8e2386a4a4559b615bb9.tar.gz compcert-kvx-75a2885f610e1d6e91df8e2386a4a4559b615bb9.zip | |
Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1
Diffstat (limited to 'riscV/Asm.v')
| -rw-r--r-- | riscV/Asm.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/Asm.v b/riscV/Asm.v index 7e8ba760..2bc6d956 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. |