aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* remove cruftDavid Monniaux2019-01-306-6/+6
|
* remove cruft dealing with __int128 and __threadDavid Monniaux2019-01-3011-291/+9
|
* no need for modulo and divisionDavid Monniaux2019-01-302-13/+1
|
* pour ne plus être embêtés avec le int128David Monniaux2019-01-301-1/+1
|
* no __SIZEOF_INT128__David Monniaux2019-01-301-1/+1
| | | | J'avais fait une erreur, les __SSE__ c'était quand je compilais sur x86.
* Merge branch 'mppa_postpass' of ↵David Monniaux2019-01-301-13/+57
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Rajouté des erreurs plus explicites dans Asmblockgen.vCyril SIX2019-01-301-13/+57
| |
* | remove preprocessor directives about SIZE_TYPE, now useless (long is now 8 ↵David Monniaux2019-01-309-8/+14
| | | | | | | | bytes like in gcc)
* | sizeof checkDavid Monniaux2019-01-301-0/+46
|/
* Rajouté -U__SSE__ -U__SSE2__ dans le ./configure pour le K1Cyril SIX2019-01-301-1/+1
|
* long types are 8 bytes nowCyril SIX2019-01-301-0/+1
|
* same format as the othersDavid Monniaux2019-01-302-10/+44
|
* bitsliced TEA from archived ↵David Monniaux2019-01-306-0/+663
| | | | http://plaintext.crypto.lo.gy/article/378/untwisted-bit-sliced-tea-time
* correct path to ccompDavid Monniaux2019-01-301-1/+1
|
* https://github.com/conorpp/bitsliced-aesDavid Monniaux2019-01-3015-0/+1920
|
* fixes in makefilesDavid Monniaux2019-01-303-39/+6
|
* synchronized with David's scheduling workDavid Monniaux2019-01-302-37/+249
|
* the state of things that workDavid Monniaux2019-01-301-2/+4
|
* blowfishDavid Monniaux2019-01-302-2/+15
|
* remove workaroundDavid Monniaux2019-01-301-4/+0
|
* no need for this anymoreDavid Monniaux2019-01-292-3/+1
|
* https://github.com/pfalcon/uzlibDavid Monniaux2019-01-29274-0/+3695
|
* muf muf mufDavid Monniaux2019-01-297-15/+21
|
* jpeg-6b modifiedDavid Monniaux2019-01-29157-0/+63909
|
* give meaningful "unhandled instr" messagesDavid Monniaux2019-01-291-11/+7
|
* Merge branch 'mppa_postpass' of ↵David Monniaux2019-01-299-78/+258
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Adding indirect calls (icall instruction)Cyril SIX2019-01-297-7/+69
| |
| * Hypothèses de pc_set_add permettant de prouver le lemmeCyril SIX2019-01-291-19/+26
| |
| * Avancement sur exec_basic_instr_pcvar + exec_load et exec_store prennent des ↵Cyril SIX2019-01-293-68/+179
| | | | | | | | ireg au lieu de preg
* | ça makeDavid Monniaux2019-01-291-6/+11
|/
* crypto algorithms from https://github.com/B-Con/crypto-algorithms/David Monniaux2019-01-2832-0/+3731
|
* give meaningful messages pleaseDavid Monniaux2019-01-271-2/+12
|
* packagedDavid Monniaux2019-01-278-571/+20579
|
* picosatDavid Monniaux2019-01-2717-0/+12288
| | | | induces bug in register allocation
* to testDavid Monniaux2019-01-261-0/+6
|
* clock cycles etc.David Monniaux2019-01-263-6/+13
|
* micro bunzipDavid Monniaux2019-01-265-20/+60
|
* micro bunzipDavid Monniaux2019-01-262-0/+540
|
* Merge branch 'mppa_postpass' of ↵David Monniaux2019-01-251-6/+110
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Avancement PostpassSchedulingproofCyril SIX2019-01-251-5/+69
| |
| * Merge branch 'mppa_postpass' of ↵Cyril SIX2019-01-251-7/+64
| |\ | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass Conflicts: mppa_k1c/PostpassSchedulingproof.v
| | * Progrès dans PostpassSchedulingproofCyril SIX2019-01-251-6/+46
| | |
| * | Preuve de app_nonil2 dans PostpassSchedulingproofCyril SIX2019-01-231-4/+5
| | |
* | | Merge branch 'mppa_postpass' of ↵David Monniaux2019-01-241-9/+27
|\ \ \ | | |/ | |/| | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * | Un peu d'avancement sur PostpassSchedulingproofCyril SIX2019-01-241-9/+27
| |/
* | Merge branch 'mppa_postpass' of ↵David Monniaux2019-01-233-126/+208
|\| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Cleaning dans PostpassSchedulingproofCyril SIX2019-01-231-43/+20
| |
| * 3ème cas de transf_step_correct de PostpassSchedulingproof finiCyril SIX2019-01-231-5/+6
| |
| * Proof of builtin case for transf_step_correct in PostpassSchedulingproofCyril SIX2019-01-231-1/+25
| |
| * Adding a predicate that a builtin must be alone in its basicblockCyril SIX2019-01-233-88/+168
| |
generated by cgit (git 2.34.1) at 2024-07-11 23:20:36 +0000