aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* For the release, turn off -warn-errorv2.7Xavier Leroy2016-06-301-1/+1
| | | | Release builds should not have -warn-error so that they are resilient to addition of new warnings in newer versions of OCaml.
* 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
|
* fix typo 'clinker_option' in configure for OSXMichael Schmidt2016-05-101-6/+10
|
* ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of ↵Xavier Leroy2016-05-072-111/+141
| | | | | | | | memory blocks Trees are slightly more efficient than Maps, and avoid maintaining the invariant on the default value. lib/Maps: add a generic construction of a (partial) Tree module from an indexed type; use it to define ZTrees (trees indexed by Z integers).
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit ↵Xavier Leroy2016-04-2725-2781/+2973
| | | | | | | | | | | | | | | | | | | architectures The original Stacking pass and its proof hard-wire assumptions about the processor and the register allocation, namely that integer registers are 32 bit wide and that all stack slots have natural alignment 4, which precludes having stack slots of type Tlong. Those assumptions become false if the target processor has 64-bit integer registers. This commit makes minimal adjustments to the Stacking pass so as to lift these assumptions: - Stack slots of type Tlong (or more generally of natural alignment 8) are supported. For slots produced by register allocation, the alignment is validated a posteriori in Lineartyping. For slots produced by the calling conventions, alignment is proved as part of the "loc_argument_acceptable" property in Conventions1. - The code generated by Stacking to save and restore used callee-save registers no longer assumes 32-bit integer registers. Actually, it supports any combination of sizes for registers. - To support the new save/restore code, Bounds was changed to record the set of all callee-save registers used, rather than just the max index of callee-save registers used. On CompCert's current 32-bit target architectures, the new Stacking pass should generate pretty much the same code as the old one, modulo minor differences in the layout of the stack frame. (E.g. padding could be introduced at different places.) The bulk of this big commit is related to the proof of the Stacking phase. The old proof strategy was painful and not obviously adaptable to the new Stacking phase, so I rewrote Stackingproof entirely, using an approach inspired by separation logic. The new library common/Separation.v defines assertions about memory states that can be composed using a separating conjunction, just like pre- and post-conditions in separation logic. Those assertions are used in Stackingproof to describe the contents of the stack frames during the execution of the generated Mach code, and relate them with the Linear location maps. As a further simplification, the callee-save/caller-save distinction is now defined in Conventions1 by a function is_callee_save: mreg -> bool, instead of lists of registers of either kind as before. This eliminates many boring classification lemmas from Conventions1. LTL and Lineartyping were adapted accordingly. Finally, this commit introduces a new library called Decidableplus to prove some propositions by reflection as Boolean computations. It is used to further simplify the proofs in Conventions1.
* bug 18004, fix file extensions for dparse optionMichael Schmidt2016-04-252-2/+2
|
* Enabled Werror via command line option.Bernhard Schommer2016-04-251-0/+1
| | | | | | The new command line option -Werror activates the treatment of warnings as errors. Bug 18004
* */TargetPrinter.ml: wrong comment attached to Init_float32 constantsXavier Leroy2016-04-093-3/+3
| | | | For informative purposes, the FP value of Init_float* constants is printed as a comment in the generated asm file. However, for Init_float32, it was wrongly printed as a double-precision FP instead of a single-precision FP.
* Also enable warnings for doc generator.Bernhard Schommer2016-04-062-8/+8
|
* Added iso646 header for alternate spellings.Bernhard Schommer2016-04-061-0/+49
| | | | | | | The iso646 header defines some macros that expand to common operators. Both clang and gcc ship with them and they are required by the standard. Bug 18645.
* Check for type compatibility when initializing TInt arrays with wide strings ↵Michael Schmidt2016-04-061-1/+1
| | | | (§6.7.8), bug 18000
generated by cgit (git 2.34.1) at 2024-06-02 23:36:22 +0000