aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Harden proof script against empty destroyed_at_movexleroy2011-08-221-7/+6
* New backend pass "RRE": optimize (somewhat) redundant reloads introduced by t...xleroy2011-08-164-20/+926
* Locations.v: add Loc.diff_dec.xleroy2011-08-141-0/+9
* IA32 port: more faithful treatment of pseudoregister ST0.xleroy2011-08-087-142/+272
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-1519-134/+125
* Coloringaux: better cost estimate for annotation builtinsxleroy2011-06-141-0/+2
* Add preference for annot_val builtinxleroy2011-06-142-4/+21
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-1322-76/+231
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).xleroy2011-05-083-5/+133
* Added pass CleanupLabels to remove unreferenced labels in a proved way.xleroy2011-05-083-0/+471
* Renamed Machconcr into Machsem.xleroy2011-04-095-1513/+16
* Merge of branch "unsigned-offsets":xleroy2011-04-0929-1359/+2115
* 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