| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
| |
This is a follow-up to commit 6e1a5ce.
Another `open! Floats` is needed.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
OCaml 4.07 introduces a Float submodule of the Stdlib
opened-by-default compilation unit. CompCert's Float compilation unit
also has a Float submodule. This triggers warning 44 when Floats is
opened. The workaround is just to silence the warning with `open! Floats`.
Closes: #241
|
| |
|
| |
|
|
|
| |
The `-iquote` option was passed to the GNU preprocessor as `-iquore`
|
|
|
|
|
| |
Information about the run of clightgen is added to the generated .v file as definitions within a sub-module named Info.
Closes: #226.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Outgoing stack slots are set to Vundef on return from a function call,
modeling the fact that the callee could write into those stack slots.
(CompCert-generated code does not do this, but code generated by other
compilers sometimes does.)
* Adapt Stackingproof to this new semantics. This requires tighter
reasoning on how Linear's locsets are related at call points and
at return points.
* Most of this reasoning was moved from Stackingproof to Lineartyping,
because it can be expressed purely in terms of the Linear semantics,
and tracked through the wt_state predicate.
* Factor out and into Conventions.v: the notion of callee-save
locations, the "agree_callee_save" predicate, and useful lemmas on
Locmap.setpair. Now the same "agree_callee_save" predicate is used
in Allocproof and in Stackingproof.
|
| |
|
| |
|
|
|
|
| |
The `_Alignas(expr)` construct is not C11, only `_Alignas(type)` is.
|
| |
|
|
|
|
| |
Inspired by and adapted from pull request #235 by Benoît Viguier.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
| |
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
|