| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
| |
Instead of reimplementing the whole scope handling in the debug information
use the existing functionality and fill the scopes explicitly in the functions.
|
|
|
|
|
|
| |
Scopes will be handled by a stack of all open scopes. This stack
then can also be used to generate the debug directives to track the
scopes through the rest of the passes.
|
|
|
|
|
| |
Introduced a new dwarf generation from the information collected in
the DebugInformation and removed the old CtODwarf translation.
|
|
|
|
|
|
| |
Added functions to add more information to the debuging interface,
like the struct layout with offsets, bitifiled layout and removed
the no longer needed mapping from stamp to atom.
|
|
|
|
| |
structured builtin arguments and results.
|
|
|
|
| |
static variables to avoid problems with files such as "a b.c".
|
| |
|
|
|
|
| |
parameter.
|
| |
|
|
|
|
|
|
| |
The copy optimization is not correct in case of overlap between destination
and source. We would need to use an hypothetical __builtin_memmove_aligned
that can cope with overlap to implement the copy at return of callee.
|
|
|
|
|
|
|
|
| |
As per ISO C99, "hosted environment".
"return 0" is added at the end of any function named "main" that has
"int" as return type. If the name is "main" but the return type is
not "int", emit a warning and do not add anything.
|
|
|
|
| |
Also: improve error message by showing old and new types.
|
|
|
|
|
|
| |
cparser/Bitfields.ml: when assigning to a bit field of type _Bool, the
right-hand side must be normalized to 0 or 1 via a cast to _Bool.
test/regression/bitfields{1,9}.c: add corresponding test cases.
|
|\ |
|
| | |
|
|/ |
|
|\
| |
| |
| |
| | |
Conflicts:
driver/Driver.ml
|
| | |
|
|\| |
|
| |
| |
| |
| |
| | |
Otherwise we get too many errors on glibc's standard headers.
A real error will occur when the anonymous struct/union is accessed.
|
| |
| |
| |
| | |
variable is redefined as a typedef.
|
|/ |
|
| |
|
|
|
|
| |
non-static declaration is followed by a static declaration/definition.
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
| |
and produce a diagnostic instead of ignoring them.
|
|
|
|
| |
bit field.
|
|
|
|
| |
unblocking; improve translation of bitfield initializers and compound literals.
|
|
|
|
|
|
| |
Bitfields: better translation of initializers and compound literals; run this pass before unblocking.
Transform.stmt: extend with ability to treat unblocked code.
test/regression: more bitfield tests.
|
|
|
|
| |
clobber lists.
|
|
|
|
|
| |
We can ignore alternatives as long as one of the constraints we
handle (r, m, i, n) is there.
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
- support "r", "m" and "i" constraints
- support "%Q" and "%R" modifiers for register pairs
- support register clobbers
- split off analysis and transformation of asm statements in
cparser/ExtendedAsm.ml
|
| |
|
|\ |
|
| |
| |
| |
| | |
integer or floating constants.
|
|\|
| |
| |
| |
| |
| | |
Conflicts:
Makefile
driver/Driver.ml
|
| |
| |
| |
| | |
nicely.
|
| |
| |
| |
| |
| |
| |
| |
| | |
composites).
- Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD.
- Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions.
- More comprehensive interoperability test in regression/interop1.c.
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
configure: special ABI value for IA32/MacOSX and PowerPC/Linux
cparser/Machine: special config for PowerPC/Linux
cparser/StructReturn: generate better code for return-as-int
driver/Clflags, driver/Driver: add options -fstruct-return=<convention>
and -fstruct-passing=<convention> to simplify testing
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The passing of struct/union arguments by value implemented in the verified
part of CompCert is not compatible with the ARM, PowerPC and x86 ABI.
Here we enrich the StructReturn source-to-source emulation pass
so that it implements the calling conventions defined in these ABIs.
Plus: for x86, implement the returning of struct/union results by value
in a way compatible with the ABI.
|
| | |
| | |
| | |
| | | |
transformations.
|
| | |
| | |
| | |
| | | |
printing of packed structs.
|
| |/
|/| |
|
|/
|
|
|
|
| |
- Error instead of warning if escape sequence overflows one character.
- Wrong normalization of L'x' to char instead of wchar_t.
- More careful overflow tests.
|
|\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- 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.
|
| |
| |
| |
| |
| | |
Use these constructor functions in C2C to rely less on the types produced
by the unverified elaborator.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Several definitions in Cutil and elsewhere were accessing the default
value of !Machine.config, before it is properly initialized in Driver.
Delay evaluation of these definitions, and initialize Machine.config
to nonsensical values so that lack of initialization is caught early
(e.g. in Cutil.find_matching_*_kind).
Also, following up on commit [3b8a094], don't use "wchar_t" typedef
to type wide string literals, even if this typedef is in scope.
The risk here is to hide an inconsistency between "wchar_t"'s definition
in standard headers and CompCert's built-in definition.
|