aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Last updates for release 1.5.v1.5xleroy2009-08-283-20/+28
* Updated for release 1.5xleroy2009-08-272-2/+33
* Remove "-ccopt -g" options: not really useful and causing problems with flexd...xleroy2009-08-271-2/+2
* Coloringaux: make identifiers unique; special treatment of precolored xleroy2009-08-265-126/+266
* Typo in docxleroy2009-08-261-1/+1
* Stronger constant folding, esp. w.r.t. floatsxleroy2009-08-213-40/+165
* In generated Cminor functions, make sure local variables includexleroy2009-08-202-23/+100
* Build bytecode version with debug symbols.xleroy2009-08-201-2/+2
* Updated Selectionxleroy2009-08-181-1/+1
* Declaration of use_fused_mul, unused in this port but needed for extraction (...xleroy2009-08-181-0/+4
* Forgot to add some filesxleroy2009-08-182-0/+717
* No '\n' in Coq strings...xleroy2009-08-183-4/+6
* "val_match_approx_increasing" moved from mach-dep part to mach-indep part.xleroy2009-08-183-22/+11
* Typo docxleroy2009-08-171-1/+1
* Refactoring of Constprop and Constpropproof into a machine-dependent part and...xleroy2009-08-178-1327/+776
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...xleroy2009-08-178-1548/+325
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-1624-523/+608
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-1610-657/+916
* Unionfind data structure, used in new implementation of backend/Tunnelingxleroy2009-08-161-0/+702
* Update spill costs when coalescingxleroy2009-08-161-2/+3
* Added 'going wrong' behaviorsxleroy2009-08-0526-273/+449
* Transition semantics for Clight and Csharpminorxleroy2009-08-0311-2365/+3013
* Use Extraction Blacklistxleroy2009-07-254-21/+7
* MAJxleroy2009-07-151-11/+12
* message macosx en accord avec configureblazy2009-06-051-1/+1
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-0571-852/+795
* Various clean-upsv1.4xleroy2009-04-179-75/+61
* Use Configuration.systemxleroy2009-03-291-28/+38
* Update creation Configuration.mlxleroy2009-03-291-1/+2
* cil.patch dir now uselessxleroy2009-03-290-0/+0
* Cleaned up configure script.xleroy2009-03-29296-1356/+82317
* Bug with overflow in line numbersxleroy2009-03-291-0/+24
* Honor "static" modifier on C globals.xleroy2009-03-283-32/+104
* Updatexleroy2009-03-261-0/+25
* Added tail call optimization passxleroy2009-03-269-9/+889
* Optimize redundant casts after memory loadsxleroy2009-02-272-0/+58
* New linearization heuristicxleroy2009-02-271-32/+72
* make install: ./ccomp au lieu de ../ccompblazy2009-02-271-1/+2
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...xleroy2009-02-2610-39/+156
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...xleroy2009-01-2911-34/+25
* Elimination of "alloc" instruction in Caml files and test files.xleroy2009-01-118-30/+4
* - Added alignment constraints to memory loads and stores.xleroy2009-01-1167-1488/+719
* Fixed unary minusxleroy2009-01-071-1/+1
* Test for int/float conversionsxleroy2009-01-073-1/+140
* Updatesxleroy2009-01-053-33/+58
* Endianness in testsxleroy2009-01-054-2/+20
* Cminor, CminorSel: removed useless premises in rules for Sreturnxleroy2009-01-044-8/+4
* Some cleanupsxleroy2009-01-021-1/+10
* Wrong dependenciesxleroy2009-01-021-4/+6
* Continuation of ARM port.xleroy2009-01-017-38/+1226