aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/SelectOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-msub' into mppa-workDavid Monniaux2019-05-301-1/+152
|\
| * correct -faddx option and propagate addim over addximDavid Monniaux2019-05-111-0/+5
| * option -faddx (off by default until questions cleared)David Monniaux2019-05-111-2/+29
| * apply .xs onto addx4 etcDavid Monniaux2019-05-111-11/+18
| * more maddxDavid Monniaux2019-05-111-0/+66
| * maddx ordre opposéDavid Monniaux2019-05-111-0/+4
| * add with shift, beginningDavid Monniaux2019-05-111-0/+36
| * Pmsub compiledDavid Monniaux2019-05-111-0/+6
* | 32-bit modulo now uses sign extend then call to the 64-bit functionDavid Monniaux2019-05-131-2/+18
* | we directly call 64-bit unsigned divisionDavid Monniaux2019-05-131-2/+18
|/
* command line options (still incomplete)David Monniaux2019-05-021-6/+13
* does not yet work, arity mismatchDavid Monniaux2019-05-011-0/+5
* float of int = float of long o long of intDavid Monniaux2019-04-291-3/+16
* float of intu = float of longu o longu of intuDavid Monniaux2019-04-291-3/+17
* more insf detectionDavid Monniaux2019-04-281-0/+31
* selection for insfDavid Monniaux2019-04-281-2/+20
* some more on bitfield detectionDavid Monniaux2019-04-281-1/+3
* some more on bit fields insert detectionDavid Monniaux2019-04-281-1/+2
* progress on bitfield detectionDavid Monniaux2019-04-281-1/+1
* detect insf case, beginDavid Monniaux2019-04-281-0/+1
* factor expressions into single fileDavid Monniaux2019-04-271-2/+2
* moved operators to specific file instead of common fileDavid Monniaux2019-04-271-4/+5
* simplify proof slightlyv3.5_k1c_1.1David Monniaux2019-04-251-20/+16
* progressDavid Monniaux2019-04-251-3/+35
* IT COMPILESDavid Monniaux2019-04-251-25/+28
* some progressDavid Monniaux2019-04-251-1/+5
* some more progressDavid Monniaux2019-04-251-1/+17
* some progress on bitfieldsDavid Monniaux2019-04-251-0/+9
* some more simplificationDavid Monniaux2019-04-121-0/+14
* some more simplificationDavid Monniaux2019-04-121-0/+6
* some more simplificationsDavid Monniaux2019-04-121-0/+6
* some more simplificationsDavid Monniaux2019-04-121-3/+19
* some more simplificationsDavid Monniaux2019-04-121-10/+11
* more simplificationsDavid Monniaux2019-04-121-0/+4
* some more progress on selectDavid Monniaux2019-04-041-26/+27
* prepare for conditions in cmoveDavid Monniaux2019-04-041-2/+2
* Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-031-0/+1
|\
| * Started to add addressing with register + register, Mach -> Asm not done yetCyril SIX2019-04-011-0/+1
* | ternary unsignedDavid Monniaux2019-03-261-0/+38
* | rm cruftDavid Monniaux2019-03-261-143/+9
* | ternary begins workingDavid Monniaux2019-03-261-8/+6
* | some progressDavid Monniaux2019-03-261-14/+8
* | implemented ternary patternDavid Monniaux2019-03-261-0/+46
* | more on ternaryDavid Monniaux2019-03-261-1/+144
|/
* restructuration pour compilation toute archiDavid Monniaux2019-03-221-1/+3
* ça recompile sur x86David Monniaux2019-03-221-65/+0
* Proof of div32/mod32/divf32/divf64 lemmasCyril SIX2019-03-201-6/+21
* la division flottante fonctionneDavid Monniaux2019-03-201-0/+16
* Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-201-6/+47
|\
| * Proving eval_divs_baseCyril SIX2019-03-201-6/+47
generated by cgit (git 2.34.1) at 2024-07-04 14:09:52 +0000