aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Backtracking on commit 1220v1.6xleroy2010-01-1345-23334/+27
* MAJ release 1.6xleroy2010-01-121-8/+5
* MAJ Changesxleroy2010-01-121-1/+1
* ajout branche allocation de registresblazy2010-01-0841-14/+23329
* Test result more reproduciblexleroy2009-12-162-2/+2
* MAJ extraction after changes in Integersxleroy2009-12-162-3/+4
* MAJ Changesxleroy2009-12-162-2/+14
* 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
generated by cgit (git 2.34.1) at 2024-05-20 11:00:28 +0000