| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|
|
|
|
| |
Valex expects Fun Section Literals and not Fun Section Literal.
Bug 18394
|
|\ |
|
| |\
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This pull request implements "approach A" to separate compilation in CompCert from the paper
Lightweight verification of separate compilation
by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis,
POPL 2016, pages 178-190
In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program.
This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.
|
| | | |
|
| | |
| | |
| | |
| | | |
Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
|
| |/
| |
| |
| |
| |
| | |
As suggested in GPR#84, use '%.15F' to force the printing of more significant digits. (The '%F' format previously used prints only 6.) This is enough to represent the FP number exactly most of the time (but not always).
Once OCaml 4.03 is out and CompCert switches to this version of OCaml, we'll be able to use hexadecimal floats for printing.
|
| |
| |
| |
| |
| |
| | |
Hide the reference used internally behind the interface and added
some functions to access the needed values.
Bug 18394
|
| |
| |
| |
| |
| |
| | |
The printer for atom constants should also use the printer
for singleton objects.
Bug 18394
|
| |
| |
| |
| |
| |
| | |
Removed unused code, factored out common functions and added an
interface file.
Bug 18394
|
| |
| |
| |
| |
| |
| | |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
| |
| |
| |
| | |
This reverts commit bac2a0854ea51217690bc6f225da62053ed7ac06.
|
| |
| |
| |
| |
| |
| | |
The ofs parameter is no longer used. Adopted the proofs and ml
code using it.
Bug 18394
|
|/
|
|
|
|
| |
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.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
compatibility, and not "unsigned int", as previously implemented.
|
|
|
|
| |
The original code produces wrong results if res and al are the same register.
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
On older version of the binutils the cfi directives are not always
supported so we only print cfi_sections if the corresponding .ini
setting is set to true.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
Instead of having a function for each instruction we now use a
generic function to print the arguments.
Bug 17544.
|
|
|
|
|
|
| |
In a first step all the print commands for the names are replaced
by a more safe variant that avoids missing \".
Bug 17328
|
|
|
|
| |
Bug 17473
|
|
|
|
| |
Bug 17473
|
|
|
|
| |
Bug 17473.
|
|
|
|
|
|
| |
Since the stacksize is casted to signed int in the alloc frame
function large stacksize lead to assembler containing overflows.
Bug 17473.
|
| |
|
|\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Conflicts:
arm/TargetPrinter.ml
backend/CMparser.mly
backend/SelectLongproof.v
backend/Selectionproof.v
cfrontend/C2C.ml
checklink/Asm_printers.ml
checklink/Check.ml
checklink/Fuzz.ml
common/AST.v
debug/DebugInformation.ml
debug/DebugInit.ml
debug/DwarfPrinter.ml
debug/DwarfTypes.mli
debug/Dwarfgen.ml
exportclight/ExportClight.ml
ia32/TargetPrinter.ml
powerpc/Asm.v
powerpc/SelectOpproof.v
powerpc/TargetPrinter.ml
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The gcc produces DW_AT_ranges for non-contiguous address ranges, like
compilation units containing functions which are placed in different
ELF-sections or lexical scopes that are split up. With this commit
CompCert also uses this DWARF v3 feature for gnu backend based targets.
In order to ensure backward compability a flag is added which avoids
this and produces debug info in DWARF v2 format.
Bug 17392.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In contrast to the dcc, the gcc uses address ranges to express
non-contiguous range of addresses. As a first step we set the
start and end addresses for the different address ranges for
the compilation unit by using the start and end addresses of
functions.
Bug 17392.
|
| |
| |
| |
| |
| |
| | |
Instead of pushing strings around use the actual section. However
the string is still used in the Hashtbl.
Bug 17392.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
Instead of using a string they now take an optional string, which
should be none if the backend is not the diab backend and the
corresponding section is the text section and Some s with s being
the custom section name else.
Bug 17392.
|