Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 |
| | | |||||
| * | some unrolling | David Monniaux | 2019-01-18 | 4 | -3/+47 |
| | | |||||
| * | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-01-18 | 1 | -1/+1 |
| |\ | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * | | fix free() bug | David Monniaux | 2019-01-18 | 1 | -0/+2 |
| | | |