diff options
| -rw-r--r-- | x86/Machregs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/x86/Machregs.v b/x86/Machregs.v index 741081a6..04be0cd6 100644 --- a/x86/Machregs.v +++ b/x86/Machregs.v @@ -196,7 +196,7 @@ Definition destroyed_by_setstack (ty: typ): list mreg := end. Definition destroyed_at_indirect_call: list mreg := - nil. + AX :: nil. Definition temp_for_parent_frame: mreg := AX. |