aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Merge pull request #46 from AbsInt/asmexpandXavier Leroy2015-08-171-0/+57
|\
| * Merge branch 'master' into asmexpandBernhard Schommer2015-07-142-2/+2
| |\
| * | Merge branch 'asmexpand' of github.com:AbsInt/CompCertBernhard Schommer2015-06-261-0/+57
| * | Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"Bernhard Schommer2015-06-261-57/+0
| * | Moved the printing of the builtin functions etc. into Asmexpand for ARM in th...Bernhard Schommer2015-06-101-0/+57
* | | ValueDomain: add some documentation comments.Xavier Leroy2015-07-191-20/+32
* | | Value analysis: keep track of pointer values that leak through small integers...Xavier Leroy2015-07-193-161/+179
* | | Value analysis: keep track of pointer values that leak through arithmetic ope...Xavier Leroy2015-07-192-156/+164
* | | ValueDomain.aptr_of_aval: be more conservative with pointers synthesized from...Xavier Leroy2015-07-182-6/+14
* | | 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
* | | Introduce tolerance for casts of pointer values to/from 64-bit integers.Xavier Leroy2015-07-151-3/+12
| |/ |/|
* | Do not search for high and low pc of inlined functions.Bernhard Schommer2015-07-021-1/+1
* | Removed the version from the compcert.ini file and add it again in a separate...Bernhard Schommer2015-07-011-1/+1
|/
* Merged PrintAnnot into PrintAsmaux.Bernhard Schommer2015-05-143-185/+163
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-092-10/+3
* Use globl also for global variables.Bernhard Schommer2015-05-071-1/+1
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-306-63/+63
* Take asm clobbers into account for determining callee-save registers used.Xavier Leroy2015-04-231-1/+6
* Cleanups and updates for extended asm.Xavier Leroy2015-04-211-1/+1
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-212-2/+18
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-173-3/+25
* Merge branch 'master' into dwarfBernhard Schommer2015-04-143-1/+5
|\
| * Harmless typo ('__' instead of '_') causing a warning at extraction time.Xavier Leroy2015-04-061-1/+1
| * Missing case for the new 'annot' instruction.Xavier Leroy2015-04-062-0/+4
* | Merge branch 'master' into dwarfBernhard Schommer2015-04-0247-330/+1337
|\|
| * Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-0146-327/+1332
| |\
| | * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-2710-73/+88
| | * Extended arguments to annotations, continued:Xavier Leroy2015-03-273-257/+133
| | * Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-2740-281/+1395
| * | Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-152-3/+5
| |/
* | Print all files ever encountered in the filenum.Bernhard Schommer2015-04-011-0/+7
* | Added translation fucntion for declarations and fundefinitions.Bernhard Schommer2015-03-231-4/+38
* | Activating the printing of the debug information for supported architecture.Bernhard Schommer2015-03-191-2/+6
* | Added function to convert C types into their dwarf represnation.Bernhard Schommer2015-03-182-4/+2
* | Started implementing the printing functions for the debug info. Added a globa...Bernhard Schommer2015-03-162-1/+11
* | Started integrating the debug printing in the common backend_printer.Bernhard Schommer2015-03-112-0/+4
* | Merge remote-tracking branch 'github/backend_printer' into dwarfBernhard Schommer2015-03-103-0/+251
|\|
| * Removed unused sel_target, changed cygwin symbol names and changed the defaul...Bernhard Schommer2015-02-192-3/+2
| * Added an elf prefix to all common elf functions in PrintAsmaux.Bernhard Schommer2015-02-182-17/+15
| * Changed print_fun/var_info to be functions instead of booleans.Bernhard Schommer2015-02-182-6/+4
| * Removed some style issues.Bernhard Schommer2015-02-181-65/+71
| * Changed arm backend to the common backend printer.Bernhard Schommer2015-02-092-2/+2
| * Changed the ia32 backend to the new Printer.Bernhard Schommer2015-02-061-0/+5
| * Changed the ASM printer of the powerpc to the generalized backend.Bernhard Schommer2015-02-053-2/+119
| * Moved more common functions into a seperate file.Bernhard Schommer2015-02-041-2/+46
| * Started moving common backend functions into one file.Bernhard Schommer2015-02-031-0/+84
* | Merge branch 'master' into dwarfBernhard Schommer2015-01-233-6/+6
|\|
| * Merge branch 'named-structs'Xavier Leroy2015-01-233-6/+6
| |\
| | * Introduce symbol environments (type Senv.t) as a restricted view on global en...Xavier Leroy2014-11-263-6/+6