| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| | |
| | |
| | |
| | |
| | | |
The function exists_type is not really used so we can remove it.
Bug 17392.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Instead of making each filed mutuable we use a reference to a record
of type implem. Now only the default implementation and the default
debug information need to be upated to add a new function.
Bug 17392.
|
| | |
| | |
| | |
| | |
| | |
| | | |
Instead of using a tuple we now use a record with descriptive names
for the different entries.
Bug 17392
|
| | |
| | |
| | |
| | |
| | |
| | | |
Since the strip functions might be useful in other context and is
more general then the debug information.
Bug 17392.
|
| | |
| | |
| | |
| | |
| | |
| | | |
The atom to global variable debug id mapping is never used so we
do not need to insert global variables into it.
Bug 17392.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Instead of defining two functions for adding the mapping from atom
to debug id we use one function which then sets the corresponding
values.
Bug 17392.
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
If a label is printed before a list of debug annotations we can use it
for the debug annotations and don't need to add an extra label.
Bug 17392
|
| | |
| | |
| | |
| | |
| | | |
The base register for the stack allocated variables should be
r1 and not r2 under powerpc. Bug 17392
|
| | | |
|
| |\ \
| | | |
| | | | |
Take advantage of PowerPC 64-bit instructions
|
| | |\ \ |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |\ \ \
| | |/ / /
| |/| / /
| | |/ / |
Resolved conflicts in:configure powerpc/Asmexpand.ml
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence.
Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".
|
| | | | |
|
| | | | |
|
|/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example:
* in $ARCH/Machregs.v to define the register conventions for builtin functions;
* in the VST program logic from Princeton to treat thread primitives specially.
So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq.
This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
|
| | | |
|
|\ \ \
| | | |
| | | | |
Upgrade to Flocq 2.5.0.
|
| | | |
| | | |
| | | |
| | | | |
Note: this version of Flocq is compatible with both Coq 8.4 and 8.5.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Like for arm and ppc the functions for section names and start and
end addresses of compilation units are defined and the print_annot
function is moved to Asmexpandaux.ml.
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The name_of_section function no returns the correct name for the
debug sections, the prologue and epilogue directives are added and
the labels for the live ranges are introduced in the Asmexpand pass.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
taking the ident as argument.
This functions are currently not used inside the proven part but it
is nice to have them already there, when they are used by some future
pass. They also come equiped with the corresponding proofs.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The function is generalized to work for all backends and takes as
additional arguments functions for the printing of the simple
instructions and the translation function for the arguments.
|
| | | | |
|
| | | | |
|
| |_|/
|/| | |
|
| | |
| | |
| | |
| | | |
handled as a function with void parameter.
|
|\ \ \ |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | | |
information.
|
| | | |
| | | |
| | | |
| | | |
| | | | |
C11 allows a typedef redefinition if the types are the same.
We now allow this also and issue a warning and an error if the types are different.
|
|/ / / |
|
| | | |
|
| | | |
|
|\ \ \
| | | |
| | | |
| | | |
| | | | |
Conflicts:
debug/DebugInformation.ml
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
|/ / /
| | |
| | |
| | |
| | | |
Since files without function definition contain no function in the
Section_text the filenum would be empty otherwise.
|
| | | |
|
| | | |
|
|\ \ \
| | | |
| | | | |
Correction of a few bugs in the pre-parser, added comments.
|
| |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
was not parsed correctly:
typedef int a;
int f() {
for(int a; ;)
if(1);
a * x;
}
Additionnaly, I tried to add some comments in the pre-parser code,
especially for the different hacks used to solve various conflicts.
|
| | | |
|