diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-02-24 13:56:07 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-24 13:56:07 +0100 |
| commit | 08efc2a09b850476e39469791650faf99dd06183 (patch) | |
| tree | f83f23a30d7e374a2b1f3b616e1bcb7396498baf /x86/Asmexpand.ml | |
| parent | 3bdb983e0b21c8d45e85aff08278475396038f4f (diff) | |
| download | compcert-08efc2a09b850476e39469791650faf99dd06183.tar.gz compcert-08efc2a09b850476e39469791650faf99dd06183.zip | |
Platform-independent implementation of Conventions.size_arguments (#222)
The "size_arguments" function and its properties can be systematically
derived from the "loc_arguments" function and its properties.
Before, the RISC-V port used this derivation, and all other ports
used hand-written "size_arguments" functions and proofs.
This commit moves the definition of "size_arguments" to the
platform-independent file backend/Conventions.v, using the systematic
derivation, and removes the platform-specific definitions.
This reduces code and proof size, and makes it easier to change the
calling conventions.
Diffstat (limited to 'x86/Asmexpand.ml')
| -rw-r--r-- | x86/Asmexpand.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index c82d406e..b8353046 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -251,7 +251,7 @@ let expand_builtin_va_start_32 r = invalid_arg "Fatal error: va_start used in non-vararg function"; let ofs = Int32.(add (add !PrintAsmaux.current_function_stacksize 4l) - (mul 4l (Z.to_int32 (Conventions1.size_arguments + (mul 4l (Z.to_int32 (Conventions.size_arguments (get_current_function_sig ()))))) in emit (Pleal (RAX, linear_addr RSP (Z.of_uint32 ofs))); emit (Pmovl_mr (linear_addr r _0z, RAX)) |