aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-094-15/+6
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-282-4/+4
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...xleroy2010-10-2713-64/+53
* Typo in doc commentxleroy2010-09-211-2/+2
* Merge of the reuse-temps branch:xleroy2010-09-0224-275/+637
* Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_extxleroy2010-08-211-3/+5
* Nettoyages pour docxleroy2010-08-181-1/+1
* Merge of branches/full-expr-4:xleroy2010-08-189-168/+1404
* Forgot to add this file. Part of the refactoring of $ARCH/$SYSTEM/Conventions.vxleroy2010-07-071-0/+251
* Support for inlined built-ins.xleroy2010-06-2948-210/+574
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-281-0/+1
* Updated Caml parts to match new representation for global variables.xleroy2010-05-261-1/+2
* More faithful semantics for volatile reads and writes.xleroy2010-05-2319-25/+90
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-1020-16/+29
* Improved coalescing heuristics based on Hailperin's paper.xleroy2010-05-081-32/+49
* Removed an ADMITTED that was unused, fortunatelyxleroy2010-05-051-2/+0
* Pretty-printers for RTL and LTL. Not yet well integrated.xleroy2010-05-022-0/+228
* Compute spill costs.xleroy2010-05-021-8/+92
* In compilation of Sassign, avoid systematic move from a fresh temp.xleroy2010-05-023-105/+211
* Coloring: allow to exclude user-specified registers from allocation.xleroy2010-04-102-25/+42
* Include targets of preference edges in all_interf_regs. Not needed for corre...xleroy2010-03-301-6/+8
* More resistant proofxleroy2010-03-281-1/+0
* Restored the big-step semantics for Cminorxleroy2010-03-111-125/+125
* Merge of the newmem and newextcalls branches:xleroy2010-03-0730-842/+951
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-031-5/+7
* Backtracking on commit 1220v1.6xleroy2010-01-1341-23329/+14
* ajout branche allocation de registresblazy2010-01-0841-14/+23329
* MAJ extraction after changes in Integersxleroy2009-12-161-1/+1
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-192-6/+6
* More realistic treatment of jump tables: show the absence of overflow when ac...xleroy2009-11-106-3/+13
* Added support for jump tables in back end.xleroy2009-11-1040-88/+380
* Coloringaux: make identifiers unique; special treatment of precolored xleroy2009-08-261-60/+132
* Forgot to add some filesxleroy2009-08-182-0/+717
* "val_match_approx_increasing" moved from mach-dep part to mach-indep part.xleroy2009-08-181-0/+11
* Refactoring of Constprop and Constpropproof into a machine-dependent part and...xleroy2009-08-172-0/+680
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...xleroy2009-08-171-0/+122
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-1614-349/+346
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-162-26/+34
* Update spill costs when coalescingxleroy2009-08-161-2/+3
* Added 'going wrong' behaviorsxleroy2009-08-0511-165/+167
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-23/+17
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-0526-229/+168
* Added tail call optimization passxleroy2009-03-263-6/+847
* New linearization heuristicxleroy2009-02-271-32/+72
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...xleroy2009-01-294-10/+6
* Elimination of "alloc" instruction in Caml files and test files.xleroy2009-01-115-24/+0
* - Added alignment constraints to memory loads and stores.xleroy2009-01-1138-537/+137
* Fixed unary minusxleroy2009-01-071-1/+1
* Cminor, CminorSel: removed useless premises in rules for Sreturnxleroy2009-01-042-4/+0
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-3032-11274/+2075
generated by cgit (git 2.34.1) at 2024-06-12 15:55:49 +0000