aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* a couple "Admitted" and the Coq compilesDavid Monniaux2019-09-081-12/+18
* moving forward with notrapDavid Monniaux2019-09-081-22/+10
* furtherDavid Monniaux2019-09-081-3/+20
* moving forward on K1CDavid Monniaux2019-09-078-171/+200
* fix for Risc-VDavid Monniaux2019-09-074-8/+34
* PowerPC compilesDavid Monniaux2019-09-076-22/+104
* fixes for compiling on other platformsDavid Monniaux2019-09-074-8/+8
* fixes for ARMDavid Monniaux2019-09-079-42/+86
* notrap works on x86David Monniaux2019-09-071-12/+3
* more for passing notrap through x86David Monniaux2019-09-076-12/+66
* for nontrapDavid Monniaux2019-09-061-0/+28
* ONE "admitted" and things compileDavid Monniaux2019-09-0612-46/+87
* progress in proofDavid Monniaux2019-09-051-14/+27
* BSload notrap1David Monniaux2019-09-051-1/+19
* moving forward with proofsDavid Monniaux2019-09-052-29/+29
* more stuff on non trapping loadsDavid Monniaux2019-09-051-0/+8
* more proofsDavid Monniaux2019-09-052-0/+52
* more on notrapDavid Monniaux2019-09-057-24/+75
* more proofDavid Monniaux2019-09-051-0/+16
* some more proofs on notrapDavid Monniaux2019-09-051-0/+12
* more proofs going throughDavid Monniaux2019-09-0511-26/+99
* LinearizeProof for non trapping loadsDavid Monniaux2019-09-051-16/+32
* CSEproof for non trapping loadsDavid Monniaux2019-09-053-19/+89
* going forwardDavid Monniaux2019-09-041-41/+50
* stuck in CSEproofDavid Monniaux2019-09-041-1/+10
* ca avanceDavid Monniaux2019-09-041-2/+11
* begin CSE proof for notrap loadDavid Monniaux2019-09-041-3/+85
* begin CSEDavid Monniaux2019-09-044-18/+23
* moved trapping_mode to a more appropriate placeDavid Monniaux2019-09-032-2/+9
* Dead code proof for non trapping loadsDavid Monniaux2019-09-031-0/+77
* forgot this functionDavid Monniaux2019-09-031-2/+0
* finished Constopproof for non trapping loadsDavid Monniaux2019-09-031-1/+41
* advancing in constant propagationDavid Monniaux2019-09-032-2/+22
* Value analysis for non trapping loadsDavid Monniaux2019-09-033-4/+58
* Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-032-4/+3
|\
| * compatibility with OCaml 4.08David Monniaux2019-09-032-4/+3
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-03180-6367/+6667
|\|
| * Fixing upstream merge buildCyril SIX2019-09-031-1/+1
| * aclrw testCyril SIX2019-09-031-0/+12
| * Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workCyril SIX2019-09-03177-6355/+6648
| |\
| | * macros for fma() fmaf()David Monniaux2019-08-302-0/+3
| | * fma with first negated operandDavid Monniaux2019-08-303-6/+17
| | * fmaDavid Monniaux2019-08-3014-15/+166
| | * début du fmaDavid Monniaux2019-08-304-7/+179
| | * use finvwDavid Monniaux2019-08-303-4/+45
| | * add finvw ; not yet generatedDavid Monniaux2019-08-3011-6/+55
| | * fabsfDavid Monniaux2019-08-293-1/+10
| | * fmin/fmax/fminf/fmaxf non bien testésDavid Monniaux2019-08-2912-11/+102
| | * begin implementing minf/maxfDavid Monniaux2019-08-295-11/+128
| | * merge upstream including fma fixesDavid Monniaux2019-08-2825-1942/+0
generated by cgit (git 2.34.1) at 2024-07-14 06:15:00 +0000