diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-03-27 13:44:24 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-03-27 13:44:24 +0000 |
| commit | 57f18784d1fac0123cdb51ed67ae761100509c1f (patch) | |
| tree | 62442626d829f8605a98aed1cd67f2eda8a9c778 /.depend | |
| parent | 75fea20a8289e4441819b45d7ce750eda1b53ad1 (diff) | |
| download | compcert-57f18784d1fac0123cdb51ed67ae761100509c1f.tar.gz compcert-57f18784d1fac0123cdb51ed67ae761100509c1f.zip | |
Revised division of labor between RTLtyping and Lineartyping:
- RTLtyping no longer keeps track of single-precision floats,
switches from subtype-based inference to unification-based inference.
- Unityping: new library for unification-based inference.
- Locations: don't normalize at assignment in a stack slot
- Allocation, Allocproof: simplify accordingly.
- Lineartyping: add inference of machine registers that contain
a single-precision float.
- Stackingproof: adapted accordingly.
This addresses a defect report by D. Dickman whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2435 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to '.depend')
0 files changed, 0 insertions, 0 deletions