diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 17:12:27 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 17:12:27 +0100 |
| commit | 1acafe8f7f61a8908f47de4c98f3d873f8f9afbd (patch) | |
| tree | eb32229e985eb5b5150ce173f3f9ff120a6bac08 /backend/Duplicate.v | |
| parent | 6bb5ae7ee76bee8b8be0c99363975bafa5753c0b (diff) | |
| download | compcert-kvx-1acafe8f7f61a8908f47de4c98f3d873f8f9afbd.tar.gz compcert-kvx-1acafe8f7f61a8908f47de4c98f3d873f8f9afbd.zip | |
Verificator finished for handling reversed Icond
Diffstat (limited to 'backend/Duplicate.v')
| -rw-r--r-- | backend/Duplicate.v | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index c53ff425..18869f39 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -138,12 +138,15 @@ Definition verify_match_inst dupmap inst tinst := | Icond cond lr n1 n2 => match tinst with | Icond cond' lr' n1' n2' => - do u1 <- verify_is_copy dupmap n1 n1'; - do u2 <- verify_is_copy dupmap n2 n2'; - if (eq_condition cond cond') then - if (list_eq_dec Pos.eq_dec lr lr') then OK tt - else Error (msg "Different lr in Icond") - else Error (msg "Different cond in Icond") + if (list_eq_dec Pos.eq_dec lr lr') then + if (eq_condition cond cond') then + do u1 <- verify_is_copy dupmap n1 n1'; + do u2 <- verify_is_copy dupmap n2 n2'; OK tt + else if (eq_condition (negate_condition cond) cond') then + do u1 <- verify_is_copy dupmap n1 n2'; + do u2 <- verify_is_copy dupmap n2 n1'; OK tt + else Error (msg "Incompatible conditions in Icond") + else Error (msg "Different lr in Icond") | _ => Error (msg "verify_match_inst Icond") end | Ijumptable r ln => match tinst with |