Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 ↵ | Bernhard Schommer | 2015-07-01 | 1 | -1/+1 |
| | | | | separate file. | ||||
* | 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 |
| | | | | | | | | | | - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting | ||||
* | 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 ↵ | Xavier Leroy | 2015-04-30 | 6 | -63/+63 |
| | | | | Val.lessdef, etc. | ||||
* | 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 |
| | | | | | | | | - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml | ||||
* | 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 |
| |\ | | | | | | | Extended annotations | ||||
| | * | 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 |
| | | | | | | | | | | | | | | | - Simplifications in RTLgen. - Updated Cexec. | ||||
| | * | Extend annotations so that they can keep track of global variables and local ↵ | Xavier Leroy | 2015-03-27 | 40 | -281/+1395 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | variables whose address is taken. - CminorSel, RTL: add "annot" instructions. - CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions. - AST, Events: simplify EF_annot because constants are now part of the arguments. Implementation is not complete yet. | ||||
| * | | Revised semantics of comparisons between a pointer and 0. | Xavier Leroy | 2015-03-15 | 2 | -3/+5 |
| |/ | | | | | | | | | | | | | | | | | | | | | It used to be that a pointer value (Vptr) always compare unequal to the null pointer (Vint Int.zero). However, this may not be true in the final machine code when pointer addition overflows and wraps around to the bit pattern 0. This patch checks the validity of the pointer being compared with 0, and makes the comparison undefined if the pointer is out of bounds. Note: only the IA32 back-end was updated, ARM and PowerPC need updating. | ||||
* | | 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 ↵ | Bernhard Schommer | 2015-03-16 | 2 | -1/+11 |
| | | | | | | | | global target dependend option to activate the printing only for targets wher it works. | ||||
* | | 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 |
|\| | | | | | | | | | | | | | Conflicts: arm/PrintAsm.ml ia32/PrintAsm.ml powerpc/PrintAsm.ml | ||||
| * | Removed unused sel_target, changed cygwin symbol names and changed the ↵ | Bernhard Schommer | 2015-02-19 | 2 | -3/+2 |
| | | | | | | | | default function aligment to be target dependent. | ||||
| * | 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 |
| | | |||||
| * | Changed arm backend to the common backend printer. | Bernhard Schommer | 2015-02-09 | 2 | -2/+2 |
| | | |||||
| * | Changed the ia32 backend to the new Printer. | Bernhard Schommer | 2015-02-06 | 1 | -0/+5 |
| | | |||||
| * | Changed the ASM printer of the powerpc to the generalized backend. | Bernhard Schommer | 2015-02-05 | 3 | -2/+119 |
| | | |||||
| * | Moved more common functions into a seperate file. | Bernhard Schommer | 2015-02-04 | 1 | -2/+46 |
| | | |||||
| * | Started moving common backend functions into one file. | Bernhard Schommer | 2015-02-03 | 1 | -0/+84 |
| | | |||||
* | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-01-23 | 3 | -6/+6 |
|\| | |||||
| * | Merge branch 'named-structs' | Xavier Leroy | 2015-01-23 | 3 | -6/+6 |
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Switch CompCert C / Clight AST of composite types (structs and unions) from a structural representation to a nominal representation, closer to concrete syntax. - This avoids algorithmic inefficiencies due to the structural representation. - Closes PR#4. - Smallstep: make small-step semantics more polymorphic in the type of the global environment. - Globalenvs: introduce Senv.t (symbol environments) as a restricted view on Genv.t (full global environments). - Events, Smallstep: use Senv instead of Genv to talk about global names. | ||||
| | * | Introduce symbol environments (type Senv.t) as a restricted view on global ↵ | Xavier Leroy | 2014-11-26 | 3 | -6/+6 |
| | | | | | | | | | | | | environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events). | ||||
* | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-01-20 | 5 | -250/+273 |
|\| | | |||||
| * | | Protect against redefinition of the __i64_xxx helper library functions. | Xavier Leroy | 2015-01-20 | 4 | -244/+252 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is achieved by declaring these functions in C2C.ml, then re-checking their declarations in the global environment during the Selection pass. In passing, the "hf" parameter for SelectLong functions was removed and replaced by fixed identifiers corresponding to the actual names of the helper functions. | ||||
| * | | Follow-up to [5aecefe]: be conservative also in the case of a "common" ↵ | Xavier Leroy | 2015-01-20 | 1 | -6/+21 |
| | | | | | | | | | | | | global const variable. | ||||
* | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-01-12 | 1 | -3/+6 |
|\| | | |||||
| * | | More prudent analysis of uninitialized const global variables. | Xavier Leroy | 2015-01-09 | 1 | -3/+6 |
| | | | | | | | | | | | | | | | | | | | | | In the presence of separate compilation and linking, an uninitialized const global variable may be initialized elsewhere with a pointer value, falsifying the points-to analysis. Report and fix by Chung-Kil Hur and Jeehoon Kang. | ||||
* | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-01-12 | 1 | -0/+67 |
|\| | | |/ |/| | | | | | Conflicts: powerpc/PrintAsm.ml | ||||
| * | In -g -S mode, annotate the generated asm file with the C source code in ↵ | Xavier Leroy | 2015-01-07 | 1 | -0/+67 |
|/ | | | | | | comments. Refactor printing of .loc debug directives in backend/PrintAnnot.ml | ||||
* | Verification of the Unusedglob pass (removal of unreferenced static global ↵ | Xavier Leroy | 2014-11-24 | 4 | -95/+1401 |
| | | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating. | ||||
* | Add Genv.public_symbol operation. | Xavier Leroy | 2014-11-24 | 13 | -56/+136 |
| | | | | | Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating. | ||||
* | Record public global definitions via field "prog_public" in AST.program. | Xavier Leroy | 2014-11-24 | 2 | -0/+3 |
| | | | | For the moment, this field is ignored. | ||||
* | Add flags to control individual optimization passes + flag -O0 for turning ↵ | Xavier Leroy | 2014-11-16 | 2 | -8/+5 |
| | | | | them off. | ||||
* | - Support "switch" statements over 64-bit integers | xleroy | 2014-08-17 | 13 | -479/+845 |
| | | | | | | | | | | | | | (in CompCert C to Cminor, included) - Translation of "switch" to decision trees or jumptables made generic over the sizes of integers and moved to the Cminor->CminorSel pass instead of CminorSel->RTL as before. - CminorSel: add "exitexpr" to support the above. - ValueDomain: more precise analysis of comparisons against an integer literal. E.g. "x >=u 0" is always true. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e |