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 /test/spass/.depend | |
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 'test/spass/.depend')
0 files changed, 0 insertions, 0 deletions