aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | Merge github.com:AbsInt/CompCertBernhard Schommer2015-07-071-2/+5
| |\ \
| | * \ Merge pull request #49 from jhjourdan/ch2o_universes_compatXavier Leroy2015-07-071-2/+5
| | |\ \
| | | * | Change the definition of Typles.tupleJacques-Henri Jourdan2015-07-071-2/+5
| | |/ /
| * | | Removed brackets around ty in macro of offestof.Bernhard Schommer2015-07-071-1/+1
| * | | Diab defines w_char to be unsigned short.Bernhard Schommer2015-07-075-3/+11
| * | | Better define the __GNUC__ macro which avoids the inclusion of va_list header...Bernhard Schommer2015-07-072-1/+5
| * | | Added an define to avoid the inclusion of the diab va_list header which defin...Bernhard Schommer2015-07-071-1/+1
| |/ /
* / / More portable test for fres and fsqrte.Xavier Leroy2015-07-083-7/+16
|/ /
* | Set/clear CR6 before calling an unprototyped function.Xavier Leroy2015-07-071-3/+4
* | Merge pull request #48 from AbsInt/json_exportBernhard Schommer2015-07-068-10/+438
|\ \
| * | Use the functions from C2C to extract the information for the atoms. Simplifi...Bernhard Schommer2015-07-061-17/+18
| * | Merge branch 'master' into json_exportBernhard Schommer2015-07-0633-201/+503
| |\ \ | |/ / |/| |
* | | Corrected little typo in __builtin_clz function.Bernhard Schommer2015-07-065-7/+7
* | | Tighten and prove correct the underflow/overflow bounds for parsing of FP lit...Xavier Leroy2015-07-063-137/+249
* | | Allow forward declarations of structure and union types in the debug informat...Bernhard Schommer2015-07-033-14/+52
* | | 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 dif...Bernhard Schommer2015-07-031-9/+48
* | | 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 separate...Bernhard Schommer2015-07-019-21/+27
* | | 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
| | * | 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 th...Bernhard Schommer2015-06-105-327/+475
| | * | | | 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 a...Bernhard Schommer2015-06-261-1/+26
| |/ / / /
| * | | | 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
* | | Preserve ordinary comments within proof scripts.Xavier Leroy2015-06-112-6/+31
* | | Update for release 2.5.Xavier Leroy2015-06-111-6/+15