aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* fix merge conflictsMichael Schmidt2016-08-1717-15/+235
|\
| * Exit earlier on empty union.Bernhard Schommer2016-08-171-1/+5
| | | | | | | | | | | | | | Instead of a warning for an empty union CompCert reports an error and exits. This avoids problems during the generation of initializers for these. Bug 19565.
| * Merge pull request #107 from AbsInt/add-fileXavier Leroy2016-08-1712-10/+219
| |\ | | | | | | Add support for response files
| | * Moved quoting functions in ResponsefileBernhard Schommer2016-08-165-36/+44
| | | | | | | | | | | | | | | | | | Also corrected some typos and corrected exception handling for expandargv. Bug 18308
| | * Added missing begin end around quoting. Bug 18308.Bernhard Schommer2016-08-101-2/+2
| | |
| | * Corrected diab quoting. Bug 18308Bernhard Schommer2016-07-211-8/+11
| | |
| | * Added support for quoting for diab backend.Bernhard Schommer2016-07-214-2/+21
| | | | | | | | | | | | | | | | | | The diab data compiler has different quoting conventions compared to the gnu tools. Bug 18308.
| | * Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-2011-145/+140
| | | | | | | | | | | | | | | | | | | | | | | | 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
| | * Merged responfile function into command.Bernhard Schommer2016-07-195-49/+33
| | | | | | | | | | | | | | | | | | Command now decides whether to use a responsefile or call the external command directly. Bug 18004
| | * Added heuristic for passing arg via responsefiles.Bernhard Schommer2016-07-127-31/+51
| | | | | | | | | | | | | | | | | | | | | 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
| | * Really added the function. Bug 18308Bernhard Schommer2016-07-112-3/+19
| | |
| | * Added function to write responsefiles.Bernhard Schommer2016-07-111-0/+24
| | | | | | | | | | | | | | | | | | The arguments are written in the responsefile separated by whitespace. If the argument itself contains a whitespace it is quoted. Bug 18308
| | * Merge branch 'master' into add-fileBernhard Schommer2016-07-1156-365/+626
| | |\
| | * | Added responsefile support for commandline.Bernhard Schommer2016-07-083-1/+141
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| * | | Catch attribute excpetion in _Alignas elabBernhard Schommer2016-08-171-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | The exception Wrong_attr_arg raised is now catched during the translation of the wrong _Alignas attributes. Bug 19568.
| * | | Fixed issue with emulation of printfBernhard Schommer2016-08-171-2/+4
| | | | | | | | | | | | | | | | | | | | | | | | The emulated printf in the interpreter did always return 0 instead of the numbers of bytes printed. Bug 19564
| * | | Fixed typo. Bug 19504Bernhard Schommer2016-08-081-1/+1
| | | |
| * | | Added error check before transformations.Bernhard Schommer2016-08-084-3/+7
| | | | | | | | | | | | | | | | | | | | | | | | Added a check for errors after the elab phases to avoid problems in the transformations due to broken input programs. Bug 19504
| * | | Exit earlier on wrong return types.Bernhard Schommer2016-08-071-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | update help text in configure scriptMichael Schmidt2016-08-081-13/+14
| | | |
* | | | port fix for configure from m-schmidt/EndiannessPlaygroundMichael Schmidt2016-08-071-0/+5
| | | |
* | | | Changed configure target for arm big endian.Bernhard Schommer2016-08-051-27/+12
| | | | | | | | | | | | | | | | | | | | | | | | Instead of an addition -little or -big at the end the configure script now accepts armeb* for the big endian arm targets. Bug 19418
* | | | Implement support for big endian arm targets.Bernhard Schommer2016-08-0537-472/+667
|/ / / | | | | | | | | | | | | | | | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* | | Added -dall which enables all tracing.Bernhard Schommer2016-08-021-0/+12
| | |
* | | Use asprintf instead of printing to a buffer.Bernhard Schommer2016-07-261-5/+2
| | |
* | | test/raytracer: use our own strdup(), since this is not a standard functionXavier Leroy2016-07-241-1/+9
| | |
* | | Updates to the local test suiteXavier Leroy2016-07-2424-187/+133
| | | | | | | | | | | | | | | | | | | | | - 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
* | | Merge pull request #109 from AbsInt/extern-scopesBernhard Schommer2016-07-221-54/+104
|\ \ \ | | | | | | | | Improved handling of block-scoped 'extern' declarations
| * | | Nicer error message for redefinitions with incompatible typeXavier Leroy2016-07-221-3/+4
| | | |
| * | | Improved handling of C90 calls to undeclared functionsXavier Leroy2016-07-211-73/+75
| | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | Revised handling of block-scoped extern declarationsXavier Leroy2016-07-211-46/+93
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2016-07-181-2/+8
|\ \ \
| * | | Update Changelog for release 2.7.1v2.7.1Xavier Leroy2016-07-181-2/+8
| | | |
* | | | Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2016-07-113-21/+32
|\| | | | |_|/ |/| |
| * | Merge pull request #105 from m-schmidt/masterXavier Leroy2016-07-113-21/+32
| |\ \ | | | | | | | | Fix parsing and handling of CMinor files
| | * | add 'runtime' token to lexerMichael Schmidt2016-07-011-0/+1
| | | |
| | * | extend cminor parser to accept "extern runtime" declarationsMichael Schmidt2016-07-011-0/+4
| | | |
| | * | add missing asmexpand step to cminor handler in driverMichael Schmidt2016-07-011-21/+27
| | |/
* | | Merge branch 'master' of /common/repositories/git/tools/compcertBernhard Schommer2016-07-094-0/+68
|\ \ \ | |/ / |/| |
| * | bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and ↵Michael Schmidt2016-07-082-0/+36
| | | | | | | | | | | | __builtin_ctzll for ARM
| * | bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and ↵Michael Schmidt2016-07-082-0/+32
| |/ | | | | | | __builtin_ctzll for PowerPC
* | Unwanted partial constant propagation in 64-bit integer arguments to builtinsXavier Leroy2016-07-088-1/+18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Port to Coq 8.5pl2Xavier Leroy2016-07-0844-364/+540
|/ | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* common/Determinism.v: dual-license with GPLXavier Leroy2016-06-302-14/+4
| | | | 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.
* Changelog update: mention -g for ARM and IA32Xavier Leroy2016-06-301-0/+4
|
* Merge branch 'master' of ssh://github.com/AbsInt/CompCertXavier Leroy2016-06-301-0/+1
|\
| * Added back ;;Bernhard Schommer2016-06-281-0/+1
| |
* | LICENSE: update the list of files that are dual-licensed under the GPLXavier Leroy2016-06-281-2/+10
|/
* Activate advanced debug information for arm, ia32.Bernhard Schommer2016-06-287-20/+5
| | | | | | The configuration advanced debug is removed and now full debug information is also generated for ia32 and arm. Bug 17609
* bug 19234, inherit varargs flag from previous function definitions for KR ↵Michael Schmidt2016-06-281-4/+19
| | | | conversion
generated by cgit (git 2.34.1) at 2024-07-04 10:27:51 +0000