diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-25 15:03:55 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-25 15:03:55 +0100 |
| commit | b2171eb8e6af1d0a19bd42fb455fccc7e9f34fe9 (patch) | |
| tree | a9bee767baf0c3e9077890c5c4938e5fb0f8ceb0 /backend/CSE3analysis.v | |
| parent | c55522c71d7ed2542bfd50d466dbeb520bde21f4 (diff) | |
| download | compcert-kvx-b2171eb8e6af1d0a19bd42fb455fccc7e9f34fe9.tar.gz compcert-kvx-b2171eb8e6af1d0a19bd42fb455fccc7e9f34fe9.zip | |
cond_valid_pointer_eq
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 8b7f1190..84f4a426 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -160,6 +160,20 @@ Proof. decide equality. Defined. +Record condition_fact := + mkcondition_fact + { cond_op : condition ; + cond_args : list reg }. + +Definition eq_dec_condition_fact : + forall cf cf' : condition_fact, {cf = cf'} + {cf <> cf'}. +Proof. + generalize peq. + generalize eq_condition. + generalize eq_dec_args. + decide equality. +Defined. + Definition eq_id := node. Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := |