aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Added builtin for the dcbi instruction.Bernhard Schommer2015-08-175-4/+11
|
* Update clightgen w.r.t. teh calling_conventions record (new field cc_unproto).Xavier Leroy2015-08-171-1/+2
|
* Update clightgen w.r.t. EF_inline_asm (type of the clobber list).Xavier Leroy2015-08-171-1/+6
|
* Added builitin for the icbi instruction.Bernhard Schommer2015-08-145-1/+11
|
* Added builtin for the lwsync barrier.Bernhard Schommer2015-08-145-3/+12
|
* Also print the system in the output to differentiate between diab and gcc ↵Bernhard Schommer2015-08-051-2/+2
| | | | produced code in later checks.
* Swapped high and low pc in the printing of the debug information for ↵Bernhard Schommer2015-07-241-2/+2
| | | | subroutines.
* More tests for alias analysis.Xavier Leroy2015-07-202-6/+30
|
* ValueDomain: add some documentation comments.Xavier Leroy2015-07-191-20/+32
|
* Test to check that alias analysis is prudently conservative on ill-defined ↵Xavier Leroy2015-07-193-1/+153
| | | | pointer manipulations.
* Value analysis: keep track of pointer values that leak through small ↵Xavier Leroy2015-07-199-232/+250
| | | | | | integers with Uns or Sgn abstract values. This is a follow-up to commit 2932b53. It adds provenance tracking to the Uns and Sgn abstract values.
* Value analysis: keep track of pointer values that leak through arithmetic ↵Xavier Leroy2015-07-195-163/+171
| | | | | | operations with undefined behaviors. Consider (x ^ 1) ^ 1 where x is a intptr_t containing a pointer value. "x ^ 1" evaluates to Vundef in the CompCert semantics, hence the value analysis, in strict mode, gives abstract result Ifptr Pbot (= any number but not a pointer). In relaxed mode, we now give abstract result Ifptr (poffset p) where p is the abstraction of the pointer, thus keeping track of the actual leak of the pointer value.
* ValueDomain.aptr_of_aval: be more conservative with pointers synthesized ↵Xavier Leroy2015-07-182-6/+14
| | | | | | from numbers. For example: *((int *) 0x10000) = 0. This write used to be treated as not interfering with any load. With this change, in relaxed value analysis mode, it is treated as interfering with any load except those from the current stack frame.
* Missing cases in ValueDomain.vnormalize, causing overapproximation.Xavier Leroy2015-07-181-2/+2
|
* Missing case in ValueDomain.pincl, causing incompleteness.Xavier Leroy2015-07-181-0/+9
|
* Remove non digit and non letter chars from filename used in renaming of ↵Bernhard Schommer2015-07-151-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 Leroy2015-07-151-3/+12
|
* Reject incomplete types as return type.Bernhard Schommer2015-07-141-1/+4
|
* Use env1 instead of env to also have the type specifiers used in the return ↵Bernhard Schommer2015-07-091-1/+1
| | | | parameter.
* Also test if the __VA_LIST macro is defined to avoid problems with the ↵Bernhard Schommer2015-07-091-2/+8
| | | | typedefs in stdio, etc. for the diab compiler.
* Propagated the composed type constructed build during identifier lookup.Bernhard Schommer2015-07-091-6/+6
|
* Merge branch 'master' of https://github.com/AbsInt/CompCertXavier Leroy2015-07-0817-32/+125
|\
| * Turn off copy optimization when returning a composite by reference.Xavier Leroy2015-07-084-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 Leroy2015-07-081-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 Leroy2015-07-081-1/+6
| | | | | | | | Also: improve error message by showing old and new types.
| * Fix issue with bit fields of type _BoolXavier Leroy2015-07-084-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/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.tuple to an equivalent definition that works better w.r.t. universe constraints.
| | | * 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 ↵Bernhard Schommer2015-07-072-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 Schommer2015-07-071-1/+1
| |/ | | | | | | defined the incompatible vararg type.
* / More portable test for fres and fsqrte.Xavier Leroy2015-07-083-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 Leroy2015-07-071-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_exportBernhard Schommer2015-07-068-10/+438
|\ | | | | Json export
| * Use the functions from C2C to extract the information for the atoms. ↵Bernhard Schommer2015-07-061-17/+18
| | | | | | | | Simplified printing of storage class.
| * Merge branch 'master' into json_exportBernhard Schommer2015-07-0633-201/+503
| |\ | |/ |/| | | | | Conflicts: driver/Driver.ml
* | 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 ↵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
| |\ \
generated by cgit (git 2.34.1) at 2024-07-02 23:02:13 +0000