diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-07 09:59:25 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-07 09:59:25 +0100 |
| commit | 7ef1d2eafecfd428e25e3cbf37300ebf73a57c02 (patch) | |
| tree | 0ec2ca7f5a13c01ba5efa5eae3c1b8083cacb066 /mppa_k1c/Asmblockdeps.v | |
| parent | 60d41ee18346ff6725ae62a7fa054708805ac9c4 (diff) | |
| download | compcert-kvx-7ef1d2eafecfd428e25e3cbf37300ebf73a57c02.tar.gz compcert-kvx-7ef1d2eafecfd428e25e3cbf37300ebf73a57c02.zip | |
Experiment Patch of Memory Model
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index aa1e7824..fa21d3b1 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -153,7 +153,7 @@ Definition arith_eval (ao: arith_op) (l: list value) := | OArithRRR n, [Val v1; Val v2; Memstate m] => match n with - | Pcompw c => Some (Val (compare_int c v1 v2 m)) + | Pcompw c => Some (Val (compare_int c v1 v2)) | Pcompl c => Some (Val (compare_long c v1 v2 m)) | _ => None end @@ -195,7 +195,7 @@ Definition arith_eval (ao: arith_op) (l: list value) := | OArithRRI32 n i, [Val v; Memstate m] => match n with - | Pcompiw c => Some (Val (compare_int c v (Vint i) m)) + | Pcompiw c => Some (Val (compare_int c v (Vint i))) | _ => None end |