aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* All axioms used in the CompCert developmentxleroy2010-06-281-0/+27
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-2812-308/+546
* Updated Caml parts to match new representation for global variables.xleroy2010-05-265-26/+57
* Clean upxleroy2010-05-261-25/+0
* Typo in documentationxleroy2010-05-261-1/+1
* More faithful semantics for volatile reads and writes.xleroy2010-05-2336-423/+684
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-1032-351/+507
* Another regressionxleroy2010-05-103-1/+10
* Fewer float axioms.xleroy2010-05-092-6/+3
* Suppressed axioms Float.eq_zero_{true,false}, since the latter isxleroy2010-05-093-14/+8
* Revised encoding/decoding of floatsxleroy2010-05-098-231/+261
* Cleaned up handling of linker sections.xleroy2010-05-089-229/+385
* Improved coalescing heuristics based on Hailperin's paper.xleroy2010-05-081-32/+49
* Cosmetic: comments to mark expansions of some pseudoinstructions.xleroy2010-05-081-7/+17
* Updatexleroy2010-05-051-1/+24
* Strengthen chunktype inference and use it to remove some useless casts.xleroy2010-05-053-24/+142
* More theorems about sign and zero extensionsxleroy2010-05-051-0/+100
* Removed an ADMITTED that was unused, fortunatelyxleroy2010-05-051-2/+0
* Pretty-printers for RTL and LTL. Not yet well integrated.xleroy2010-05-024-0/+235
* Compute spill costs.xleroy2010-05-021-8/+92
* In compilation of Sassign, avoid systematic move from a fresh temp.xleroy2010-05-023-105/+211
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-027-5/+39
* Optimisation: addrsymbol + (expr + cst) and addrstack + (expr + cst).xleroy2010-05-022-0/+28
* ARM version of Machregsauxxleroy2010-05-012-0/+59
* More struct testsxleroy2010-04-171-1/+2
* __builtin_memcpy, continued.xleroy2010-04-177-20/+117
* Support __builtin_memcpy; use it for struct assignmentxleroy2010-04-175-30/+93
* Update for 1.7.1v1.7.1xleroy2010-04-131-0/+17
* PowerPC: xleroy2010-04-103-3/+32
* Coloring: allow to exclude user-specified registers from allocation.xleroy2010-04-105-28/+131
* Test bit field of size 32xleroy2010-04-093-1/+18
* Bug fix: infinite loop in cparser/ on bit field of size 32 bits.xleroy2010-04-0910-59/+53
* Static initialization of structs with bitfieldsxleroy2010-04-073-1/+109
* Wrong type for __builtin_volatile_*_int32xleroy2010-04-021-1/+1
* In cparser/SimplExpr.ml:xleroy2010-04-024-12/+30
* cparser/AddCasts.ml: forgot to materialize cast at return statement.xleroy2010-04-014-13/+29
* Updates for release 1.7v1.7xleroy2010-03-302-9/+64
* Update for 1.7xleroy2010-03-302-2/+8
* Determine endianness at run-timexleroy2010-03-301-21/+23
* Options -I -D -U with a spacexleroy2010-03-301-0/+3
* Updated Linux conventionsxleroy2010-03-301-3/+6
* Cleaner generation of .dependxleroy2010-03-302-69/+65
* Include targets of preference edges in all_interf_regs. Not needed for corre...xleroy2010-03-301-6/+8
* Pretty stringsxleroy2010-03-291-3/+8
* Extra volatile testxleroy2010-03-283-1/+45
* More resistant proofxleroy2010-03-281-1/+0
* Prettier printing of configurationxleroy2010-03-281-1/+2
* Updated ARM asm printerxleroy2010-03-281-4/+67
* Typoxleroy2010-03-281-1/+0
* Emit a few comments to help reading the generated asmxleroy2010-03-281-10/+16
generated by cgit (git 2.34.1) at 2024-06-03 00:22:46 +0000