| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | ça make | David Monniaux | 2019-01-29 | 1 | -6/+11 |
| | | |||||
| * | crypto algorithms from https://github.com/B-Con/crypto-algorithms/ | David Monniaux | 2019-01-28 | 32 | -0/+3731 |
| | | |||||
| * | give meaningful messages please | David Monniaux | 2019-01-27 | 1 | -2/+12 |
| | | |||||
| * | packaged | David Monniaux | 2019-01-27 | 8 | -571/+20579 |
| | | |||||
| * | picosat | David Monniaux | 2019-01-27 | 17 | -0/+12288 |
| | | | | | induces bug in register allocation | ||||
| * | to test | David Monniaux | 2019-01-26 | 1 | -0/+6 |
| | | |||||
| * | clock cycles etc. | David Monniaux | 2019-01-26 | 3 | -6/+13 |
| | | |||||
| * | micro bunzip | David Monniaux | 2019-01-26 | 5 | -20/+60 |
| | | |||||
| * | micro bunzip | David Monniaux | 2019-01-26 | 2 | -0/+540 |
| | | |||||
| * | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-01-25 | 1 | -6/+110 |
| |\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| | * | Avancement PostpassSchedulingproof | Cyril SIX | 2019-01-25 | 1 | -5/+69 |
| | | | |||||
| | * | Merge branch 'mppa_postpass' of ↵ | Cyril SIX | 2019-01-25 | 1 | -7/+64 |
| | |\ | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass Conflicts: mppa_k1c/PostpassSchedulingproof.v | ||||
| | | * | Progrès dans PostpassSchedulingproof | Cyril SIX | 2019-01-25 | 1 | -6/+46 |
| | | | | |||||
| | * | | Preuve de app_nonil2 dans PostpassSchedulingproof | Cyril SIX | 2019-01-23 | 1 | -4/+5 |
| | | | | |||||
| * | | | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-01-24 | 1 | -9/+27 |
| |\ \ \ | | |/ | |/| | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| | * | | Un peu d'avancement sur PostpassSchedulingproof | Cyril SIX | 2019-01-24 | 1 | -9/+27 |
| | |/ | |||||
| * | | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-01-23 | 3 | -126/+208 |
| |\| | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| | * | Cleaning dans PostpassSchedulingproof | Cyril SIX | 2019-01-23 | 1 | -43/+20 |
| | | | |||||
| | * | 3ème cas de transf_step_correct de PostpassSchedulingproof fini | Cyril SIX | 2019-01-23 | 1 | -5/+6 |
| | | | |||||
| | * | Proof of builtin case for transf_step_correct in PostpassSchedulingproof | Cyril SIX | 2019-01-23 | 1 | -1/+25 |
| | | | |||||
| | * | Adding a predicate that a builtin must be alone in its basicblock | Cyril SIX | 2019-01-23 | 3 | -88/+168 |
| | | | |||||
| * | | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-01-23 | 1 | -14/+47 |
| |\| | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| | * | Merge branch 'mppa_postpass' of ↵ | Cyril SIX | 2019-01-23 | 3 | -9/+393 |
| | |\ | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| | * | | Changement de modèle de preuve pour le 1er cas du tranf_step_correct de ↵ | Cyril SIX | 2019-01-23 | 1 | -14/+47 |
| | | | | | | | | | | | | | PostpassSchedulingproof | ||||
| * | | | autoincrement | David Monniaux | 2019-01-22 | 1 | -1/+12 |
| | |/ |/| | |||||
| * | | to test memcpy one day | David Monniaux | 2019-01-22 | 1 | -1/+6 |
| | | | |||||
| * | | unroll loops | David Monniaux | 2019-01-22 | 1 | -0/+232 |
| | | | |||||
| * | | replace array[8] by 8 variables | David Monniaux | 2019-01-22 | 1 | -0/+103 |
| | | | |||||
| * | | correct measurement | David Monniaux | 2019-01-22 | 1 | -2/+17 |
| | | | |||||
| * | | sha-2 benchmark works | David Monniaux | 2019-01-22 | 1 | -3/+22 |
| | | | |||||
| * | | check malloc() return values | David Monniaux | 2019-01-22 | 1 | -3/+12 |
| | | | |||||
| * | | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-01-22 | 11 | -37/+58 |
| |\| | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| | * | Léger avancement PostpassSchedulingproof.v | Cyril SIX | 2019-01-22 | 1 | -1/+7 |
| | | | |||||
| | * | Added sxwd and zxwd support | Cyril SIX | 2019-01-22 | 10 | -36/+51 |
| | | | |||||
| * | | attribution | David Monniaux | 2019-01-22 | 1 | -0/+1 |
| |/ | |||||
| * | SHA-2 from https://github.com/amosnier/sha-2 | David Monniaux | 2019-01-22 | 6 | -0/+612 |
| | | |||||
| * | AES | David Monniaux | 2019-01-21 | 8 | -0/+1167 |
| | | |||||
| * | DES | David Monniaux | 2019-01-21 | 1 | -0/+500 |
| | | |||||
| * | Un poil d'avancement sur PostpassSchedulingproof.v. Corrections à faire sur ↵ | Cyril SIX | 2019-01-21 | 1 | -1/+47 |
| | | | | | le modèle | ||||
| * | some more example | David Monniaux | 2019-01-19 | 5 | -1/+128 |
| | | |||||
| * | use a prime in PRNG | David Monniaux | 2019-01-19 | 3 | -3/+3 |
| | | |||||
| * | quicksort | David Monniaux | 2019-01-19 | 6 | -27/+138 |
| | | |||||
| * | fixes in Makefile | David Monniaux | 2019-01-19 | 1 | -7/+1 |
| | | |||||
| * | fix Makefile | David Monniaux | 2019-01-18 | 1 | -2/+2 |
| | | |||||
| * | fix bug when using reoptimization (sat4j) | David Monniaux | 2019-01-18 | 1 | -9/+13 |
| | | |||||
| * | more on matrices | David Monniaux | 2019-01-18 | 3 | -5/+68 |
| | | |||||
| * | loop transformation | David Monniaux | 2019-01-18 | 3 | -2/+50 |
| | | |||||
| * | adjust path | David Monniaux | 2019-01-18 | 1 | -1/+1 |
| | | |||||
| * | Merge branch 'mppa_postpass' of ↵ | Cyril SIX | 2019-01-18 | 4 | -2/+84 |
| |\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| | * | moved to subdirectory | David Monniaux | 2019-01-18 | 4 | -1/+1 |
| | | | |||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |