aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* | | | 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
| * Added version string to Clightgen.Bernhard Schommer2016-05-242-3/+15
| | | | | | | | | | | | Clightgen now also prints a version string. Also the CompCert version string is now similar in both modes. Bug 18768.
| * Escape all newlines.Bernhard Schommer2016-05-241-5/+5
| | | | | | | | Bug 18768.
| * Moved shared frontend code in own file.Bernhard Schommer2016-05-248-437/+356
| | | | | | | | | | | | | | 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
| * Moved some system functions into own module.Bernhard Schommer2016-05-243-68/+120
|/ | | | | | The process handling is now in its own file, like the output name generation etc. Bug 18768
* bug 18925, fix loading of symbols for thumb: :lower16: and :upper16: are ↵Michael Schmidt2016-05-131-1/+2
| | | | restricted to 15bit signed immediate offsets
* Split dependency generation.Bernhard Schommer2016-05-131-1/+2
| | | | | | 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.
* Respect COQBIN in configure script.Bernhard Schommer2016-05-131-1/+1
|
* Added option to pass linker options to gcc.Bernhard Schommer2016-05-131-0/+2
| | | | | | | | 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.
* configure: bump Menhir required version to 20160303Xavier Leroy2016-05-111-1/+1
| | | | Earlier versions of Menhir run into "string too long" errors in Coq when building on a 32-bit platform.
* fix typo 'clinker_option' in configure for OSXMichael Schmidt2016-05-101-2/+2
|
* fix typo in commentMichael Schmidt2016-05-101-1/+1
|
generated by cgit (git 2.34.1) at 2024-07-08 21:33:35 +0000