Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | | | Corrected little typo in __builtin_clz function. | Bernhard Schommer | 2015-07-06 | 5 | -7/+7 | |
| | | | ||||||
* | | | Tighten and prove correct the underflow/overflow bounds for parsing of FP ↵ | Xavier Leroy | 2015-07-06 | 3 | -137/+249 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | literals. This is a follow-up to commit 350354c. - Move Float.build_from_parsed to Fappli_IEEE_extra.Bparse - Add early checks for overflow and underflow and prove them correct. - Improve speed of Bparse by using a fast exponentiation (square-and-multiply). | |||||
* | | | Allow forward declarations of structure and union types in the debug ↵ | Bernhard Schommer | 2015-07-03 | 3 | -14/+52 | |
| | | | | | | | | | | | | information. | |||||
* | | | Added a fast test for too large exponents too avoid never ending computations. | Bernhard Schommer | 2015-07-03 | 1 | -29/+42 | |
| | | | ||||||
* | | | Simple path for problems whith diab assembler in the case of functions in ↵ | Bernhard Schommer | 2015-07-03 | 1 | -9/+48 | |
| | | | | | | | | | | | | different sections. | |||||
* | | | Do not search for high and low pc of inlined functions. | Bernhard Schommer | 2015-07-02 | 3 | -5/+13 | |
| | | | ||||||
* | | | Allow Anonymous structs, unions and enums in debug info. | Bernhard Schommer | 2015-07-02 | 3 | -18/+18 | |
| | | | ||||||
* | | | Add bulitin typedes during C to dwarf translation. | Bernhard Schommer | 2015-07-02 | 1 | -6/+9 | |
| | | | ||||||
* | | | 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 | |
| | | |