| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| |
| | |
When -c is not given, .o files are now generated in /tmp, but they are still not erased.
This commit uses an "at_exit" action to erase those temporary .o files before CompCert exits.
Using at_exit is easier to implement than explicit erasure (like we do for other temporary files), yet should not result in temporary files lingering in /tmp longer than strictly necessary, since the call to the linker is the last thing that CompCert does before exiting, hence temporary .o files are erased just after the linker returns.
|
|/
|
|
|
|
|
| |
When -c is not given, .o files are now generated in /tmp, but they are still not erased.
This commit uses an "at_exit" action to erase those temporary .o files before CompCert exits.
Using at_exit is easier to implement than explicit erasure (like we do for other temporary files), yet should not result in temporary files lingering in /tmp longer than strictly necessary, since the call to the linker is the last thing that CompCert does before exiting, hence temporary .o files are erased just after the linker returns.
|
|
|
|
|
|
|
| |
pointers (#209)
Comparisons such as "(uintptr_t) &global == 0x1234" are undefined behavior
in CompCert but their status in ISO C is unclear and they may occur in
real-world code. Make sure they are statically analyzed as Btop.
|
|
|
|
| |
So that it looks more like valid C source.
|
|
|
|
|
|
|
| |
The json export for the abstract ARM Assembler is quite similar
to it's PowerPC equivalent expect for the different instruction
arguments.
Bug 22472
|
|
|
|
|
|
|
|
| |
Instead of expanding the fixup code for incoming and outgoing
registers in the TargetPrinter we expand them in Asmexpand. This
simplifies the estimate size function and is a prerequisite for
the json export.
Bug 22472
|
|
|
|
|
| |
The common json export functionallity is moved into an own File.
Bug 22472
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
The powerpc version of print_init can be used without problems for
all backends.
Bug 22525
|
|
|
|
|
|
| |
Instead of using reset_constants use reset_literals which avoids
emptying the jumptables.
Bug 22525
|
|
|
|
|
|
| |
Instead of just storing the constants in a list, they are now
stored in a hashtable. This avoids printing of duplicates.
Bug 22525
|
|
|
|
|
| |
The new_label function is alway equal to PrintAsmaux.new_label.
Bug 22472
|
|
|
|
|
|
| |
This allows for an easier replacement of the binary address and
avoids that the user specifies his own binary addresses.
Bug 22468
|
| |
|
| |
|
|
|
|
|
|
| |
The file and line information are now stored as comment string at
the start of each annotation.
Bug 22462
|
|
|
|
|
|
| |
configure: accept Coq 8.7.0 and 8.6.1.
(Coq 8.6 became incompatible with commit b4f59c4.)
Changelog: updated.
|
|\
| |
| |
| | |
Ensure FunInd or Recdef is imported if functional induction is used.
This is necessary for Coq 8.7.0.
|
| |
| |
| |
| |
| |
| | |
Coq 8.7 does not load FunInd in prelude anymore, so this is necessary.
Recdef exports FunInd, so if Recdef is imported, importing FunInd
is not required.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The ais annotations can be inserted via the new ais variants of
the builtin annotation. They mainly differe in that they have an
address format specifier '%addr' which will be replaced by the
adress in the binary.
The implementation simply prints a label for the builtin call
alongside a the text of the annotation as comment and inserts the
annotation together as acii string in a separate section
'ais_annotations' and replaces the usages of the address format
specifiers by the address of the label of the builtin call.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Check recursively for const for modifiable lvalues
According to 6.3.2.1 a modifiable lvalue is an lvalue that does
have a const-qualified type, and if it is a union or structure it
does not have any member, including any member of all contained
strutures or union, with a const-qualified type.
The new check for modifiable lvalue additionally checks this now
instead of only testing for toplevel const.
Bug 22420
|
| |
| |
| |
| |
| |
| | |
If CompCert is called to compile and link object files should not
be created.
Bug 22399
|
| | |
|
| | |
|
| | |
|
|\ \ |
|
| | |
| | |
| | |
| | | |
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
|
| | |
| | |
| | |
| | |
| | |
| | | |
This option allows it to dump a list of all used mnemonics into
a file.
Bug 22239
|
|/ /
| |
| |
| | |
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
|
| |
| |
| |
| |
| |
| |
| | |
In order to ensure that no new instruction is added without adding
it to the Json export we enforce warning 4 for the instruction
printer and removed all default pattern matchings.
Bug 22239
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
These are conditionals where the "ifso" and the "ifnot" successors are the same. By eliminating them here and not later, we can also eliminate the instructions that compute the arguments to the condition, if any.
There is another, later point where these trivial conditional instructions are eliminated: in the Tunneling phase. The elimination done in Tunneling is more powerful in that it works not just for conditionals whose two successors are the same, but also for conditionals whose two successors lead to the same point after a series of nops. The elimination done in Deadcode is more powerful in that it eliminates the instructions that compute the arguments to the condition. Hence it is worth having both eliminations.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* Clarify that ARMv6 is in fact ARMv6T2
The ARMv6 comes in two flavors depending on the version of the Thumb
instruction set supported: ARMv6 for the original Thumb, ARMv6T2 for Thumb2.
CompCert only supports Thumb2, so its ARMv6 architecture should really be
called ARMv6T2. This makes a difference: the GNU assembler rejects most of
the instructions CompCert generates for ARMv6 with "-mthumb" if the
architecture is specified as ".arch armv6" as opposed to ".arch armv6t2".
This patch fixes the architecture specification in the target printer and
the internal name of the architecture. It does not change the configure
script's flags to avoid breaking changes.
* Always use ARM movw/movt to load large immediates
These move-immediate instructions used to be only emitted in Thumb mode, not
in ARM mode. As far as I understand ARM's documentation, these instructions
are available in *both* modes in ARMv6T2 and above. This should cover all of
CompCert's ARM targets.
Tested for ARMv6 and ARMv7, both with and without Thumb2. The behavior is
now identical to Clang, and the GNU assembler accepts these instructions in
all configurations.
* Separate ARMv6 and ARMv6T2; no movw/movt on ARMv6
- define separate architecture models for ARMv6 and ARMv6T2
- introduce `Archi.move_imm` parameter on ARM to identify models with
`movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM
and Thumb mode)
* Fixes for support for architectures with Thumb2
- rename relevant parameter to `Archi.thumb2_support`
- on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb)
- allow generation of `sbfx` in ARM mode if Thumb2 is supported
|
|\ \
| | |
| | | |
Strength reduction patterns for ARM mla instruction.
|
|/ / |
|
| |
| |
| |
| | |
Some alignments were wrong. Follow-up to [4d099ef].
|
| |
| |
| |
| | |
Even with __GNUC__ undefined, the standard header files contain bizarre __attribute__ declarations that CompCert fails to parse.
|
| |
| |
| |
| | |
It got lost during the addition of the x86-64 port in release 3.0.
|
| |
| |
| |
| |
| | |
Not very useful in practice (make clean is generally done before make all)
and problematic under Cygwin where ../../ccomp is really ../../ccomp.exe
|
| |
| |
| |
| |
| | |
The latter, in conjunction with some values of the umask, gives weird messages
"new permissions are ... not ...".
|
| |
| |
| |
| |
| | |
Qualify imports in clightgen-produced files and in Clightdefs so that they can be used with coq -Q /path/to/compcert compcert.
Remove 'Require Export' from Clightdefs as suggested in issue #199.
|
| |
| |
| |
| | |
Otherwise the interpreter uses the system's header files instead of CompCert's. This can lead to mismatches e.g. on the definition of wchar_t.
|