Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | In AST.calling_conventions, record whether the original C function was ↵ | Xavier Leroy | 2015-05-22 | 4 | -23/+28 |
| | | | | | | "old-style" unprototyped. Use this info in printing function types for Csyntax and Clight. | ||||
* | Missing case in type_conditional (long long vs. int or float). | Xavier Leroy | 2015-05-22 | 1 | -6/+3 |
| | |||||
* | Ctyping: better typing of conditional expressions. | Xavier Leroy | 2015-05-21 | 4 | -52/+202 |
| | | | | | | | | | | | | Ctyping: define a typechecker for whole programs. Csyntax: introduce the type "pre-program" (non-dependent). C2C: use Ctyping.econdition instead of Ctyping.econdition'. Note: Ctyping.typecheck_program could be used as the first step in the verified compilation pipeline. Then, retyping would no longer be performed in C2C. We keep it this way (for the time being) because retyping errors are reported more precisely in C2C than in Ctyping. | ||||
* | Changed the producer tag to include more information. | Bernhard Schommer | 2015-05-18 | 1 | -1/+2 |
| | |||||
* | Make a register as storage specify to a fatal error. | Bernhard Schommer | 2015-05-14 | 1 | -1/+1 |
| | |||||
* | Merged PrintAnnot into PrintAsmaux. | Bernhard Schommer | 2015-05-14 | 7 | -200/+178 |
| | |||||
* | Changed the enter_or_refine_ident function to produce an error if a ↵ | Bernhard Schommer | 2015-05-13 | 1 | -6/+14 |
| | | | | non-static declaration is followed by a static declaration/definition. | ||||
* | Updated PrintOp for the single-precision FP operations. | Xavier Leroy | 2015-05-09 | 3 | -0/+41 |
| | |||||
* | Extended inline asm: revised treatment of clobbered registers. | Xavier Leroy | 2015-05-09 | 17 | -110/+147 |
| | | | | | | | | | | - 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 |
| | |||||
* | Typo: Val.sun_inject -> Val.sub_inject. | Xavier Leroy | 2015-05-06 | 2 | -5/+5 |
| | |||||
* | Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵ | Xavier Leroy | 2015-04-30 | 18 | -371/+373 |
| | | | | Val.lessdef, etc. | ||||
* | Detect uses of anonymous structs/unions (a C2011 feature and GCC extension) ↵ | Xavier Leroy | 2015-04-30 | 1 | -0/+14 |
| | | | | and produce a diagnostic instead of ignoring them. | ||||
* | Detect and reject "&" operator applied to "register" local variable or to a ↵ | Xavier Leroy | 2015-04-28 | 3 | -0/+34 |
| | | | | bit field. | ||||
* | Bitfield improvements continued: perform bitfield expansion before ↵ | Xavier Leroy | 2015-04-28 | 3 | -181/+211 |
| | | | | unblocking; improve translation of bitfield initializers and compound literals. | ||||
* | Extended inline asm: handle missing cases. | Xavier Leroy | 2015-04-28 | 8 | -19/+105 |
| | | | | | | Bitfields: better translation of initializers and compound literals; run this pass before unblocking. Transform.stmt: extend with ability to treat unblocked code. test/regression: more bitfield tests. | ||||
* | Warn if a nonzero FP literal converts to infinity (overflow) or to 0 ↵ | Xavier Leroy | 2015-04-25 | 1 | -3/+17 |
| | | | | | | (underflow). Also: spurious '\n' in C2C.warning. | ||||
* | Allow "scratch" (non-allocatable temporary registers) to be mentioned in asm ↵ | Xavier Leroy | 2015-04-23 | 7 | -2/+12 |
| | | | | clobber lists. | ||||
* | Take asm clobbers into account for determining callee-save registers used. | Xavier Leroy | 2015-04-23 | 9 | -4/+37 |
| | |||||
* | Give a name to the type of atoms. | Xavier Leroy | 2015-04-23 | 1 | -2/+4 |
| | |||||
* | Update clightgen to the new annotations and the new inline asm. | Xavier Leroy | 2015-04-23 | 2 | -25/+10 |
| | |||||
* | Merge pull request #40 from AbsInt/inline-asm | Xavier Leroy | 2015-04-22 | 33 | -76/+604 |
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GCC-style extended inline asm. The subset implemented is: - zero or one output - output constraints "=r" (to register) or "=m" (to memory) - zero, one or several inputs - input constraints "r" (in register), "m" (in memory), "i" and "n" (compile-time integer constant) - clobbered registers (the 3rd argument) - both anonymous (%3) and named (%[name]) operands - modifiers %R and %Q to refer to the most significant / least significant part of a register pair holding a 64-bit integer. (Undocumented GCC ARM feature.) All asm statements are treated as "volatile", possibly modifying memory and condition codes. | ||||
| * | Extended asm: more lenient treatment of constraints. | Xavier Leroy | 2015-04-22 | 1 | -10/+21 |
| | | | | | | | | | | We can ignore alternatives as long as one of the constraints we handle (r, m, i, n) is there. | ||||
| * | Avoid multiple errors being reported in the case #outputs >= 2. | Xavier Leroy | 2015-04-21 | 1 | -2/+6 |
| | | |||||
| * | Proper treatment of extended asm. | Xavier Leroy | 2015-04-21 | 1 | -1/+5 |
| | | |||||
| * | Use Cerrors for error reporting instead of rolling our own reporting in C2C. | Xavier Leroy | 2015-04-21 | 1 | -11/+5 |
| | | |||||
| * | Cleanups and updates for extended asm. | Xavier Leroy | 2015-04-21 | 5 | -7/+5 |
| | | |||||
| * | Printing of EF_inline_asm builtins in GCC extended asm syntax. | Xavier Leroy | 2015-04-21 | 1 | -0/+30 |
| | | |||||
| * | Support for GCC-style extended asm, continued: | Xavier Leroy | 2015-04-21 | 15 | -101/+306 |
| | | | | | | | | | | | | | | | | - 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 | 25 | -63/+341 |
| | | |||||
| * | Define M_PI if not already there (it's not in <math.h> for strict ISO C99). | Xavier Leroy | 2015-04-17 | 1 | -0/+4 |
|/ | |||||
* | Correct type of label function. | Bernhard Schommer | 2015-04-16 | 1 | -1/+1 |
| | |||||
* | Added missing dummy functions. | Bernhard Schommer | 2015-04-16 | 2 | -0/+12 |
| | |||||
* | Merge pull request #37 from AbsInt/dwarf | Bernhard Schommer | 2015-04-15 | 24 | -42/+1615 |
|\ | | | | | Added the Dwarf v2 debugging information for global variables and functions for the Diab Backend. | ||||
| * | Merge branch 'dwarf' of /local/schommer/trunk/build/compcert.ppc/compcert ↵ | Bernhard Schommer | 2015-04-14 | 24 | -42/+1615 |
|/| | | | | | | | into dwarf | ||||
| * | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-04-14 | 5 | -7/+18 |
| |\ | |||||
| * \ | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-04-04 | 3 | -12/+23 |
| |\ \ | |||||
| * \ \ | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-04-02 | 88 | -682/+1973 |
| |\ \ \ | |||||
| * \ \ \ | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-04-01 | 2 | -2/+2 |
| |\ \ \ \ | |||||
| * | | | | | Print all files ever encountered in the filenum. | Bernhard Schommer | 2015-04-01 | 3 | -4/+11 |
| | | | | | | |||||
| * | | | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-03-31 | 22 | -112/+1117 |
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile driver/Driver.ml | ||||
| * | | | | | | Added more comments and fixed issue in DwarfPrinter.mli | Bernhard Schommer | 2015-03-30 | 3 | -10/+21 |
| | | | | | | | |||||
| * | | | | | | Refactored code, added comments and changed handling of types with ↵ | Bernhard Schommer | 2015-03-30 | 1 | -316/+417 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | attributes to avoid duplications. | ||||
| * | | | | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-03-30 | 1 | -2/+2 |
| |\ \ \ \ \ \ | |||||
| * | | | | | | | Refactored the DwarfPrinter and added comments. | Bernhard Schommer | 2015-03-30 | 1 | -106/+80 |
| | | | | | | | | |||||
| * | | | | | | | Compute the size of structs using the result of the packing and bitfield ↵ | Bernhard Schommer | 2015-03-26 | 3 | -18/+36 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | transformations. | ||||
| * | | | | | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-03-26 | 1 | -9/+4 |
| |\ \ \ \ \ \ \ | |||||
| * | | | | | | | | Added missing functions for printing the structs and unions. Still missing ↵ | Bernhard Schommer | 2015-03-24 | 6 | -31/+149 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | printing of packed structs. | ||||
| * | | | | | | | | Added translation fucntion for declarations and fundefinitions. | Bernhard Schommer | 2015-03-23 | 6 | -73/+188 |
| | | | | | | | | | |||||
| * | | | | | | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-03-23 | 1 | -2/+6 |
| |\ \ \ \ \ \ \ \ |