| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The functions expandargv and writeargv resemble the functions from
the libiberity that are used by the gnu tools. Additionaly a new
configuration is added in order to determine which kind of response
files are supported for calls to other tools.
Bug 18308
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Command now decides whether to use a responsefile or call the
external command directly.
Bug 18004
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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
|
| |\ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The exception Wrong_attr_arg raised is now catched during the
translation of the wrong _Alignas attributes.
Bug 19568.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The emulated printf in the interpreter did always return 0 instead
of the numbers of bytes printed.
Bug 19564
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Added a check for errors after the elab phases to avoid problems
in the transformations due to broken input programs.
Bug 19504
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | | |
Return with a expression that is not compatible with the given return type
of a function now causes and fatal error, to avoid problems with later
transformation passes depending on it.
|
| |_|/
|/| | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- Adjust parameters to bring the running time of each test closer to 1 second
- compression/arcode.c: array access one past
- "inline" -> "static inline"
- Remove cchecklink support
|
|\ \ \
| | | |
| | | | |
Improved handling of block-scoped 'extern' declarations
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
In a call such as "f(expr, ..., expr)", if the identifier "f" is not declared, declare it as specified in the ISO C90 standard, namely like "extern int f()" would do it. Previously, the declaration was done "on the side" and not properly recorded in the environments.
The diff is relatively large because the "enter_or_refine_ident" had to be moved up in the file.
|
|/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Currently, CompCert incorrectly handles 'extern' and function
declarations within a block. For example:
int main(void)
{
{
extern int i;
i = 0;
}
{
extern float i;
i = 10;
}
}
CompCert fails to detect the inconsistent declarations of "i" in the
two blocks, simply because the first declaration is not in scope when
the second declaration is processed.
This commit changes the elaboration of file-scope declarations,
block-scope "extern" declarations and block-scope function
declarations so that they are checked against possible earlier
declarations found in the already-elaborated top-level declarations,
instead of in the current typing environment.
Owing to the lifting of block-scoped extern and static declarations to
the top-level already performed by the elaboration pass, the
already-elaborated top-level declarations give an accurate view of the
declarations of variables with internal or external linkage already
encountered and processed, even if they are not currently in scope.
|
|\ \ \ |
|
| | | | |
|
|\| | |
| |_|/
|/| | |
|
| |\ \
| | | |
| | | | |
Fix parsing and handling of CMinor files
|
| | | | |
|
| | | | |
|
| | |/ |
|
|\ \ \
| |/ /
|/| | |
|
| | |
| | |
| | |
| | | |
__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.
|
|
|
|
| |
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.
|
| |
|