aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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
* Check for type compatibility when initializing TInt arrays with wide strings ↵Michael Schmidt2016-04-061-1/+1
| | | | (§6.7.8), bug 18000
* Revert initialization check, bug 18000Michael Schmidt2016-04-051-8/+0
|
* Match type size with size of wchar_t when initializing TInt arrays with wide ↵Michael Schmidt2016-04-051-1/+1
| | | | strings, bug 18000
* Catch initialization of arrays with single expressions, bug 18000Michael Schmidt2016-04-051-2/+2
|
* Catch initialization of arrays with single expressions, bug 18000Michael Schmidt2016-04-051-0/+8
|
* Merge pull request #95 from AbsInt/noreturnBernhard Schommer2016-04-0411-26/+150
|\ | | | | Added the _Noreturn keyword.
| * Added the _Noreturn keyword.Bernhard Schommer2016-03-2311-26/+150
| | | | | | | | | | | | | | | | CompCert now recognizes the C11 _Noreturn function specifier and emits a simple warning for functions declared _Noreturn containing a return statement. Also the stdnoreturn header and additionally the stdalign header are added. Bug 18541
* | Compatibility with newer ocaml versions. Bug 18313.Bernhard Schommer2016-03-314-6/+10
|/
* Merge pull request #94 from jhjourdan/parentherized_funBernhard Schommer2016-03-232-0/+18
|\ | | | | Fix a bug in the pre-parser.
| * Fix a bug in the pre-parser.Jacques-Henri Jourdan2016-03-232-0/+18
|/
* Also refactor clightgen to work with new warnings. Bug 18394Bernhard Schommer2016-03-231-6/+6
|
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2016-03-211-1/+1
|\
| * configure: fix test for CFI directivesXavier Leroy2016-03-211-1/+1
| | | | | | | | The test was failing as a consequence of the split casm -> casm / casm_options.
* | Reverted name for entry back to the old one.Bernhard Schommer2016-03-211-1/+1
|/ | | | | Valex expects Fun Section Literals and not Fun Section Literal. Bug 18394
* Merge pull request #92 from AbsInt/cleanupXavier Leroy2016-03-2168-647/+624
|\ | | | | This PR activates more OCaml warnings and turns all warnings into errors. Also some unused functions, variables and types are removed.
| * Merge branch 'master' into cleanupBernhard Schommer2016-03-2188-5401/+6282
| |\
| * | Revert "Add the -Xalign-value options for diab."Bernhard Schommer2016-03-181-1/+0
| | | | | | | | | | | | This reverts commit 771d8576fbae8bd48f6bc80c74722ce1c7cc5259.
| * | Add the -Xalign-value options for diab.Bernhard Schommer2016-03-181-0/+1
| | | | | | | | | | | | | | | | | | The default of the diab compiler is to interpret the alignment as power of two. Bug 18490.
| * | Added an interface file for DebugInformation.Bernhard Schommer2016-03-185-43/+183
| | | | | | | | | | | | | | | | | | The interface hides the implementation details, like the huge number of Hashtbls from the rest of the implementatio. Bug 18394
| * | Added interface for the Asmexpansion.Bernhard Schommer2016-03-165-10/+55
| | | | | | | | | | | | | | | | | | Hide the reference used internally behind the interface and added some functions to access the needed values. Bug 18394
| * | Change atom printer to use the common function.Bernhard Schommer2016-03-161-1/+1
| | | | | | | | | | | | | | | | | | The printer for atom constants should also use the printer for singleton objects. Bug 18394
| * | Cleanup of AsmToJSON.Bernhard Schommer2016-03-166-128/+140
| | | | | | | | | | | | | | | | | | Removed unused code, factored out common functions and added an interface file. Bug 18394
| * | Removed not needed env.Bernhard Schommer2016-03-151-5/+5
| | | | | | | | | | | | | | | | | | The functions for naming string and wstring literals no longer need an env. Bug 18394
| * | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-1547-447/+449
| | | | | | | | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
| * | Added back invariant checks for IRC.Bernhard Schommer2016-03-151-0/+36
| | | | | | | | | | | | | | | | | | Since the invariant checks are not currently used and they are not exported they are renamed to include a _ to avoid warning. Bug 18394
| * | Revert "Removed unused parameter from is_small/rel_data."Bernhard Schommer2016-03-156-26/+28
| | | | | | | | | | | | This reverts commit bac2a0854ea51217690bc6f225da62053ed7ac06.
| * | Removed unused parameter from is_small/rel_data.Bernhard Schommer2016-03-116-28/+26
| | | | | | | | | | | | | | | | | | The ofs parameter is no longer used. Adopted the proofs and ml code using it. Bug 18394
| * | Cleanup of Clightgen code.Bernhard Schommer2016-03-102-45/+41
| | | | | | | | | | | | | | | Removed unused code and code generating warnings. Bug 18394
| * | Clean up of ia32 target dependend code.Bernhard Schommer2016-03-104-58/+18
| | | | | | | | | | | | | | | Removed some unused functions and opens. Bug 18394
| * | Cleanup of ARM dependedn code.Bernhard Schommer2016-03-102-66/+8
| | | | | | | | | | | | | | | Removed unused functions and avoid warnings. Bug 18394.
| * | Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-105-17/+21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since the menhir version we use requires ocaml>4.02 we can also upgrade the required ocaml version to >4.02 and remove the deprecate String functions. Also we now activate all warnings except for 4,9 und 27 for regular code plus a bunch of warnings for the generated code. 4 and 9 are not really usefull and 27 is deactivated since until the usage string is printed in a way that requires no newline. Bug 18394.
| * | Code cleanup.Bernhard Schommer2016-03-1056-740/+590
| | | | | | | | | | | | | | | | | | Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394.
generated by cgit (git 2.34.1) at 2024-07-02 20:08:04 +0000