| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
| |
operations with undefined behaviors.
Consider (x ^ 1) ^ 1 where x is a intptr_t containing a pointer value. "x ^ 1" evaluates to Vundef in the CompCert semantics, hence the value analysis, in strict mode, gives abstract result Ifptr Pbot (= any number but not a pointer). In relaxed mode, we now give abstract result Ifptr (poffset p) where p is the abstraction of the pointer, thus keeping track of the actual leak of the pointer value.
|
|
|
|
| |
Val.lessdef, etc.
|
|
|
|
|
|
|
|
|
|
| |
variables whose address is taken.
- CminorSel, RTL: add "annot" instructions.
- CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions.
- AST, Events: simplify EF_annot because constants are now part of the arguments.
Implementation is not complete yet.
|
|\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- Switch CompCert C / Clight AST of composite types (structs and unions)
from a structural representation to a nominal representation,
closer to concrete syntax.
- This avoids algorithmic inefficiencies due to the structural representation.
- Closes PR#4.
- Smallstep: make small-step semantics more polymorphic in the type of the
global environment.
- Globalenvs: introduce Senv.t (symbol environments) as a restricted view
on Genv.t (full global environments).
- Events, Smallstep: use Senv instead of Genv to talk about global names.
|
| |
| |
| |
| | |
environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
|
| |
| |
| |
| | |
global const variable.
|
|/
|
|
|
|
|
| |
In the presence of separate compilation and linking, an uninitialized
const global variable may be initialized elsewhere with a pointer value,
falsifying the points-to analysis. Report and fix by Chung-Kil Hur
and Jeehoon Kang.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
support saving and restoring registers without knowing
the exact types (int/single/float) of their contents, just
their sizes.
- Memory model: generalize the opaque encoding of pointers to
apply to any value, not just pointers, if chunks Many32/Many64
are selected.
- More properties of FP arithmetic proved.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
Refactored compilation flags that affect the Coq part (module Compopts).
Added support for C99 for loops with declarations.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
NeedOp, Deadcode: must have distinct needs per argument of an operator.
This change remains to be propagated to IA32 and PPC.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
__builtin_memcpy_aligned now supports the case sz = 0.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2392 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|