diff options
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 := |