| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
| |
cfrontend/C2C.ml
|
| |
|
|
|
|
|
|
|
| |
Move its definitions to modules C (the type `builtins`) and Env
(the operations that deal with the initial environment).
Reasons for the refactoring:
1- The name "Builtins" will soon be reused for a Coq module
2- `Env.initial()` makes more sense than `Builtins.environment()`.
|
| |
|
|
|
|
|
| |
In order to avoid adding ranges to the wrong scopes due to
inlining they are numbered consecutively for the whole compilation
unit.
Bug 26234
|
| |
|
|
|
|
| |
Fix various typos in diagnostic messages and unified wording and
capitalization.
Bug 23850
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/
* Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the
Diagnostics module.
* Raise on error before calling external tools.
* Added diagnostics to clightgen.
* Fix error handling of AsmToJson.
* Cleanup error handling of Elab and C2C.
*The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
|
| |
|
|
|
|
| |
If the label is on a different line than the code we can still
emit a line directive for the label.
Bug 21232
|
| | |
|
| |
|
|
|
|
|
| |
Since before a case statement is potentially unreachable code due
to break, etc. it is better to skip printing line information
directly before the case statement and print it afterwards.
Bug 21232
|
| |
|
|
|
|
|
|
|
|
| |
Now each warning either has a name and can be turned on/off, made
into an error,etc. or is a warning that always will be triggered.
The message of the warnings are similar to the ones emited by
gcc/clang and all fit into one line.
Furthermore the diagnostics are now colored if colored output is
available.
Bug 18004
|
| |
|
|
|
|
| |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
| |
|
|
|
|
| |
Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
|
| |
|
|
| |
Use tail-recursive operations to implement transformations on initializers for global arrays. This way, very large static initializers no longer cause stack overflows at compile-time.
|
| | |
|
| |
|
|
|
|
| |
Local variables are now added with bogus lexical scopes to reflect
the actually lexical scopes. Also this commit fixes assembler problems
of the das when a user section with the name ".text" is defined.
|
| |\
| |
| |
| |
| | |
Conflicts:
cparser/Unblock.ml
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
|
|
| |
Instead of creating separate annotations for the local variables
we call the Debug.add_lvar_scope and we construct a mapping from
function id + scope id to scope information.
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
| |
Elab: Handle C99 designated initializers.
C2C, Initializers: more precise intermediate AST for initializers.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
| |
cparser: add primitive support for enum types.
bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
| |
cparser: renamed Errors to Cerrors; removed packing into Cparser.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
