diff options
| author | Pierre Goutagny <pierre.goutagny@ens-lyon.fr> | 2021-06-04 13:45:59 +0200 |
|---|---|---|
| committer | Pierre Goutagny <pierre.goutagny@ens-lyon.fr> | 2021-06-04 13:45:59 +0200 |
| commit | 731d22f1b917a3e55deb82505fc5f981b4a37bcc (patch) | |
| tree | f43fb9cdbbe7784432871cfe9b81c3104c61731a /backend | |
| parent | 245f4f86865ce62b82242af81897936b5034438a (diff) | |
| download | compcert-kvx-731d22f1b917a3e55deb82505fc5f981b4a37bcc.tar.gz compcert-kvx-731d22f1b917a3e55deb82505fc5f981b4a37bcc.zip | |
Fix check_instr Icond target conditions
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/RTLTunneling.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v index 4885002f..e6901a9f 100644 --- a/backend/RTLTunneling.v +++ b/backend/RTLTunneling.v @@ -63,8 +63,8 @@ Definition check_instr (td: UF) (pc: node) (i: instruction): res unit := | Icond _ _ ifso ifnot _ => let (tso,dso) := get td ifso in let (tnot,dnot) := get td ifnot in - if peq tpc ifso then - if peq tpc ifnot then + if peq tpc tso then + if peq tpc tnot then if zlt dso dpc then if zlt dnot dpc then OK tt else Error (msg "bad distance on else branch") |