diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-04 19:46:40 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-04 19:46:40 +0200 |
| commit | fcb50cc5284a006bde4eda21431dc811412cf819 (patch) | |
| tree | c06b71abe3c7086e028de6c78c352b2d0974f89c /backend/CSEdomain.v | |
| parent | 55a90812e9f6f65b4abe7a124e933875f212238c (diff) | |
| download | compcert-kvx-fcb50cc5284a006bde4eda21431dc811412cf819.tar.gz compcert-kvx-fcb50cc5284a006bde4eda21431dc811412cf819.zip | |
stuck in CSEproof
Diffstat (limited to 'backend/CSEdomain.v')
| -rw-r--r-- | backend/CSEdomain.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v index aa0b9fb1..26d9c481 100644 --- a/backend/CSEdomain.v +++ b/backend/CSEdomain.v @@ -109,7 +109,16 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem): | load_eval_to: forall trap chunk addr vl a v, eval_addressing ge sp addr (map valu vl) = Some a -> Mem.loadv chunk m a = Some v -> - rhs_eval_to valu ge sp m (Load trap chunk addr vl) v. + rhs_eval_to valu ge sp m (Load trap chunk addr vl) v + | load_notrap1_eval_to: forall chunk addr vl, + eval_addressing ge sp addr (map valu vl) = None -> + rhs_eval_to valu ge sp m (Load NOTRAP chunk addr vl) + (default_notrap_load_value chunk) + | load_notrap2_eval_to: forall chunk addr vl a, + eval_addressing ge sp addr (map valu vl) = Some a -> + Mem.loadv chunk m a = None -> + rhs_eval_to valu ge sp m (Load NOTRAP chunk addr vl) + (default_notrap_load_value chunk). Inductive equation_holds (valu: valuation) (ge: genv) (sp: val) (m: mem): equation -> Prop := |