| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | PPC64: revised generation of rldic* instructions | Xavier Leroy | 2021-10-28 | 1 | -15/+24 |
| * | Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructions | Xavier Leroy | 2020-12-06 | 1 | -17/+1 |
| * | Implement a `Osel` operation for PowerPC | Xavier Leroy | 2019-05-20 | 1 | -9/+34 |
| * | Remove coq warnings (#28) | Bernhard Schommer | 2017-09-22 | 1 | -1/+1 |
| * | Extend builtin arguments with a pointer addition operator, continued | Xavier Leroy | 2017-07-06 | 1 | -0/+23 |
| * | Hybrid 64bit/32bit PowerPC port | Bernhard Schommer | 2017-05-03 | 1 | -26/+252 |
| * | Replace 'decide equality' in powerpc/Op.v. Bug 21332 | Bernhard Schommer | 2017-04-03 | 1 | -4/+5 |
| * | Support for 64-bit architectures: update the PowerPC port | Xavier Leroy | 2016-10-01 | 1 | -74/+89 |
| * | bug 17392: remove trailing whitespace in source files | Michael Schmidt | 2015-10-14 | 1 | -29/+29 |
| * | Use PowerPC 64 bits instructions (when available) for int<->FP conversions. | Xavier Leroy | 2015-09-13 | 1 | -0/+16 |
| * | Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va... | Xavier Leroy | 2015-04-30 | 1 | -35/+35 |
| * | Ccompuimm now depends on the memory, this is needed to proof the Lemma op_dep... | Bernhard Schommer | 2015-04-02 | 1 | -2/+3 |
| * | Update PowerPC port. | Xavier Leroy | 2014-11-24 | 1 | -17/+39 |
| * | Merge of "newspilling" branch: | xleroy | 2014-07-23 | 1 | -90/+47 |
| * | Refactoring: move symbol_offset into Genv. | xleroy | 2014-05-24 | 1 | -21/+15 |
| * | Merge of branch value-analysis. | xleroy | 2013-12-20 | 1 | -4/+6 |
| * | powerpc/: new unary operation "addsymbol" | xleroy | 2013-11-17 | 1 | -3/+13 |
| * | Optimize integer divisions by positive constants, turning them into | xleroy | 2013-07-29 | 1 | -0/+10 |
| * | Merge of the "princeton" branch: | xleroy | 2013-06-16 | 1 | -2/+2 |
| * | Merge of the float32 branch: | xleroy | 2013-05-19 | 1 | -17/+4 |
| * | Coq-defined equality functions for Allocation. (continued) | xleroy | 2013-05-01 | 1 | -3/+10 |
| * | Big merge of the newregalloc-int64 branch. Lots of changes in two directions: | xleroy | 2013-04-20 | 1 | -10/+45 |
| * | Glasnost: making transparent a number of definitions that were opaque | xleroy | 2013-03-10 | 1 | -2/+4 |
| * | Pointers one past | xleroy | 2013-02-15 | 1 | -50/+34 |
| * | Updated PowerPC port to new integers. | xleroy | 2013-02-12 | 1 | -2/+1 |
| * | Ported to Coq 8.4pl1. Merge of branches/coq-8.4. | xleroy | 2013-01-29 | 1 | -8/+8 |
| * | Remove some useless "Require". | xleroy | 2012-12-30 | 1 | -1/+0 |
| * | Make min_int / -1 and min_int % -1 semantically undefined | xleroy | 2012-06-09 | 1 | -2/+5 |
| * | CSE: add recognition of some combined operators, conditions, and addressing m... | xleroy | 2012-05-26 | 1 | -13/+11 |
| * | PowerPC: remove the fmadd and fmsub operators/Asm instructions | xleroy | 2012-03-07 | 1 | -10/+0 |
| * | Improved instruction selection for "notint". | xleroy | 2012-02-24 | 1 | -0/+15 |
| * | More aggressive common subexpression elimination (CSE) of memory loads. | xleroy | 2012-02-23 | 1 | -0/+55 |
| * | Merge of the nonstrict-ops branch: | xleroy | 2012-01-14 | 1 | -660/+605 |
| * | Recognition of rlwimi instruction (useful for bitfield assignment) | xleroy | 2011-06-21 | 1 | -3/+12 |
| * | Merge of branch "unsigned-offsets": | xleroy | 2011-04-09 | 1 | -97/+230 |
| * | Float.intoffloat and Float.intuoffloat are now partial functions. | xleroy | 2010-10-28 | 1 | -1/+4 |
| * | Merge of the reuse-temps branch: | xleroy | 2010-09-02 | 1 | -15/+75 |
| * | Merge of the newmem and newextcalls branches: | xleroy | 2010-03-07 | 1 | -26/+15 |
| * | Revised lib/Integers.v to make it parametric w.r.t. word size. | xleroy | 2009-11-19 | 1 | -20/+20 |
| * | Adapted to work with Coq 8.2-1v1.4.1 | xleroy | 2009-06-05 | 1 | -12/+12 |
| * | - Added alignment constraints to memory loads and stores. | xleroy | 2009-01-11 | 1 | -118/+46 |
| * | Reorganized the development, modularizing away machine-dependent parts. | xleroy | 2008-12-30 | 1 | -0/+925 |
