| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
| |
Since gnu make and other tools under windows seem to have a limit
of around 8000 bytes per command line the arguments should be
passed via responsefiles instead.
Bug 18308
|
| |
|
|
|
|
|
|
| |
The arguments are written in the responsefile separated by whitespace.
If the argument itself contains a whitespace it is quoted.
Bug 18308
|
|\ |
|
| |\ |
|
| | |
| | |
| | |
| | | |
__builtin_ctzll for ARM
|
| | |
| | |
| | |
| | | |
__builtin_ctzll for PowerPC
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Here are two examples that cause an internal error in Asmexpand.ml:
volatile long long x; void f(unsigned int i) { x = i; }
unsigned g(unsigned i) { return __builtin_clzll(i); }
The argument "i" to builtin volatile store or __builtin_clzll is turned into a BA_splitlong(BA_int 0, BA <variable i>), which Asmexpand.ml doesn't know how to handle.
The fix (in AST.builtin_arg_ok) is to prevent this 'optimization' for all builtins except those of the "OK_all" kind, i.e. __builtin_annot.
Regression tests were added and tested on IA32. Need to retest on ARM and PowerPC.
|
| |/
| |
| |
| |
| | |
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
|
|/
|
|
|
|
|
|
| |
Commandline can now be passed in a file specifed with @file on the
Commandline. The quoting convention is similar to the one used by
gcc, etc. Options are separated by whitespaces and options with
whitespaecs need to be quoted.
Bug 18303
|
|
|
|
| |
There was no good reason why Determinism.v was the only file in common/ that was not dual-licensed (GPL + noncommercial). Plus, it simplifies the wording of the LICENSE file.
|
| |
|
|\ |
|
| | |
|
|/ |
|
|
|
|
|
|
| |
The configuration advanced debug is removed and now full debug
information is also generated for ia32 and arm.
Bug 17609
|
|
|
|
| |
conversion
|
|\
| |
| | |
Revised handling of old-style, K&R function definitions
|
| |
| |
| |
| |
| |
| |
| |
| | |
This commits handles the case where the argument is passed with a type different from the actual type of the argument, as in
float f (x) float x; { return x; }
"x" is passed with type "double", and must be converted to "float" at the beginning of the function.
|
|\ \
| | |
| | | |
Stricter control of permissions in memory injections and extensions
|
| |/
| |
| |
| | |
As suggested by Lennart Beringer, this commits strengthens memory injections and extensions so as to guarantee that the permissions of existing memory locations are not increased by the injection/extension. The only increase of permissions permitted is empty locations in the source memory state of the injection/extension being mapped to nonempty locations.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
The function to call the assembler and the linker are now in own
files like the preprocessor.
Bug 19197
|
|/
|
|
|
|
| |
Options only available for gnu systems or arm target arch are no
longer displayed in the help and cannot be selected any longer.
Bug 19197
|
| |
|
|
|
|
|
|
|
|
| |
- Values: "rol" and "ror" are defined even if their second argument
is not in the [0,31] range (for consistency with "rolm" and because
the semantics is definitely well defined in this case).
- NeedDomain: more precise analysis of "rol" and "rolm", could
benefit the PowerPC port.
|
| |
|
|
|
|
|
|
|
|
| |
Most of the code can be String.uppercase usages can either be
replaced by a more specialized version of coqstring_of_camlstring
(which is also slightly more effecient) or by specialized checks
that reject wrong code earlier.
Bug 19187
|
|
|
|
|
|
| |
Since casts, sizeof, etc. expressions can introduce new types
we also need to add these to the environment and pass it through.
Bug 17814
|
|
|
|
| |
can parse its own .compcert.c output, bug 18060
|
| |
|
|\
| |
| | |
Fixed a comment.
|
|/ |
|
|\
| |
| | |
Introduce register pairs to describe calling conventions more precisely
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations.
In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves. We will need to change this in the future to support 64-bit processors. The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting. Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves.
Summary of changes:
- AST: introduce the type "rpair A" of register pairs
- Conventions1, Conventions: use it when describing calling conventions
- LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls
- Events: suppress external_call', no longer useful
- All passes from Allocation to Asmgen: adapt accordingly.
|
|\ \
| |/
|/| |
Driver refactoring
|
| |
| |
| |
| |
| |
| | |
Clightgen now also prints a version string. Also the CompCert version
string is now similar in both modes.
Bug 18768.
|
| |
| |
| |
| | |
Bug 18768.
|
| |
| |
| |
| |
| |
| |
| | |
Clightgen and CompCert share the code for preprocessing as well as
parsing C files. The code as well as command line switches is moved
in the new module Frontend.
Bug 18768
|
|/
|
|
|
|
| |
The process handling is now in its own file, like the output name
generation etc.
Bug 18768
|
|
|
|
| |
restricted to 15bit signed immediate offsets
|
|
|
|
|
|
| |
GNU make under windows seems to have a restriction to 8192 characters
for commandline arguments. The dependency generation of compcert is
too large. Thus we split it into two steps.
|
| |
|
|
|
|
|
|
|
|
| |
Some gcc options have influence on the linking (especially -march,
etc.). The new -WUl options allows it to pass the options to the
gcc called for linking instead of passing them to the linker
directly.
Bug 18949.
|
|
|
|
| |
Earlier versions of Menhir run into "string too long" errors in Coq when building on a 32-bit platform.
|
| |
|
| |
|