| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
It is compatible with 8.7.0 and 8.6.1, no changes required to the Coq sources of CompCert.
|
|
|
|
|
|
|
| |
pointers (#209)
Comparisons such as "(uintptr_t) &global == 0x1234" are undefined behavior
in CompCert but their status in ISO C is unclear and they may occur in
real-world code. Make sure they are statically analyzed as Btop.
|
|
|
|
| |
So that it looks more like valid C source.
|
|
|
|
|
|
| |
configure: accept Coq 8.7.0 and 8.6.1.
(Coq 8.6 became incompatible with commit b4f59c4.)
Changelog: updated.
|
|
|
|
| |
It got lost during the addition of the x86-64 port in release 3.0.
|
|
|
|
| |
It is also easier to recognize than the old one for binary analysis tools.
|
| |
|
| |
|
|
|
|
|
|
| |
The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196.
The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _". From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation.
|
| |
|
|
|
|
| |
This happens when the divisor of an unsigned int32 division is constant-propagated to 1.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes.
The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/
This port required the following additional changes:
- Integers: More properties about shrx
- SelectOp: now provides smart constructors for mulhs and mulhu
- SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu.
- Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library.
- test/: add SIMU make variable to run tests through a simulator
- test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers
commit da14495c01cf4f66a928c2feff5c53f09bde837f
Author: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu Apr 13 17:36:10 2017 +0200
RISC-V port, continued
Now working on Asmgen.
commit 36f36eb3a5abfbb8805960443d087b6a83e86005
Author: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed Apr 12 17:26:39 2017 +0200
RISC-V port, first steps
This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
|
| |
|
|
|
|
| |
Follow-up to [29653ba]
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
|
| |
|
| |
|
|
|
|
| |
compatibility, and not "unsigned int", as previously implemented.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Assorted updates to configure and Makefile.
|
|
|
|
| |
from a file or from standard input.
|
| |
|
|
|
|
|
|
|
|
| |
The previous behavior for illegal escape sequences (e.g. '\%') in character
and string literals was to emit an error, then treat "\x" as "x".
As reported by a user, this is dangerous, because the warning can go
unnoticed, and other compilers can treat "\x" as "\\x"
(backslash followed by 'x'). Better to error out.
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2624 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
use case is unclear.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2621 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2620 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
IA32: add __builtin_clz, __builtin_ctz.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|