diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-02-22 16:57:02 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:06 +0200 |
| commit | f1d3dbb3fa70233d1ad83ae88876dd384346a16a (patch) | |
| tree | 356dd54e5ae0a960eaa60a7b174ceb4fa750f9fc /mppa_k1c/Op.v | |
| parent | 6a3f3a62452670380827f9e39dd28c5092741099 (diff) | |
| download | compcert-kvx-f1d3dbb3fa70233d1ad83ae88876dd384346a16a.tar.gz compcert-kvx-f1d3dbb3fa70233d1ad83ae88876dd384346a16a.zip | |
Changed ptr64 to be always true
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index bb04f786..74101f53 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -522,7 +522,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* addrsymbol *) - unfold Genv.symbol_address. destruct (Genv.find_symbol genv id)... (* addrstack *) - - destruct sp... apply Val.Vptr_has_type. + - destruct sp... (* castsigned *) - destruct v0... - destruct v0... @@ -532,8 +532,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* neg, sub *) - destruct v0... - unfold Val.sub. destruct v0; destruct v1... - unfold Val.has_type; destruct Archi.ptr64... - destruct Archi.ptr64... destruct (eq_block b b0)... (* mul, mulhs, mulhu *) - destruct v0; destruct v1... - destruct v0; destruct v1... @@ -582,7 +580,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0... - unfold Val.subl. destruct v0; destruct v1... unfold Val.has_type; destruct Archi.ptr64... - destruct Archi.ptr64... destruct (eq_block b b0)... + destruct (eq_block b b0)... (* mull, mullhs, mullhu *) - destruct v0; destruct v1... - destruct v0; destruct v1... |