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 /cparser | |
| parent | 3bdb983e0b21c8d45e85aff08278475396038f4f (diff) | |
| download | compcert-kvx-08efc2a09b850476e39469791650faf99dd06183.tar.gz compcert-kvx-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 'cparser')
0 files changed, 0 insertions, 0 deletions