aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-1920-552/+652
* Added support for jump tables.xleroy2009-11-194-1/+87
* Unsupported: return/return type mismatchesxleroy2009-11-191-2/+17
* Cleaned up list_drop.xleroy2009-11-182-42/+37
* More realistic treatment of jump tables: show the absence of overflow when ac...xleroy2009-11-1012-25/+78
* Added support for jump tables in back end.xleroy2009-11-1049-145/+767
* PowerPC/EABI port: preliminary support for #pragma section andxleroy2009-11-0313-151/+337
* Use callee-save regs starting with R31/F31 and going down, like Diab doesxleroy2009-11-021-14/+14
* Simplified the treatment of the PowerPC small data area; now more specific to...xleroy2009-11-029-195/+151
* Preliminary support for small data area in PowerPC port.xleroy2009-11-019-96/+201
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-018-7/+49
* Storing of single floats: must insert frsp instruction before store. (Tempor...xleroy2009-10-304-16/+35
* Problem with MacOS X 10.6xleroy2009-10-251-1/+1
* Problem with const enum initializersxleroy2009-09-153-0/+6
* Updated for 1.5xleroy2009-09-151-0/+3
* 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
generated by cgit (git 2.34.1) at 2024-06-11 20:26:55 +0000