aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Cminortyping.v
Commit message (Collapse)AuthorAgeFilesLines
* finish merging master branch (fixes problems in glpk colamd)David Monniaux2019-06-061-35/+0
|
* Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-06-061-5/+42
|\
| * Cminortyping: relax typechecking of function callsXavier Leroy2019-06-061-12/+15
| | | | | | | | | | | | | | Sometimes the result of a void function is assigned to a variable. This can occur with C conditional expressions ?: at type void, e.g. the "assert" macro of MacOS. A similar relaxation was already there in RTLtyping.
| * Type inference and type checking for CminorXavier Leroy2019-06-061-0/+797
| | | | | | | This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.
* Type inference and type checking for CminorXavier Leroy2019-05-311-0/+798
This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.