diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-02 21:39:20 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-02 21:39:20 +0100 |
| commit | 553714035fc08f9b145b89b3dd7c455f06e917df (patch) | |
| tree | 164f3837a342000eae3addb403b7a189bb2097c6 /backend/Duplicate.v | |
| parent | f0c1cc8327ecf2b1e3021bce66f2d6bb0265f6c0 (diff) | |
| download | compcert-kvx-553714035fc08f9b145b89b3dd7c455f06e917df.tar.gz compcert-kvx-553714035fc08f9b145b89b3dd7c455f06e917df.zip | |
finish merge
Diffstat (limited to 'backend/Duplicate.v')
| -rw-r--r-- | backend/Duplicate.v | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 3ad37c83..46f0855d 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -72,17 +72,19 @@ Definition verify_match_inst dupmap inst tinst := else Error(msg "Different operations in Iop") | _ => Error(msg "verify_match_inst Inop") end - | Iload m a lr r n => match tinst with - | Iload m' a' lr' r' n' => + | Iload tm m a lr r n => match tinst with + | Iload tm' m' a' lr' r' n' => do u <- verify_is_copy dupmap n n'; - if (chunk_eq m m') then - if (eq_addressing a a') then - if (list_eq_dec Pos.eq_dec lr lr') then - if (Pos.eq_dec r r') then OK tt - else Error (msg "Different r in Iload") - else Error (msg "Different lr in Iload") - else Error (msg "Different addressing in Iload") - else Error (msg "Different mchunk in Iload") + if (trapping_mode_eq tm tm') then + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r in Iload") + else Error (msg "Different lr in Iload") + else Error (msg "Different addressing in Iload") + else Error (msg "Different mchunk in Iload") + else Error (msg "Different trapping_mode in Iload") | _ => Error (msg "verify_match_inst Iload") end | Istore m a lr r n => match tinst with @@ -195,4 +197,4 @@ Definition transf_fundef (f: fundef) : res fundef := transf_partial_fundef transf_function f. Definition transf_program (p: program) : res program := - transform_partial_program transf_fundef p.
\ No newline at end of file + transform_partial_program transf_fundef p. |