Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | | | Added Build, Tag, etc in version string and driver/Version.ml should be ignored | Bernhard Schommer | 2015-07-01 | 2 | -2/+2 | |
| | | | ||||||
* | | | Removed the version from the compcert.ini file and add it again in a ↵ | Bernhard Schommer | 2015-07-01 | 9 | -21/+27 | |
| | | | | | | | | | | | | separate file. | |||||
* | | | Merge branch 'master' of https://github.com/AbsInt/CompCert | Xavier Leroy | 2015-06-30 | 8 | -17/+84 | |
|\ \ \ | ||||||
| * \ \ | Merge github.com:AbsInt/CompCert | Bernhard Schommer | 2015-06-26 | 2 | -16/+33 | |
| |\ \ \ | | | |/ | | |/| | ||||||
| | * | | Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert" | Bernhard Schommer | 2015-06-26 | 8 | -997/+615 | |
| | | | | | | | | | | | | | | | | | | | | This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1. | |||||
| | * | | Merge branch 'asmexpand' of github.com:AbsInt/CompCert | Bernhard Schommer | 2015-06-26 | 8 | -615/+997 | |
| | |\ \ | ||||||
| | | * \ | Merge branch 'master' into asmexpand | Bernhard Schommer | 2015-06-22 | 6 | -21/+61 | |
| | | |\ \ | ||||||
| | | * | | | Moved the rest of the ia32 builtins to asmexpand. | Bernhard Schommer | 2015-06-22 | 4 | -310/+293 | |
| | | | | | | ||||||
| | | * | | | Started moving functions from TargetPrinter.ml to Asmexpand.ml for ia32. | Bernhard Schommer | 2015-06-18 | 3 | -2/+253 | |
| | | | | | | ||||||
| | | * | | | Moved the printing of the builtin functions etc. into Asmexpand for ARM in ↵ | Bernhard Schommer | 2015-06-10 | 5 | -327/+475 | |
| | | | | | | | | | | | | | | | | | | | | | | | | the same way as it is done for PPC. | |||||
| | * | | | | Added --version option to print version string. | Bernhard Schommer | 2015-06-26 | 1 | -9/+19 | |
| | | | | | | ||||||
| | * | | | | Adapt LICENSE file to include AbsInt and how to obtain a commercial license. | Bernhard Schommer | 2015-06-26 | 1 | -7/+14 | |
| | | | | | | ||||||
| * | | | | | Make also the wchar definition diab compatible. | Bernhard Schommer | 2015-06-26 | 1 | -0/+15 | |
| | | | | | | ||||||
| * | | | | | Added diab specific macros for stddef to avoid redefinition of size_t. | Bernhard Schommer | 2015-06-26 | 1 | -0/+9 | |
| |/ / / / | ||||||
| * | | | | Merge branch 'master' of file:///common/repositories/git/tools/compcert | Bernhard Schommer | 2015-06-26 | 3 | -0/+0 | |
| |\ \ \ \ | ||||||
| | * | | | | Remove stray +x. | Christoph Mallon | 2015-06-25 | 3 | -0/+0 | |
| | | | | | | ||||||
| * | | | | | Check also the discarded part of the switch statements for cases outside of ↵ | Bernhard Schommer | 2015-06-26 | 1 | -1/+26 | |
| |/ / / / | | | | | | | | | | | | | | | | an switch to bail out on earlier on unstructured switch. | |||||
| * | | | | Simple fix for problem with local extern. | Bernhard Schommer | 2015-06-24 | 1 | -0/+1 | |
| | | | | | ||||||
* | | | | | Signedness issue in specification of subtraction between two pointers. | Xavier Leroy | 2015-06-30 | 6 | -7/+32 | |
|/ / / / | ||||||
| | | * | Added diab specific size_t define in stddef. | Bernhard Schommer | 2015-06-26 | 1 | -0/+9 | |
| | | | | ||||||
| | | * | Print bit representation of floats. | Bernhard Schommer | 2015-06-24 | 1 | -5/+6 | |
| | | | | ||||||
| | | * | Fixed typo also in json export. | Bernhard Schommer | 2015-06-22 | 1 | -1/+1 | |
| | | | | ||||||
| | | * | Merge branch 'master' into json_export | Bernhard Schommer | 2015-06-22 | 5 | -7/+7 | |
| | | |\ | |_|_|/ |/| | | | ||||||
* | | | | Changed a minor typo: Pstwxu should be Pstwux | Bernhard Schommer | 2015-06-22 | 5 | -7/+7 | |
| |/ / |/| | | ||||||
| | * | Merge branch 'master' into json_export | Bernhard Schommer | 2015-06-17 | 19 | -38/+487 | |
| | |\ | |_|/ |/| | | ||||||
* | | | Update the years.v2.5 | Xavier Leroy | 2015-06-12 | 1 | -2/+2 | |
| | | | ||||||
* | | | More updates for release 2.5. | Xavier Leroy | 2015-06-11 | 1 | -4/+5 | |
| | | | ||||||
* | | | Turn the error on anonymous structs/unions into a warning. | Xavier Leroy | 2015-06-11 | 1 | -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 Leroy | 2015-06-11 | 2 | -6/+31 | |
| | | | ||||||
* | | | Update for release 2.5. | Xavier Leroy | 2015-06-11 | 1 | -6/+15 | |
| | | | ||||||
* | | | Update for release 2.5. | Xavier Leroy | 2015-06-11 | 1 | -6/+11 | |
|/ / | ||||||
* | | Merge pull request #43 from AbsInt/standard-headers | Xavier Leroy | 2015-06-08 | 11 | -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 Leroy | 2015-05-09 | 1 | -1/+1 | |
| | | | ||||||
| * | | Improve compatibility with MacOS X. | Xavier Leroy | 2015-04-26 | 1 | -0/+3 | |
| | | | ||||||
| * | | Provide and use compiler-dependent standard headers. | Xavier Leroy | 2015-04-25 | 11 | -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 Leroy | 2015-06-07 | 2 | -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 Leroy | 2015-06-06 | 1 | -2/+8 | |
| | | | | | | | | | | | | variable is redefined as a typedef. | |||||
* | | | Update Changelog for release 2.5. | Xavier Leroy | 2015-06-05 | 1 | -4/+79 | |
| | | | ||||||
* | | | Allow the option -o to be also the prefix of the file name for compability ↵ | Bernhard Schommer | 2015-05-31 | 1 | -0/+2 | |
| | | | | | | | | | | | | with different build systems. | |||||
| | * | Merge branch 'master' into json_export | Bernhard Schommer | 2015-05-29 | 4 | -29/+31 | |
| | |\ | |_|/ |/| | | ||||||
* | | | In AST.calling_conventions, record whether the original C function was ↵ | Xavier Leroy | 2015-05-22 | 4 | -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 Leroy | 2015-05-22 | 1 | -6/+3 | |
| | | | ||||||
| | * | Merged instructions that are printed as same instruction already in printer. | Bernhard Schommer | 2015-05-29 | 1 | -26/+26 | |
| | | | ||||||
| | * | Merge branch 'master' into json_export | Bernhard Schommer | 2015-05-21 | 5 | -53/+204 | |
| | |\ | |_|/ |/| | | ||||||
* | | | Ctyping: better typing of conditional expressions. | Xavier Leroy | 2015-05-21 | 4 | -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 Schommer | 2015-05-18 | 1 | -1/+2 | |
| | | | ||||||
| | * | Added flag for the renaming of static functions. | Bernhard Schommer | 2015-05-19 | 5 | -8/+27 | |
| | | | ||||||
| | * | Updated the printing of iniline asm and simplified some structures. | Bernhard Schommer | 2015-05-18 | 1 | -136/+118 | |
| | | | ||||||
| | * | Merge branch 'master' into json_export | Bernhard Schommer | 2015-05-18 | 28 | -317/+381 | |
| | |\ | |_|/ |/| | | ||||||
* | | | Make a register as storage specify to a fatal error. | Bernhard Schommer | 2015-05-14 | 1 | -1/+1 | |
| | | |