| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |\| | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
needed.
|
| | | | | | | |
|
| | | |_|_|/
| | |/| | |
| | | | | |
| | | | | | |
In test_int64.c: don't test FP->int64 conversions when the FP argument is out of range.
|
| | | | | | |
|
| |/ / / /
| | | | |
| | | | |
| | | | | |
is that every symbol must start with an "_".
|
| | |_|/
| |/| |
| | | |
| | | |
| | | |
| | | | |
Cexec: record names of rules used in every reduction.
Interp: print these rule names in -trace mode. Also: simplified the exploration in "-all" mode; give unique names to states.
Csem: fix name of reduction rule "red_call".
|
| | | | |
|
|\| | | |
|
| | | |
| | | |
| | | |
| | | | |
functions used in the arm and ia32 backend.
|
|\| | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Instead of assuming name uniqueness for all definitions in the program,
these variants only assume uniqueness for a particular name.
Use this approach to weaken the hypotheses for match_program
and transf_program_partial_augment.
|
| |\ \ \
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
- 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.
|
| | | | |
| | | | |
| | | | |
| | | | | |
induction over composite types.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Use these constructor functions in C2C to rely less on the types produced
by the unverified elaborator.
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
environments. Use symbol environments for the part of semantics that deals with observable events.
|
| | | | |
| | | | |
| | | | |
| | | | | |
environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
|\| | | | |
|
| |\ \ \ \
| | | |/ /
| | |/| | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
changed the configure script to deactivated the checklink build if needed.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is achieved by declaring these functions in C2C.ml, then
re-checking their declarations in the global environment during
the Selection pass.
In passing, the "hf" parameter for SelectLong functions was removed
and replaced by fixed identifiers corresponding to the actual names
of the helper functions.
|
| |/ / /
| | | |
| | | |
| | | | |
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.
|
|\| | |
| | | |
| | | |
| | | |
| | | | |
Conflicts:
powerpc/PrintAsm.ml
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
comments.
Refactor printing of .loc debug directives in backend/PrintAnnot.ml
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Plus: simplify handling of -help and --help.
Plus: error on unrecognized "-xxx" options so that "-foo.c" is not treated
as a source file.
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Closes PR#13.
Also: give string literals type unsigned char [] or signed char []
depending on the machine configuration. (Instead of unsigned char [] before.)
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Reapply commit c3b615f875ed2cf8418453c79c4621d2dc61b0a0
which was overwritten by 2d32afc5daf16c75d1a34f2716c34ae2e1efcce4
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We now distinguish 3 modes (instead of 2 previously) for attributes: 1- strict compatibility, 2- ignore top-level attrs, 3- ignore all attrs recursively.
In strict mode, const/volatile/restrict attributes must be identical, but nonstandard attributes may vary.
Also: ignore top-level attrs when comparing function argument types, like GCC/Clang do.
Net result is fewer warnings and type-checking that is closer to GCC/Clang.
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- cparser/Machine indicates whether wchar_t is signed or not
(it is signed int in Linux and BSD, but unsigned short in Win32)
- The type of a wide string literal is "wchar_t *" if the typedef "wchar_t"
exists in the environment (e.g. after #include <stddef.h>). Only if
wchar_t is not defined do we use the default from Machine.
- Permit initialization of any integer array from a wide string literal,
not just an array of wchar_t.
|
| | | |
| | | |
| | | |
| | | | |
This is a partial fix because other cases of struct definitions within type-names are still not handled, e.g. (struct { ... } *) <expr>. However, error reporting was improved for these cases.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Based on the source of GCC 4.9.2.
Plus: reordered keywords in alphabetic order to facilitate comparison.
|
| | |/
| |/|
| | |
| | | |
The CompCert back-end already treats "asm" inserts as "volatile" in GCC's sense (performing unpredictable side-effects), so no change is required outside of the parser.
|
| | | |
|
| | |
| | |
| | |
| | | |
Assorted updates to configure and Makefile.
|