| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
| |
Share the testing code for built-in functions that are available on
all target platforms.
Improve testing of __builtin_clz* and __builtin_ctz*
|
| |
|
|
|
|
|
|
|
|
| |
Now that some builtin functions have known semantics, constant
propagation can happen in this test. This defeats the purpose,
which is to check that the correct processor instructions are generated.
To prevent this constant propagation, we move the initialized
variables to global scope. Since they are not "const", their
values are not known to the optimizer.
|
|
|
-> x86/x86_32/x86_64
Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq.
This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86.
While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures.
Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
|
