diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-03 17:02:26 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-03 17:02:26 +0200 |
| commit | 40d48f68d02b21905016e9ee2e529be22e34ca9d (patch) | |
| tree | 6bd6b79a6635991c310c1eae97827d8d18e1d577 /aarch64/Asmblock.v | |
| parent | 6fd50b465026cafce0c52fbee322a109108d0578 (diff) | |
| download | compcert-kvx-40d48f68d02b21905016e9ee2e529be22e34ca9d.tar.gz compcert-kvx-40d48f68d02b21905016e9ee2e529be22e34ca9d.zip | |
fixing type of PLoad and PStore
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 9d368d35..ae23cb93 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -561,8 +561,8 @@ Inductive ar_instruction : Type := Inductive basic : Type := | PArith (i: ar_instruction) (**r TODO *) - | PLoad (ld: load_rd_a) (rd: ireg) (a: addressing) (**r TODO *) - | PStore (st: store_rs_a) (r: ireg) (a: addressing) (**r TODO *) + | PLoad (ld: load_rd_a) (rd: preg) (a: addressing) (**r TODO *) + | PStore (st: store_rs_a) (r: preg) (a: addressing) (**r TODO *) | Pallocframe (sz: Z) (linkofs: ptrofs) (**r allocate new stack frame *) | Pfreeframe (sz: Z) (linkofs: ptrofs) (**r deallocate stack frame and restore previous frame *) | Ploadsymbol (rd: ireg) (id: ident) (**r load the address of [id] *) @@ -1283,7 +1283,7 @@ Definition exec_cfi (f: function) (cfi: cf_instruction) (rs: regset) (m: mem) : end end. -Definition arith_eval_r i := +Definition arith_eval_r (i:arith_r): val := match i with (* XXX change from ge to lk similar to ADadr change *) | Padrp id ofs => symbol_high lk id ofs |