aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Minor updatesxleroy2012-03-111-1/+0
* Proof didn't go through for ARMxleroy2012-03-111-2/+2
* Another update from Andrew Tolmachxleroy2012-03-091-1/+1
* PrintCminor: printing Sskipxleroy2012-03-091-1/+1
* Merge of Andrew Tolmach's HASP-related changesxleroy2012-03-094-20/+120
* Take advantage of Cmaskzero and Cmasknotzero.xleroy2012-02-242-11/+14
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-232-224/+357
* Merge of the "volatile" branch:xleroy2012-02-046-2/+66
* powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a cert...xleroy2012-01-211-11/+28
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-152-3/+10
* Merge of the nonstrict-ops branch:xleroy2012-01-1416-1300/+570
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-188-24/+23
* 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
generated by cgit (git 2.34.1) at 2024-06-02 15:36:46 +0000