aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/SelectOpproof.v
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-2/+3
|\
| * [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-161-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
* | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-201-2/+2
|/ | | | mppa-work-upstream-merge
* fma with first negated operandDavid Monniaux2019-08-301-6/+14
|
* fmaDavid Monniaux2019-08-301-3/+50
|
* use finvwDavid Monniaux2019-08-301-1/+30
|
* fmin/fmax/fminf/fmaxf non bien testésDavid Monniaux2019-08-291-1/+3
|
* various fixesDavid Monniaux2019-07-191-0/+15
|
* move with immediatesDavid Monniaux2019-06-041-1/+27
|
* osel immDavid Monniaux2019-06-041-11/+8
|
* shortcut cmove worksDavid Monniaux2019-06-041-69/+0
|
* why doesn't it work?David Monniaux2019-06-041-6/+222
|
* start to have whole path if-conversion?David Monniaux2019-06-041-1/+13
|
* rm old select/selectl/selectf/selectfsDavid Monniaux2019-06-031-79/+18
|
* Merge remote-tracking branch 'origin/mppa-msub' into mppa-workDavid Monniaux2019-05-301-1/+152
|\ | | | | | | | | Conflicts: mppa_k1c/ExtValues.v
| * 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
|
generated by cgit (git 2.34.1) at 2024-07-12 02:39:03 +0000