| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | Isuue #50: outdated comment on type RTL.function. | Xavier Leroy | 2015-09-15 | 1 | -2/+1 |
| * | Issue with ignoring the result of non-void builtin functions. | Xavier Leroy | 2015-09-15 | 3 | -12/+20 |
| * | Upgrade the ARM port to the new builtins. | Xavier Leroy | 2015-08-24 | 1 | -2/+4 |
| * | Some "feel good" proofs about avail sets. | Xavier Leroy | 2015-08-23 | 1 | -0/+171 |
| * | Track the locations of local variables using EF_debug annotations. | Xavier Leroy | 2015-08-23 | 4 | -14/+817 |
| * | Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong. | Xavier Leroy | 2015-08-22 | 15 | -50/+55 |
| * | Simplify the handling of extended inline asm, taking advantage of the new, st... | Xavier Leroy | 2015-08-21 | 1 | -5/+24 |
| * | Refactoring of builtins and annotations in the back-end. | Xavier Leroy | 2015-08-21 | 51 | -1472/+1718 |
| * | Merge pull request #46 from AbsInt/asmexpand | Xavier Leroy | 2015-08-17 | 1 | -0/+57 |
| |\ |
|
| | * | Merge branch 'master' into asmexpand | Bernhard Schommer | 2015-07-14 | 2 | -2/+2 |
| | |\ |
|
| | * | | Merge branch 'asmexpand' of github.com:AbsInt/CompCert | Bernhard Schommer | 2015-06-26 | 1 | -0/+57 |
| | * | | Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert" | Bernhard Schommer | 2015-06-26 | 1 | -57/+0 |
| | * | | Moved the printing of the builtin functions etc. into Asmexpand for ARM in th... | Bernhard Schommer | 2015-06-10 | 1 | -0/+57 |
| * | | | ValueDomain: add some documentation comments. | Xavier Leroy | 2015-07-19 | 1 | -20/+32 |
| * | | | Value analysis: keep track of pointer values that leak through small integers... | Xavier Leroy | 2015-07-19 | 3 | -161/+179 |
| * | | | Value analysis: keep track of pointer values that leak through arithmetic ope... | Xavier Leroy | 2015-07-19 | 2 | -156/+164 |
| * | | | ValueDomain.aptr_of_aval: be more conservative with pointers synthesized from... | Xavier Leroy | 2015-07-18 | 2 | -6/+14 |
| * | | | 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 |
| * | | | Introduce tolerance for casts of pointer values to/from 64-bit integers. | Xavier Leroy | 2015-07-15 | 1 | -3/+12 |
| | |/
|/| |
|
| * | | Do not search for high and low pc of inlined functions. | Bernhard Schommer | 2015-07-02 | 1 | -1/+1 |
| * | | Removed the version from the compcert.ini file and add it again in a separate... | Bernhard Schommer | 2015-07-01 | 1 | -1/+1 |
| |/ |
|
| * | Merged PrintAnnot into PrintAsmaux. | Bernhard Schommer | 2015-05-14 | 3 | -185/+163 |
| * | Extended inline asm: revised treatment of clobbered registers. | Xavier Leroy | 2015-05-09 | 2 | -10/+3 |
| * | Use globl also for global variables. | Bernhard Schommer | 2015-05-07 | 1 | -1/+1 |
| * | Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va... | Xavier Leroy | 2015-04-30 | 6 | -63/+63 |
| * | Take asm clobbers into account for determining callee-save registers used. | Xavier Leroy | 2015-04-23 | 1 | -1/+6 |
| * | Cleanups and updates for extended asm. | Xavier Leroy | 2015-04-21 | 1 | -1/+1 |
| * | Support for GCC-style extended asm, continued: | Xavier Leroy | 2015-04-21 | 2 | -2/+18 |
| * | Experiment: support a subset of GCC's extended asm statements. | Xavier Leroy | 2015-04-17 | 3 | -3/+25 |
| * | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-04-14 | 3 | -1/+5 |
| |\ |
|
| | * | Harmless typo ('__' instead of '_') causing a warning at extraction time. | Xavier Leroy | 2015-04-06 | 1 | -1/+1 |
| | * | Missing case for the new 'annot' instruction. | Xavier Leroy | 2015-04-06 | 2 | -0/+4 |
| * | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-04-02 | 47 | -330/+1337 |
| |\| |
|
| | * | Merge pull request #34 from AbsInt/extended-annotations | Xavier Leroy | 2015-04-01 | 46 | -327/+1332 |
| | |\ |
|
| | | * | Updated the Caml part. Added some more tests in annot1.c. | Xavier Leroy | 2015-03-27 | 10 | -73/+88 |
| | | * | Extended arguments to annotations, continued: | Xavier Leroy | 2015-03-27 | 3 | -257/+133 |
| | | * | Extend annotations so that they can keep track of global variables and local ... | Xavier Leroy | 2015-03-27 | 40 | -281/+1395 |
| | * | | Revised semantics of comparisons between a pointer and 0. | Xavier Leroy | 2015-03-15 | 2 | -3/+5 |
| | |/ |
|
| * | | Print all files ever encountered in the filenum. | Bernhard Schommer | 2015-04-01 | 1 | -0/+7 |
| * | | Added translation fucntion for declarations and fundefinitions. | Bernhard Schommer | 2015-03-23 | 1 | -4/+38 |
| * | | Activating the printing of the debug information for supported architecture. | Bernhard Schommer | 2015-03-19 | 1 | -2/+6 |
| * | | Added function to convert C types into their dwarf represnation. | Bernhard Schommer | 2015-03-18 | 2 | -4/+2 |
| * | | Started implementing the printing functions for the debug info. Added a globa... | Bernhard Schommer | 2015-03-16 | 2 | -1/+11 |
| * | | Started integrating the debug printing in the common backend_printer. | Bernhard Schommer | 2015-03-11 | 2 | -0/+4 |
| * | | Merge remote-tracking branch 'github/backend_printer' into dwarf | Bernhard Schommer | 2015-03-10 | 3 | -0/+251 |
| |\| |
|
| | * | Removed unused sel_target, changed cygwin symbol names and changed the defaul... | Bernhard Schommer | 2015-02-19 | 2 | -3/+2 |
| | * | Added an elf prefix to all common elf functions in PrintAsmaux. | Bernhard Schommer | 2015-02-18 | 2 | -17/+15 |
| | * | Changed print_fun/var_info to be functions instead of booleans. | Bernhard Schommer | 2015-02-18 | 2 | -6/+4 |
| | * | Removed some style issues. | Bernhard Schommer | 2015-02-18 | 1 | -65/+71 |
