Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | | | | Missing cases in ValueDomain.vnormalize, causing overapproximation. | Xavier Leroy | 2015-07-18 | 1 | -2/+2 | |
| | | | | ||||||
* | | | | Missing case in ValueDomain.pincl, causing incompleteness. | Xavier Leroy | 2015-07-18 | 1 | -0/+9 | |
| | | | | ||||||
* | | | | Remove non digit and non letter chars from filename used in renaming of ↵ | Bernhard Schommer | 2015-07-15 | 1 | -0/+1 | |
| | | | | | | | | | | | | | | | | static variables to avoid problems with files such as "a b.c". | |||||
* | | | | Introduce tolerance for casts of pointer values to/from 64-bit integers. | Xavier Leroy | 2015-07-15 | 1 | -3/+12 | |
| |_|/ |/| | | ||||||
* | | | Reject incomplete types as return type. | Bernhard Schommer | 2015-07-14 | 1 | -1/+4 | |
| |/ |/| | ||||||
* | | Use env1 instead of env to also have the type specifiers used in the return ↵ | Bernhard Schommer | 2015-07-09 | 1 | -1/+1 | |
| | | | | | | | | parameter. | |||||
* | | Also test if the __VA_LIST macro is defined to avoid problems with the ↵ | Bernhard Schommer | 2015-07-09 | 1 | -2/+8 | |
| | | | | | | | | typedefs in stdio, etc. for the diab compiler. | |||||
* | | Propagated the composed type constructed build during identifier lookup. | Bernhard Schommer | 2015-07-09 | 1 | -6/+6 | |
| | | ||||||
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert | Xavier Leroy | 2015-07-08 | 17 | -32/+125 | |
|\ \ | ||||||
| * | | Turn off copy optimization when returning a composite by reference. | Xavier Leroy | 2015-07-08 | 4 | -5/+50 | |
| | | | | | | | | | | | | | | | | | | The copy optimization is not correct in case of overlap between destination and source. We would need to use an hypothetical __builtin_memmove_aligned that can cope with overlap to implement the copy at return of callee. | |||||
| * | | Add implicit "return 0;" at end of function "main". | Xavier Leroy | 2015-07-08 | 1 | -1/+13 | |
| | | | | | | | | | | | | | | | | | | | | | | | | As per ISO C99, "hosted environment". "return 0" is added at the end of any function named "main" that has "int" as return type. If the name is "main" but the return type is not "int", emit a warning and do not add anything. | |||||
| * | | Turn "redefinition with an incompatible type" warning into an error. | Xavier Leroy | 2015-07-08 | 1 | -1/+6 | |
| | | | | | | | | | | | | Also: improve error message by showing old and new types. | |||||
| * | | Fix issue with bit fields of type _Bool | Xavier Leroy | 2015-07-08 | 4 | -18/+34 | |
| | | | | | | | | | | | | | | | | | | cparser/Bitfields.ml: when assigning to a bit field of type _Bool, the right-hand side must be normalized to 0 or 1 via a cast to _Bool. test/regression/bitfields{1,9}.c: add corresponding test cases. | |||||
| * | | Merge github.com:AbsInt/CompCert | Bernhard Schommer | 2015-07-07 | 1 | -2/+5 | |
| |\ \ | ||||||
| | * \ | Merge pull request #49 from jhjourdan/ch2o_universes_compat | Xavier Leroy | 2015-07-07 | 1 | -2/+5 | |
| | |\ \ | | | | | | | | | | | Change the definition of Typles.tuple to an equivalent definition that works better w.r.t. universe constraints. | |||||
| | | * | | Change the definition of Typles.tuple | Jacques-Henri Jourdan | 2015-07-07 | 1 | -2/+5 | |
| | |/ / | ||||||
| * | | | Removed brackets around ty in macro of offestof. | Bernhard Schommer | 2015-07-07 | 1 | -1/+1 | |
| | | | | ||||||
| * | | | Diab defines w_char to be unsigned short. | Bernhard Schommer | 2015-07-07 | 5 | -3/+11 | |
| | | | | ||||||
| * | | | Better define the __GNUC__ macro which avoids the inclusion of va_list ↵ | Bernhard Schommer | 2015-07-07 | 2 | -1/+5 | |
| | | | | | | | | | | | | | | | | header and set the __VA_LIST macro if it is not defined. | |||||
| * | | | Added an define to avoid the inclusion of the diab va_list header which ↵ | Bernhard Schommer | 2015-07-07 | 1 | -1/+1 | |
| |/ / | | | | | | | | | | defined the incompatible vararg type. | |||||
* / / | More portable test for fres and fsqrte. | Xavier Leroy | 2015-07-08 | 3 | -7/+16 | |
|/ / | | | | | | | These instructions are approximate and produce different results on different processors. Just check the error bounds specified in the PPC ISA. | |||||
* | | Set/clear CR6 before calling an unprototyped function. | Xavier Leroy | 2015-07-07 | 1 | -3/+4 | |
| | | | | | | | | | | | | A function declared without a prototype could be implemented by a vararg function (even though this is undefined behavior in C99). Be nice in this case. | |||||
* | | Merge pull request #48 from AbsInt/json_export | Bernhard Schommer | 2015-07-06 | 8 | -10/+438 | |
|\ \ | | | | | | | Json export | |||||
| * | | Use the functions from C2C to extract the information for the atoms. ↵ | Bernhard Schommer | 2015-07-06 | 1 | -17/+18 | |
| | | | | | | | | | | | | Simplified printing of storage class. | |||||
| * | | Merge branch 'master' into json_export | Bernhard Schommer | 2015-07-06 | 33 | -201/+503 | |
| |\ \ | |/ / |/| | | | | | | | | Conflicts: driver/Driver.ml | |||||
* | | | 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. |