aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* | | | 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.
* | | 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
* Merge pull request #103 from AbsInt/KR_fundefsBernhard Schommer2016-06-274-64/+171
|\ | | | | Revised handling of old-style, K&R function definitions
| * Revised handling of old-style, K&R function definitionsXavier Leroy2016-06-244-64/+171
| | | | | | | | | | | | | | | | 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.
* | Merge pull request #102 from AbsInt/memory_permissionsXavier Leroy2016-06-275-9/+154
|\ \ | | | | | | Stricter control of permissions in memory injections and extensions
| * | Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-225-9/+154
| |/ | | | | | | 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.
* | Also add braces for arm. Bug 19197Bernhard Schommer2016-06-241-2/+2
| |
* | Added braces back. Bug 19197Bernhard Schommer2016-06-241-16/+16
| |
* | Moved assembler and linker into own files.Bernhard Schommer2016-06-249-122/+210
| | | | | | | | | | | | The function to call the assembler and the linker are now in own files like the preprocessor. Bug 19197
* | Deactivate options target dependend.Bernhard Schommer2016-06-242-110/+131
|/ | | | | | 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
* Update in preparation for release 2.7Xavier Leroy2016-06-222-3/+49
|
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-225-42/+73
| | | | | | | | - 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.
* Driveraux.mli: fix documentation commentXavier Leroy2016-06-221-1/+1
|
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-2111-19/+29
| | | | | | | | 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
* Pass the updated env through elab_expr.Bernhard Schommer2016-06-211-149/+166
| | | | | | Since casts, sizeof, etc. expressions can introduce new types we also need to add these to the environment and pass it through. Bug 17814
* fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert ↵Michael Schmidt2016-06-074-4/+4
| | | | can parse its own .compcert.c output, bug 18060
* Fixed warning 45 for ExportClight.ml.Bernhard Schommer2016-05-281-1/+1
|
* Merge pull request #101 from fpottier/commentBernhard Schommer2016-05-272-5/+3
|\ | | | | Fixed a comment.
| * Fixed a comment.François Pottier2016-05-272-5/+3
|/
* Merge pull request #99 from AbsInt/register-pairsXavier Leroy2016-05-2731-893/+870
|\ | | | | Introduce register pairs to describe calling conventions more precisely
| * ia32/Conventions1: remove commented-out proof attemptXavier Leroy2016-05-241-17/+0
| |
| * configure: regression on Menhir's minimal versionXavier Leroy2016-05-241-1/+1
| |
| * Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-1732-894/+888
| | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Merge pull request #100 from AbsInt/driver-splitXavier Leroy2016-05-279-509/+492
|\ \ | |/ |/| Driver refactoring
generated by cgit (git 2.34.1) at 2024-07-05 17:23:56 +0000