Skip to content
  • Xavier Leroy's avatar
    Platform-independent implementation of Conventions.size_arguments (#222) · 08efc2a0
    Xavier Leroy authored
    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.
    08efc2a0