diff options
Diffstat (limited to 'backend/LTL.v')
-rw-r--r-- | backend/LTL.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/backend/LTL.v b/backend/LTL.v index 48c5c850..bb596fa2 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -111,10 +111,7 @@ Definition call_regs (caller: locset) : locset := Definition return_regs (caller callee: locset) : locset := fun (l: loc) => match l with - | R r => - if In_dec mreg_eq r destroyed_at_call - then callee (R r) - else caller (R r) + | R r => if is_callee_save r then caller (R r) else callee (R r) | S sl ofs ty => caller (S sl ofs ty) end. |