aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* | | Tighten and prove correct the underflow/overflow bounds for parsing of FP ↵Xavier Leroy2015-07-063-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 Schommer2015-07-033-14/+52
| | | | | | | | | | | | information.
* | | Added a fast test for too large exponents too avoid never ending computations.Bernhard Schommer2015-07-031-29/+42
| | |
* | | Simple path for problems whith diab assembler in the case of functions in ↵Bernhard Schommer2015-07-031-9/+48
| | | | | | | | | | | | different sections.
* | | Do not search for high and low pc of inlined functions.Bernhard Schommer2015-07-023-5/+13
| | |
* | | Allow Anonymous structs, unions and enums in debug info.Bernhard Schommer2015-07-023-18/+18
| | |
* | | Add bulitin typedes during C to dwarf translation.Bernhard Schommer2015-07-021-6/+9
| | |
* | | Added Build, Tag, etc in version string and driver/Version.ml should be ignoredBernhard Schommer2015-07-012-2/+2
| | |
* | | Removed the version from the compcert.ini file and add it again in a ↵Bernhard Schommer2015-07-019-21/+27
| | | | | | | | | | | | separate file.
* | | Merge branch 'master' of https://github.com/AbsInt/CompCertXavier Leroy2015-06-308-17/+84
|\ \ \
| * \ \ Merge github.com:AbsInt/CompCertBernhard Schommer2015-06-262-16/+33
| |\ \ \ | | | |/ | | |/|
| | * | 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
| | | | | |
| * | | | | Make also the wchar definition diab compatible.Bernhard Schommer2015-06-261-0/+15
| | | | | |
| * | | | | Added diab specific macros for stddef to avoid redefinition of size_t.Bernhard Schommer2015-06-261-0/+9
| |/ / / /
| * | | | 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
| | | | |
* | | | | Signedness issue in specification of subtraction between two pointers.Xavier Leroy2015-06-306-7/+32
|/ / / /
| | | * Added diab specific size_t define in stddef.Bernhard Schommer2015-06-261-0/+9
| | | |
| | | * Print bit representation of floats.Bernhard Schommer2015-06-241-5/+6
| | | |
| | | * Fixed typo also in json export.Bernhard Schommer2015-06-221-1/+1
| | | |
| | | * Merge branch 'master' into json_exportBernhard Schommer2015-06-225-7/+7
| | | |\ | |_|_|/ |/| | |
* | | | Changed a minor typo: Pstwxu should be PstwuxBernhard Schommer2015-06-225-7/+7
| |/ / |/| |
| | * Merge branch 'master' into json_exportBernhard Schommer2015-06-1719-38/+487
| | |\ | |_|/ |/| |
* | | 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.
| | * Merge branch 'master' into json_exportBernhard Schommer2015-05-294-29/+31
| | |\ | |_|/ |/| |
* | | 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
| | |
| | * Merged instructions that are printed as same instruction already in printer.Bernhard Schommer2015-05-291-26/+26
| | |
generated by cgit (git 2.34.1) at 2024-07-04 23:18:16 +0000