| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
| |
As observed by B. Schommer, it is not enough to track scopes for every source line, as blocks can occur on a single line (think macros). Hence:
- Revert debug annotations of kind 1 to contain only line number info.
Generate them only when the line number changes.
- Use debug annotations of kind 6 to record the list of active scopes
(as BA_int integer arguments to __builtin_annot). Generate them
before every nontrivial statement, even if on the same line as others.
- Remove the generation of "variable x is declared in scope N" debug
annotations. This can be tracked separately and more efficiently.
|
|
|
|
|
|
|
|
|
|
|
| |
C2C: the code that insert debug builtins with the line numbers is now
in Unblock. Handle calls to __builtin_debug.
Unblock: generate __builtin_debug(1) for line numbers, carrying
the list of active scopes as extra arguments.
Generate __builtin_debug(6) for local variable declarations,
carrying the corresponding scope number as extra argument.
Constprop: avoid duplicating debug arguments that are constants already.
PrintAsmaux: show this extra debug info as comments.
|
|
|
|
|
| |
The transformation is the same as the one used for structs but packing
always stops after each member.
|
|
|
|
|
| |
If they only report an error an assertion failure in Reame.ml was
triggered.
|
|
|
|
| |
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.
|