aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Remove usage of do.Bernhard Schommer2016-10-043-122/+121
| | | | | | Apparently coq compiled with camlp4 has a problem with the user defined do <- ... ; ... and do. Bug 20050
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-024-31/+361
|
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-0222-203/+547
| | | | | | Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port. Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
* Support for 64-bit architectures: x86 in 64-bit modeXavier Leroy2016-10-0131-1625/+4945
| | | | | | | | | | | | | | | | | | | This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model. To activate x86-64 bit support, configure with "x86_64-linux". Main steps: - Enrich Op.v and Asm.v with 64-bit operations - SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers - Conventions1: support x86-64 ABI in addition to the 32-bit ABI. - Add support for the new 64-bit operations everywhere. - runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode To do: - More optimizations are possible on 64-bit integer arithmetic operations. - Could add new chunks to load, say, an unsigned byte into a 64-bit long (currently we load as a 32-bit int then zero-extend). - Implements the wrong ABI for struct passing.
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-0116-752/+478
| | | | | The PowerPC port remains 32-bit only, no support is added for PPC 64. This shows how much work is needed to update an existing port a minima.
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-0176-2557/+4834
| | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* Keep anonymous members of anonymous structs.Bernhard Schommer2016-09-272-3/+5
| | | | | The anonymous members are kept but using them is still an error. Bug 19907
* undefine _Nullable to add some compatibility with macOS 10.12 SDKMichael Schmidt2016-09-231-1/+1
|
* Improved error messages for wrong vararg calls.Bernhard Schommer2016-09-232-4/+10
| | | | | | Now "expected at least %d" instead of "expected %d". Also improved error message for __builtin_debug. Bug 19872
* Catch case of zero in builtin debug.Bernhard Schommer2016-09-221-2/+2
|
* Merge branch 'master' of /common/repositories/git/tools/compcertBernhard Schommer2016-09-221-0/+1
|\
| * mention -Wall in help textMichael Schmidt2016-09-221-0/+1
| |
* | Added sizetyp for subarray bounds. Fix 19894Bernhard Schommer2016-09-223-21/+43
|/
* Added compcert-conformance to wall. Bug 19872Bernhard Schommer2016-09-221-0/+2
|
* Renamed pedantic to implicit-int.Bernhard Schommer2016-09-223-8/+9
| | | | | | | | The only case where compcert raise a pedantic warning was for implicit int parameters. This is the behavior of clang. However since not all other pedantic warnings are supported the behavior of gcc is adopted. Bug 19872.
* Allow %lf type specifier in printf.Bernhard Schommer2016-09-221-1/+1
| | | | | %lf is official part of the C99 standard. Bug 19877
* Reverted noisy change.Bernhard Schommer2016-09-221-1/+1
| | | | | | In order to empty declarations it is necessary to distinguish between forward declarations and empty declarations. Bug 19859
* Merge pull request #142 from maximedenes/minor-fixesXavier Leroy2016-09-213-9/+13
|\ | | | | | | | | | | Fix minor issues in some proofs and tactics. Patch by Maxime Dénès.
| * Fix minor issues in some proofs and tactics.Maxime Dénès2016-09-213-9/+13
| | | | | | | | | | These minor problems were revealed by porting CompCert to Coq 8.6, where they trigger errors.
* | Fix typo in option name. Bug 18004Bernhard Schommer2016-09-211-1/+1
| |
* | Also warn for empty default declarations. Bug 18004Bernhard Schommer2016-09-211-1/+1
| |
* | Make unnamed default + correct empty struct warning. Bug 18004Bernhard Schommer2016-09-212-2/+3
| |
* | Allow empty alignment attribute. Bug 18004Bernhard Schommer2016-09-211-0/+1
| |
* | Remove the duplicated :. Bug 18004Bernhard Schommer2016-09-211-3/+3
| |
* | Ignore also ignores the argunment. Bug 18004Bernhard Schommer2016-09-202-2/+7
| |
* | Merge pull request #139 from AbsInt/advanced-diagnosticsBernhard Schommer2016-09-2021-395/+781
|\ \ | | | | | | Advanced diagnostics
| * | Fixed typos and reverted error message. Bug 18004Bernhard Schommer2016-09-051-9/+9
| | |
| * | Readded parameter number. Bug 18004Bernhard Schommer2016-09-011-6/+6
| | |
| * | Reworded warning. Bug 18004Bernhard Schommer2016-09-011-6/+6
| | |
| * | Simplified int to pointer tests.Bernhard Schommer2016-09-012-16/+17
| | | | | | | | | | | | | | | | | | Now the same warning is triggered for both cases, int to ptr and ptr to int. Bug 18004
| * | Fixed error message for & operator. Bug 18004Bernhard Schommer2016-08-311-1/+1
| | |
| * | Added conformance warning.Bernhard Schommer2016-08-313-0/+4
| | | | | | | | | | | | | | | | | | This warning should be triggered if a feature is used that is not part of the code CompCert C language. Bug 18004
| * | Added back logical operator in error. Bug 18004Bernhard Schommer2016-08-311-1/+1
| | |
| * | Reworded errors/warnings in Elab.Bernhard Schommer2016-08-311-60/+76
| | | | | | | | | | | | | | | | | | | | | | | | Some old errors/warnings messages were better before and are now rephrased. Furthermore some formulations are rephrased to match the used formulations of the ISO C stanard, e.g. storage class is replaced with storage-class. Bug 18004
| * | Restored original bit-field warning. Bug 18004Bernhard Schommer2016-08-311-1/+1
| | |
| * | Updated comment string. Bug 18004.Bernhard Schommer2016-08-312-3/+3
| | |
| * | Readded warning about ignored volatile. Bug 18004Bernhard Schommer2016-08-311-1/+1
| | |
| * | Added missing literal. Bug 18004Bernhard Schommer2016-08-311-1/+1
| | |
| * | Fixed typos.Bernhard Schommer2016-08-311-8/+8
| | | | | | | | | | | | | | | | | | Removed duplicated of, changed string to string literal for wording than the C standard. Bug 18004
| * | bug 18004, fix some typos/grammarMichael Schmidt2016-08-301-1/+1
| | |
| * | bug 18004, fix some typos/grammarMichael Schmidt2016-08-301-4/+4
| | |
| * | Fixed types in Elab.ml. Bug 18004Bernhard Schommer2016-08-291-5/+5
| | |
| * | Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-8/+18
| |\ \
| * \ \ Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-2956-577/+1051
| |\ \ \
| * | | | Added raw printing of types without formatting.Bernhard Schommer2016-08-163-5/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This avoids introducing line breaks during printing of function types. Bug 18004
| * | | | Additional test for color output.Bernhard Schommer2016-08-056-75/+102
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Color output is only enabled if stderr is a tty, and the environment variable TERM is not empty or dumb. Bug 18004
| * | | | Classified all warnings and added various options.Bernhard Schommer2016-07-2916-358/+690
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now each warning either has a name and can be turned on/off, made into an error,etc. or is a warning that always will be triggered. The message of the warnings are similar to the ones emited by gcc/clang and all fit into one line. Furthermore the diagnostics are now colored if colored output is available. Bug 18004
* | | | | IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-185-50/+187
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | lib/Integers.v: define division-remainder of a double word by a word ia32/Asm.v: use it to give Pdiv and Pidiv their "true" semantics like in the processor; add Pcltd as an instruction ia32/*: adapt accordingly Additional benefit: Pcltd could be used for an alternate implementation of shrximm.
* | | | | Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-173-31/+39
| | | | | | | | | | | | | | | | | | | | Inline directives in extraction.v make the Caml output efficient and almost nice.
* | | | | Decidableplus: remove stuff that was cut-and-paste from Coq 8.5 libraryXavier Leroy2016-09-171-48/+1
| | | | | | | | | | | | | | | | | | | | The cut-and-paste was for compatibility with Coq 8.4
generated by cgit (git 2.34.1) at 2024-07-05 09:05:33 +0000