diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-10-27 16:26:08 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-10-27 16:26:08 +0200 |
commit | 9922feea537ced718a3822dd50eabc87da060338 (patch) | |
tree | 6f67bb6707ef59e50d6bb81c61b2ed0b3c6097ab /backend/Inlining.v | |
parent | f2d6637c7d4a11f961ff289e64f70bf4de93d0aa (diff) | |
parent | d50773e537ec6729f9152b545c6f938ab19eb7b8 (diff) | |
download | compcert-9922feea537ced718a3822dd50eabc87da060338.tar.gz compcert-9922feea537ced718a3822dd50eabc87da060338.zip |
Merge pull request #145 from AbsInt/64
Support for 64-bit target processors + support for x86 in 64-bit mode
Diffstat (limited to 'backend/Inlining.v')
-rw-r--r-- | backend/Inlining.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/backend/Inlining.v b/backend/Inlining.v index 5c8f4419..61776743 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -192,16 +192,16 @@ Definition sregs (ctx: context) (rl: list reg) := List.map (sreg ctx) rl. Definition sros (ctx: context) (ros: reg + ident) := sum_left_map (sreg ctx) ros. Definition sop (ctx: context) (op: operation) := - shift_stack_operation (Int.repr ctx.(dstk)) op. + shift_stack_operation ctx.(dstk) op. Definition saddr (ctx: context) (addr: addressing) := - shift_stack_addressing (Int.repr ctx.(dstk)) addr. + shift_stack_addressing ctx.(dstk) addr. Fixpoint sbuiltinarg (ctx: context) (a: builtin_arg reg) : builtin_arg reg := match a with | BA x => BA (sreg ctx x) - | BA_loadstack chunk ofs => BA_loadstack chunk (Int.add ofs (Int.repr ctx.(dstk))) - | BA_addrstack ofs => BA_addrstack (Int.add ofs (Int.repr ctx.(dstk))) + | BA_loadstack chunk ofs => BA_loadstack chunk (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk))) + | BA_addrstack ofs => BA_addrstack (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk))) | BA_splitlong hi lo => BA_splitlong (sbuiltinarg ctx hi) (sbuiltinarg ctx lo) | _ => a end. @@ -437,13 +437,13 @@ Definition expand_function (fenv: funenv) (f: function): mon context := Local Open Scope string_scope. (** Inlining can increase the size of the function's stack block. We must - make sure that the new size does not exceed [Int.max_unsigned], otherwise + make sure that the new size does not exceed [Ptrofs.max_unsigned], otherwise address computations within the stack would overflow and produce incorrect results. *) Definition transf_function (fenv: funenv) (f: function) : Errors.res function := let '(R ctx s _) := expand_function fenv f initstate in - if zlt s.(st_stksize) Int.max_unsigned then + if zlt s.(st_stksize) Ptrofs.max_unsigned then OK (mkfunction f.(fn_sig) (sregs ctx f.(fn_params)) s.(st_stksize) |