| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |\ |
|
| | |
| |
| |
| |
| | |
The name_of_register and register_of_name function are shared between
all architectures and can be moved in a common file.
|
| | |
| |
| |
| |
| | |
The function is in fact just a call to the
function`is_callee_save_register` from `Conventions1.v`.
|
| |/ |
|
| |
|
|
|
|
|
|
| |
Most of the code can be String.uppercase usages can either be
replaced by a more specialized version of coqstring_of_camlstring
(which is also slightly more effecient) or by specialized checks
that reject wrong code earlier.
Bug 19187
|
| |
|
|
|
|
|
|
|
|
| |
- Treat clobbered registers as being destroyed by EF_inline_asm builtins
(which is the truth, semantically).
- To enable the above, represent clobbers as Coq strings rather than idents
and move register_by_name from Machregsaux.ml to Machregs.v.
- Side benefit: more efficient implementation of Machregsaux.name_of_register.
-# Please enter the commit message for your changes. Lines starting
|
| |
|
|
| |
clobber lists.
|
| | |
|
|
|
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1327 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
