Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'master' into debug_locations | Bernhard Schommer | 2015-08-26 | 15 | -241/+268 |
|\ | | | | | | | | | | | | | Conflicts: debug/CtoDwarf.ml debug/DwarfPrinter.ml debug/DwarfTypes.mli | ||||
| * | Improve printing of internal compiler errors. | Xavier Leroy | 2015-08-25 | 1 | -2/+2 |
| | | |||||
| * | Fixed the -T option. | Bernhard Schommer | 2015-08-25 | 1 | -1/+1 |
| | | | | | | | | The diab compiler expected -Wm<pathname> without whitespace. | ||||
| * | Fixed abbreviation of DW_TAG_formal_parameter. | Bernhard Schommer | 2015-08-25 | 1 | -1/+1 |
| | | | | | | | | | | | | Dwarf debuging entries for formal parameters were printed as variables. This could lead to confusion in function pointer types and later with local variables. | ||||
| * | Fixed error in handling of anonymous struct/union/enum types. | Bernhard Schommer | 2015-08-24 | 1 | -8/+15 |
| | | | | | | | | Composite types should be always handled by the composite_type_info table and not by the normal type table. | ||||
| * | Also change the order of high and low pc in the compilation unit tag. | Bernhard Schommer | 2015-08-24 | 1 | -1/+1 |
| | | |||||
| * | Count number of input files and do not use number of source files for ↵ | Bernhard Schommer | 2015-08-24 | 1 | -12/+14 |
| | | | | | | | | warning about no input. | ||||
| * | Added error message when no input file is specified. | Bernhard Schommer | 2015-08-23 | 1 | -0/+5 |
| | | |||||
| * | Revert "Added support for the location of non static global variables." | Bernhard Schommer | 2015-08-23 | 3 | -9/+2 |
| | | | | | | | | This reverts commit b4846ffadfa3fbb73ffa7d9c43e5218adeece8da. | ||||
| * | Do not add subsize tag to array types without size such as flexible array ↵ | Bernhard Schommer | 2015-08-23 | 1 | -10/+14 |
| | | | | | | | | members. | ||||
| * | Added the directory ../share/compcert to the search path for .ini files and ↵ | Bernhard Schommer | 2015-08-23 | 1 | -9/+12 |
| | | | | | | | | replaced the if else for the different possibilities by a List.find. | ||||
| * | test/regression: test packedstruct1 only if unaligned accesses are supported. | Xavier Leroy | 2015-08-21 | 5 | -6/+15 |
| | | | | | | | | Also: exit on error when a test fails. | ||||
| * | Erase incomplete file .depend.extr if "make depend" fails. | Xavier Leroy | 2015-08-21 | 1 | -3/+2 |
| | | |||||
| * | Don't use strdup(), it is not ISO C99. | Xavier Leroy | 2015-08-21 | 1 | -1/+2 |
| | | |||||
| * | Asmexpand for ARM: fixed bug in Pfreeframe. | Xavier Leroy | 2015-08-21 | 2 | -5/+5 |
| | | | | | | | | Plus: update comments and credit Bernhard Schommer. | ||||
| * | Fix bugs in Asmexpand.ml for ARM. | Xavier Leroy | 2015-08-21 | 1 | -8/+9 |
| | | |||||
| * | Consistent naming of "P" instructions and consistent ordering of arguments | Xavier Leroy | 2015-08-21 | 3 | -174/+171 |
| | | | | | | | | according to Intel convention (instr destination, argument). | ||||
* | | Added symbol functions for printing of the location for global variables. | Bernhard Schommer | 2015-08-21 | 10 | -28/+69 |
|/ | |||||
* | Fixed bugs in asm expansion causing the test suite to fail. | Xavier Leroy | 2015-08-21 | 1 | -13/+20 |
| | | | | More bugs remain. | ||||
* | Added command line option to specify a linker command file for the linker. | Bernhard Schommer | 2015-08-20 | 1 | -0/+5 |
| | |||||
* | Added support for the location of non static global variables. | Bernhard Schommer | 2015-08-18 | 3 | -2/+9 |
| | |||||
* | Added builtin for the dcbf instruction | Bernhard Schommer | 2015-08-17 | 5 | -0/+9 |
| | |||||
* | Merge pull request #46 from AbsInt/asmexpand | Xavier Leroy | 2015-08-17 | 8 | -615/+1031 |
|\ | | | | | Merge branch 'asmexpand' of github.com:AbsInt/CompCert | ||||
| * | Merge branch 'master' into asmexpand | Bernhard Schommer | 2015-07-14 | 1 | -1/+4 |
| |\ | |||||
| * | | Updated the branch and implemented the suggested changes. | Bernhard Schommer | 2015-07-14 | 3 | -44/+78 |
| | | | |||||
| * | | Merge branch 'master' into asmexpand | Bernhard Schommer | 2015-07-14 | 51 | -241/+1046 |
| |\ \ | |||||
| * | | | Merge branch 'asmexpand' of github.com:AbsInt/CompCert | Bernhard Schommer | 2015-06-26 | 8 | -615/+997 |
| | | | | |||||
* | | | | Added builtin for the dcbi instruction. | Bernhard Schommer | 2015-08-17 | 5 | -4/+11 |
| | | | | |||||
* | | | | Update clightgen w.r.t. teh calling_conventions record (new field cc_unproto). | Xavier Leroy | 2015-08-17 | 1 | -1/+2 |
| | | | | |||||
* | | | | Update clightgen w.r.t. EF_inline_asm (type of the clobber list). | Xavier Leroy | 2015-08-17 | 1 | -1/+6 |
| | | | | |||||
* | | | | Added builitin for the icbi instruction. | Bernhard Schommer | 2015-08-14 | 5 | -1/+11 |
| | | | | |||||
* | | | | Added builtin for the lwsync barrier. | Bernhard Schommer | 2015-08-14 | 5 | -3/+12 |
| | | | | |||||
* | | | | Also print the system in the output to differentiate between diab and gcc ↵ | Bernhard Schommer | 2015-08-05 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | | produced code in later checks. | ||||
* | | | | Swapped high and low pc in the printing of the debug information for ↵ | Bernhard Schommer | 2015-07-24 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | | subroutines. | ||||
* | | | | More tests for alias analysis. | Xavier Leroy | 2015-07-20 | 2 | -6/+30 |
| | | | | |||||
* | | | | ValueDomain: add some documentation comments. | Xavier Leroy | 2015-07-19 | 1 | -20/+32 |
| | | | | |||||
* | | | | Test to check that alias analysis is prudently conservative on ill-defined ↵ | Xavier Leroy | 2015-07-19 | 3 | -1/+153 |
| | | | | | | | | | | | | | | | | pointer manipulations. | ||||
* | | | | Value analysis: keep track of pointer values that leak through small ↵ | Xavier Leroy | 2015-07-19 | 9 | -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 Leroy | 2015-07-19 | 5 | -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 Leroy | 2015-07-18 | 2 | -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 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. |