| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| ... | |
| |
|
|
|
|
|
| |
Nonstatic inline functions can be expanded in several compilation units.
The static variables in question may differ between different expansions.
This is a manual merge and adaptation of pull request #P95 by @bschommer.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Before, we would pass just the `ctx_vararg` component of the context
to `elab_expr` as a Boolean argument.
For future extensions, we will need to pass more of the context to
`elab_expr`, so why not pass the whole context?
This is what this commit does. The `stmt_context` type is renamed
`elab_context` and its definition is moved earlier. The `ctx`
argument is passed as is from `elab_stmt` to `elab_expr`.
|
| |
|
|
|
|
|
| |
The current check for redefinition is too strict, ruling out e.g.
```
typedef int t;
void f(void) { typedef char t; }
```
|
| |
|
|
|
|
| |
These are extensions w.r.t. C99, not incompatible changes.
Nothing bad can happen if those C11 features are used, except making
the code incompatible with C99.
|
| |
|
|
| |
Consistently with _Noreturn, anonymous structs, etc.
|
| |
|
|
|
| |
It's not really necessary, and under Windows it's really ../../clightgen.exe,
which confuses make.
|
| |
|
|
|
|
|
|
|
|
| |
The semantics of external function calls in LTL, Linear, Mach and Asm
now consider that all caller-save registers are set to Vundef by the call.
This models that fact that the external function can modify those registers
arbitrarily.
Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes
accordingly.
|
| |
|
|
|
| |
coq2html is now a standalone project (https://github.com/xavierleroy/coq2html)
packaged as coq-coq2html in OPAM-Coq.
|
| |
|
|
| |
Also: add "parallel" entry to test/Makefile for parallel execution of tests.
|
| |
|
| |
This is useful for the VST project and can be useful for others.
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
.vo files are installed if configure options
-install-coqdev or -clightgen or -coqdevdir are given.
Installation directory is $(PREFIX)/lib/compcert/coq by default and
can be changed by configure option -coqdevdir.
Closes: #227
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Simplify the theorems about preservation of specifications (section 2)
There were three theorems, transf_c_program_preserves_spec, _safety_spec, and _liveness_spec) with the first being needlessly general and the last being hard to understand. Plus, the "liveness" and "safety" terminology wasn't very good.
Replaced by two theorems:
- transf_c_program_preserves_spec, which is the theorem previously named _safety_spec and talks about specifications that exclude going-wrong behaviors;
- transf_c_program_preserves_initial_trace, which is an instance of the theorem previously named _liveness_spec, and now talks about a single initial trace of interest rather than a set of such traces.
Added named definitions for properties of interest.
Added more explanations.
* Added theorems that talk about separate compilation (section 3)
These are the theorems from section 1 and 2 but reformulated in terms of multiple C source compilation units being separately compiled to Asm units then linked together.
|
| |
|
|
|
|
| |
As the standard says (and is already implemented) an _Alignas(0)
does not change the alignment at all. The same holds for the gcc
attribute.
Bug 23387
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Allow strings literals as lvalues.
Strings and WStrings literals are lvalues, thus it is allowed to take their
addresses.
Bug 23356.
* String literals have types "array of (wide) char", not "pointer to (wide) char"
The pointer types were a leftover from the early, CIL-based C frontend.
* Remove special case for sizeof("string literal") during elaboration
No longer needed now that literals have array types.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is a follow-up to the introduction of the Storage_auto storage class
in commit 760e422.
For functions declared within a block, we used to set their storage class
to "extern":
{ {
int f(void); ---> extern int f(void);
} }
This helped enter_or_refine_ident understand that those declarations
have linkage.
Now that we have Storage_auto, this commit teaches enter_or_refine_ident
that local declarations have no linkage if auto or static, and have
linkage if extern or default.
Then, there is no need to change storage class to extern for
locally-declared functions.
In turn, this improves the "extern-after-definition" warning recently
introduced, avoiding a bizarre warning in the following case:
int foo(void){return 0;}
int main(void){
int foo(void);
return foo();
}
|
| |
|
|
|
|
|
|
|
| |
Warning for change of storage class after the definition of a function
from default storage class to extern storage class. This only plays a
role if the function is also declared inline, since for inline functions
with default storage class no code is generated, but for inline functions
with extern storage class code should be generated.
Bug 23512
|
| |
|
|
| |
This is what ISO C99 says, even though C++ and some C compilers accept it.
|
| |
|
|
|
|
|
| |
The definition is similar to that of gcc, however since we don't support
long doubles out of the box and long doubles are doubles in compat mode
we can directly define max_align_t to be long long.
Bug 23380
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
In rare cases we can end up querying the attributes of a struct, union
or enum type that is no longer in scope and therefore not bound
in the current environment.
Instead of raising an Env.Error_ exception in this case,
this commit treats such structs / unions / enums as having no
attributes attached to their definitions: only the attributes
carried by the type expression are returned.
One example where this occurs is the following, made possible by
the previous commit ("Revised elaboration of function definitions"):
int f(struct s { int a; } * p) { return p-> a; }
int g(void) { return f(NULL); }
"struct s" is scoped within the definition of f. When we get to
checking the call to f from g, checking that the NULL argument
is compatible with the "struct s *" parameters, we're outside
the scope of "struct s" and its definition is not found in the
current environment.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Change elab_type_declarator and elab_fundef_name so that the latter
returns two environments: the first one takes into account
struct/union definitions from the function return type,
while the second one also contains bindings for function
parameters and struct/union definitions from the function parameter list.
To this end the "kr_ok" bool argument of elab_type_declarator is
repurposed and renamed "fundef". It controls not just whether
K&R function declarators are supported, but also which bindings
the returned environment contains.
Change elab_fundef to adapt to the changes in elab_fundef_name
and to maintain two environments:
- the global environment, enriched with struct/union definitions from
the function return type, and with the function binding itself;
- the local environment, used for elaborating the body of the
function, which also contains bindings for function parameters
and struct/union definitions from the function parameter list.
Change elab_funbody so that it does not open a new scope for elaborating
the body, even though the body is represented as a block in the AST.
The standard says that the function body is processed in the same
scope where function parameters are declared, so that the following
is illegal:
int f(int x) { double x; ... }
Introduce a variant enter_or_refine_function of enter_or_refine_ident
where the fresh identifier to use (if no earlier declaration is found)
is created in advance in an earlier scope. This helps implement the
proper scoping of function names.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Partial revert of commit ec95665e087d39e29ece455b90e7d5918dc88cee.
That commit introduced a "keep_ty" parameter to type elaboration
functions telling them to keep struct/union definitions occurring
in function parameter lists and lift them to the outer environment.
By setting keep_ty to true, the following could typecheck:
int f(struct s { int a; } x) { return x.a; }
However, "struct s" would escape the scope of the function definition
and leak to the top-level environment, which is not correct.
In subsequent commits we'll address the issues above differently,
in a way that does not need the "keep_ty = true" behavior.
|
| |
|
|
|
|
| |
The new warning is raise for function declaration after a function
definition that introduce new attributes, which are ignored.
Bug 23385
|
| |
|
|
|
|
| |
The C standards says that either both types must be pointer to
complete compatible or incomplete compatible types.
Bug 23631
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Check for static and extern variables in for
The declaration inside of a for statement is not allowed to have
static or extern storage duration.
Bug 23330
* Also check that the declared variables don't have function types.
* Also checks that no typedefs occur in 'for' declarations.
* Simplify the `elab_declarations` function. It's used only to elaborate the whole program, and the resulting declarations and environment are ignored. So, replace `elab_declarations` by a simpler iteration over the program in `elab_program`.
|
| |
|
|
|
| |
Empty declarations in K&R function parameters are not allowed
by the C standard.
Bug 23375
|
| |
|
|
| |
The type of array elements must be complete.
Bug 23341
|
| | |
|
| |
|
|
|
|
| |
New builtin for 64-bit load/store with byte reversal and 64-bit
mul-high.
Bug 23541
|
| | |
|
| | |
|
| |
|
|
| |
Report an error in this case.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The Elab pass checks that the argument of 'case' is a compile-time constant
expression. This commit records the value of this expression in the
C.Scase AST generated by Elab, so that it can be used for further
diagnostics, i.e. checking (in Elab) for duplicate cases.
Note that C2C ignores the recorded value and recomputes the value of
the expression using Ceval.integer_expr. This is intentional:
Ceval.integer_expr is more trustworthy, as it is formally verified
against the CompCert C semantics.
|
| |
|
|
| |
Report an error in this case.
|
| |
|
|
| |
Typedefs should have a name and also should not contain _Noreturn.
Bug 23381
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit checks *during elaboration* that initializers for global
variables or local static variables are compile-time constants.
Before this commit, some non-constant initializers were detected
later in the C2C pass, but others were eliminated by the Cleanup
pass before being checked, and yet others could cause the Rename pass
to abort.
To determine which variables are constant l-values, we leverage
the recent addition of the Storage_auto storage class and base
the determination on the storage class of the identifier:
'auto' or 'register' is not constant, the others are constant.
|
| |
|
|
|
| |
Enum tags, struct tags and union tags share a common namespace, thus having
an enum with the same tag as a struct or union is not allowed.
Bug 23548
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For anonymous bit-fields in structs, carrier fields may
be introduced which are not initialized since no default
initializer are generated earlier. This cause the translation in
C2C to throw an error since too few initializers are available.
Example:
struct s2 {
int : 10;
int a;
int : 10;
char b;
int : 10;
short c;
int : 10;
} s2 = { 42, 'a', 43 };
To work around this issue we need to generate a default inializer
for every new member that does not have a translated member.
Based on P#80, with more efficient algorithms.
Bug 23362
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
For each struct or union that contains bitfields,
we record the list of members after transformation,
where bit fields were replaced by carrier fields.
Right now we do not use this information but it will come handy
to fix a problem with struct initialization.
Also: clear the global hash tables on entry so that multiple runs
of the Bitfields transformation don't interfere with each other.
There probably was no interference before because identifiers are unique
enough, but this is fragile.
|
| |
|
|
|
|
|
|
|
|
|
| |
Bit fields in unions were initialized like normal fields,
causing mismatch on the name of the field.
Also: added function Bitfields.carrier_field and refactored.
Patch by Bernhard Schommer.
Bug 23362
|
