aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'asmexpand' of github.com:AbsInt/CompCertBernhard Schommer2015-06-268-615/+997
|
* Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"Bernhard Schommer2015-06-268-997/+615
| | | | | This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
* Merge branch 'asmexpand' of github.com:AbsInt/CompCertBernhard Schommer2015-06-268-615/+997
|\
| * Merge branch 'master' into asmexpandBernhard Schommer2015-06-226-21/+61
| |\
| * | Moved the rest of the ia32 builtins to asmexpand.Bernhard Schommer2015-06-224-310/+293
| | |
| * | Started moving functions from TargetPrinter.ml to Asmexpand.ml for ia32.Bernhard Schommer2015-06-183-2/+253
| | |
| * | Moved the printing of the builtin functions etc. into Asmexpand for ARM in ↵Bernhard Schommer2015-06-105-327/+475
| | | | | | | | | | | | the same way as it is done for PPC.
* | | Added --version option to print version string.Bernhard Schommer2015-06-261-9/+19
| | |
* | | Adapt LICENSE file to include AbsInt and how to obtain a commercial license.Bernhard Schommer2015-06-261-7/+14
| | |
* | | Merge branch 'master' of file:///common/repositories/git/tools/compcertBernhard Schommer2015-06-263-0/+0
|\ \ \
| * | | Remove stray +x.Christoph Mallon2015-06-253-0/+0
| | | |
* | | | Check also the discarded part of the switch statements for cases outside of ↵Bernhard Schommer2015-06-261-1/+26
|/ / / | | | | | | | | | an switch to bail out on earlier on unstructured switch.
* | | Simple fix for problem with local extern.Bernhard Schommer2015-06-241-0/+1
| | |
* | | Changed a minor typo: Pstwxu should be PstwuxBernhard Schommer2015-06-225-7/+7
| |/ |/|
* | Update the years.v2.5Xavier Leroy2015-06-121-2/+2
| |
* | More updates for release 2.5.Xavier Leroy2015-06-111-4/+5
| |
* | Turn the error on anonymous structs/unions into a warning.Xavier Leroy2015-06-111-1/+1
| | | | | | | | | | Otherwise we get too many errors on glibc's standard headers. A real error will occur when the anonymous struct/union is accessed.
* | Preserve ordinary comments within proof scripts.Xavier Leroy2015-06-112-6/+31
| |
* | Update for release 2.5.Xavier Leroy2015-06-111-6/+15
| |
* | Update for release 2.5.Xavier Leroy2015-06-111-6/+11
|/
* Merge pull request #43 from AbsInt/standard-headersXavier Leroy2015-06-0811-13/+339
|\ | | | | | | | | | | | | | | | | | | Merge of the "standard-headers" branch. This provides CompCert-compatible implementations of the following standard headers: float.h, stdarg.h, stdbool.h, stddef.h, varargs.h. These are the headers that are provided by GCC, Clang, and TCC. Other standard headers are provided by Glibc and similar C standard libraries. So far in CompCert we rely on the headers provided by whatever C compiler is installed on the host platform. This causes some difficulties that this branch addresses: 1- Diab C's stdarg.h is not compatible with CompCert 2- On IA32 and PowerPC, CompCert's "long double" type differs from the "long double" type specified by the ABI. Hence, the platform's float.h gives "long double" parameters that do not match CompCert.
| * Typo in #ifndef guard.Xavier Leroy2015-05-091-1/+1
| |
| * Improve compatibility with MacOS X.Xavier Leroy2015-04-261-0/+3
| |
| * Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-2511-13/+336
| | | | | | | | | | | | | | | | | | | | | | | | This branch provides implementations of the following standard headers: <float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h> These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux).
* | Represent external worlds by a coinductive type rather than an inductive type.Xavier Leroy2015-06-072-2/+2
| | | | | | | | As noticed by R. Krebbers, an inductive type for external worlds implies that all sequences of program-world interactions are finite, which is not the case.
* | Error if, in the same scope, a typedef is redefined as a variable, or a ↵Xavier Leroy2015-06-061-2/+8
| | | | | | | | variable is redefined as a typedef.
* | Update Changelog for release 2.5.Xavier Leroy2015-06-051-4/+79
| |
* | Allow the option -o to be also the prefix of the file name for compability ↵Bernhard Schommer2015-05-311-0/+2
| | | | | | | | with different build systems.
* | In AST.calling_conventions, record whether the original C function was ↵Xavier Leroy2015-05-224-23/+28
| | | | | | | | | | | | "old-style" unprototyped. Use this info in printing function types for Csyntax and Clight.
* | Missing case in type_conditional (long long vs. int or float).Xavier Leroy2015-05-221-6/+3
| |
* | Ctyping: better typing of conditional expressions.Xavier Leroy2015-05-214-52/+202
| | | | | | | | | | | | | | | | | | | | | | | | Ctyping: define a typechecker for whole programs. Csyntax: introduce the type "pre-program" (non-dependent). C2C: use Ctyping.econdition instead of Ctyping.econdition'. Note: Ctyping.typecheck_program could be used as the first step in the verified compilation pipeline. Then, retyping would no longer be performed in C2C. We keep it this way (for the time being) because retyping errors are reported more precisely in C2C than in Ctyping.
* | Changed the producer tag to include more information.Bernhard Schommer2015-05-181-1/+2
| |
* | Make a register as storage specify to a fatal error.Bernhard Schommer2015-05-141-1/+1
| |
* | Merged PrintAnnot into PrintAsmaux.Bernhard Schommer2015-05-147-200/+178
| |
* | Changed the enter_or_refine_ident function to produce an error if a ↵Bernhard Schommer2015-05-131-6/+14
| | | | | | | | non-static declaration is followed by a static declaration/definition.
* | Updated PrintOp for the single-precision FP operations.Xavier Leroy2015-05-093-0/+41
| |
* | Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-0917-110/+147
| | | | | | | | | | | | | | | | | | | | - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
* | Use globl also for global variables.Bernhard Schommer2015-05-071-1/+1
| |
* | Typo: Val.sun_inject -> Val.sub_inject.Xavier Leroy2015-05-062-5/+5
| |
* | Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵Xavier Leroy2015-04-3018-371/+373
| | | | | | | | Val.lessdef, etc.
* | Detect uses of anonymous structs/unions (a C2011 feature and GCC extension) ↵Xavier Leroy2015-04-301-0/+14
| | | | | | | | and produce a diagnostic instead of ignoring them.
* | Detect and reject "&" operator applied to "register" local variable or to a ↵Xavier Leroy2015-04-283-0/+34
| | | | | | | | bit field.
* | Bitfield improvements continued: perform bitfield expansion before ↵Xavier Leroy2015-04-283-181/+211
| | | | | | | | unblocking; improve translation of bitfield initializers and compound literals.
* | Extended inline asm: handle missing cases.Xavier Leroy2015-04-288-19/+105
|/ | | | | | Bitfields: better translation of initializers and compound literals; run this pass before unblocking. Transform.stmt: extend with ability to treat unblocked code. test/regression: more bitfield tests.
* Warn if a nonzero FP literal converts to infinity (overflow) or to 0 ↵Xavier Leroy2015-04-251-3/+17
| | | | | | (underflow). Also: spurious '\n' in C2C.warning.
* Allow "scratch" (non-allocatable temporary registers) to be mentioned in asm ↵Xavier Leroy2015-04-237-2/+12
| | | | clobber lists.
* Take asm clobbers into account for determining callee-save registers used.Xavier Leroy2015-04-239-4/+37
|
* Give a name to the type of atoms.Xavier Leroy2015-04-231-2/+4
|
* Update clightgen to the new annotations and the new inline asm.Xavier Leroy2015-04-232-25/+10
|
* Merge pull request #40 from AbsInt/inline-asmXavier Leroy2015-04-2233-76/+604
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GCC-style extended inline asm. The subset implemented is: - zero or one output - output constraints "=r" (to register) or "=m" (to memory) - zero, one or several inputs - input constraints "r" (in register), "m" (in memory), "i" and "n" (compile-time integer constant) - clobbered registers (the 3rd argument) - both anonymous (%3) and named (%[name]) operands - modifiers %R and %Q to refer to the most significant / least significant part of a register pair holding a 64-bit integer. (Undocumented GCC ARM feature.) All asm statements are treated as "volatile", possibly modifying memory and condition codes.
generated by cgit (git 2.34.1) at 2024-07-03 01:50:37 +0000