diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-08 16:53:08 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-08 16:53:08 +0200 |
| commit | 7df2b7d824f3187f1936685629c06d1028fdc243 (patch) | |
| tree | 0d466d7ccab5225f25e1c68ee7382cb8b416851c /mppa_k1c/Asmvliw.v | |
| parent | be40bfa8516ab7c2b2f5d5c542af73a4f7b8148e (diff) | |
| download | compcert-kvx-7df2b7d824f3187f1936685629c06d1028fdc243.tar.gz compcert-kvx-7df2b7d824f3187f1936685629c06d1028fdc243.zip | |
asmblockgen works
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index bfe9d77b..9508bfbd 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -313,7 +313,7 @@ Inductive cf_instruction : Type := . (** Loads **) -Definition concrete_default_notrap_load_value chunk := +Definition concrete_default_notrap_load_value (chunk : memory_chunk) := match chunk with | Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned | Mint32 => Vint Int.zero |