Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Added indirect tailcalls | Cyril SIX | 2019-02-08 | 6 | -6/+38 |
| | |||||
* | Oshrxlimm | Cyril SIX | 2019-02-08 | 2 | -17/+24 |
| | |||||
* | Un peu de refactorisation | Cyril SIX | 2019-02-07 | 2 | -82/+67 |
| | |||||
* | Removing the low_half axiom | Cyril SIX | 2019-02-05 | 4 | -53/+46 |
| | |||||
* | Fix pour le register allocation | Cyril SIX | 2019-02-05 | 1 | -2/+2 |
| | |||||
* | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-02-04 | 1 | -22/+152 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * | Preuves (en dehors du verified_schedule) terminées dans PostpassSchedulingproof | Cyril SIX | 2019-02-04 | 1 | -6/+44 |
| | | |||||
| * | Proof of transf_exec_control \o/ | Cyril SIX | 2019-02-04 | 1 | -2/+5 |
| | | |||||
| * | Proof of label_pos related things in PostpassSchedulingproof | Cyril SIX | 2019-02-04 | 1 | -15/+104 |
| | | |||||
* | | comment | David Monniaux | 2019-02-02 | 1 | -0/+1 |
|/ | |||||
* | new version of the scheduler, interface to Gurobi | David Monniaux | 2019-02-01 | 2 | -37/+96 |
| | | | | | | | in jpeg-6b REOPTIMIZING SUCCEEDED 22 < 23 for 32 instructions REOPTIMIZING SUCCEEDED 81 < 83 for 139 instructions REOPTIMIZING SUCCEEDED 46 < 47 for 81 instructions | ||||
* | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-02-01 | 1 | -10/+137 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * | Encore de la tuyauterie | Cyril SIX | 2019-02-01 | 1 | -1/+91 |
| | | |||||
| * | Proof of transf_blocks_verified | Cyril SIX | 2019-02-01 | 1 | -9/+46 |
| | | |||||
* | | Ugly hack to get at the k1c standard library stdin/stdout/stderr | David Monniaux | 2019-02-01 | 1 | -1/+6 |
|/ | |||||
* | implemented builtin memcpy | David Monniaux | 2019-02-01 | 4 | -98/+56 |
| | |||||
* | Décomposition de transf_find_bblock en lemmes | Cyril SIX | 2019-01-31 | 1 | -1/+22 |
| | |||||
* | Adding a "check_size" in concat2 | Cyril SIX | 2019-01-31 | 1 | -13/+30 |
| | |||||
* | idee de refactoring | Sylvain Boulmé | 2019-01-31 | 1 | -24/+54 |
| | |||||
* | Rajouté des erreurs plus explicites dans Asmblockgen.v | Cyril SIX | 2019-01-30 | 1 | -13/+57 |
| | |||||
* | synchronized with David's scheduling work | David Monniaux | 2019-01-30 | 2 | -37/+249 |
| | |||||
* | give meaningful "unhandled instr" messages | David Monniaux | 2019-01-29 | 1 | -11/+7 |
| | |||||
* | Adding indirect calls (icall instruction) | Cyril SIX | 2019-01-29 | 6 | -7/+36 |
| | |||||
* | Hypothèses de pc_set_add permettant de prouver le lemme | Cyril SIX | 2019-01-29 | 1 | -19/+26 |
| | |||||
* | Avancement sur exec_basic_instr_pcvar + exec_load et exec_store prennent des ↵ | Cyril SIX | 2019-01-29 | 3 | -68/+179 |
| | | | | ireg au lieu de preg | ||||
* | give meaningful messages please | David Monniaux | 2019-01-27 | 1 | -2/+12 |
| | |||||
* | Avancement PostpassSchedulingproof | Cyril SIX | 2019-01-25 | 1 | -5/+69 |
| | |||||
* | Progrès dans PostpassSchedulingproof | Cyril SIX | 2019-01-25 | 1 | -6/+46 |
| | |||||
* | Un peu d'avancement sur PostpassSchedulingproof | Cyril SIX | 2019-01-24 | 1 | -9/+27 |
| | |||||
* | 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 |
| | |||||
* | Changement de modèle de preuve pour le 1er cas du tranf_step_correct de ↵ | Cyril SIX | 2019-01-23 | 1 | -14/+47 |
| | | | | PostpassSchedulingproof | ||||
* | Léger avancement PostpassSchedulingproof.v | Cyril SIX | 2019-01-22 | 1 | -1/+7 |
| | |||||
* | Added sxwd and zxwd support | Cyril SIX | 2019-01-22 | 7 | -36/+30 |
| | |||||
* | Un poil d'avancement sur PostpassSchedulingproof.v. Corrections à faire sur ↵ | Cyril SIX | 2019-01-21 | 1 | -1/+47 |
| | | | | le modèle | ||||
* | fix bug when using reoptimization (sat4j) | David Monniaux | 2019-01-18 | 1 | -9/+13 |
| | |||||
* | -O0 will not perform postpass scheduling | Cyril SIX | 2019-01-18 | 1 | -1/+1 |
| | |||||
* | Minor bug in encode_imm | Cyril SIX | 2019-01-18 | 1 | -2/+2 |
| | |||||
* | Minor bug fixes | Cyril SIX | 2019-01-17 | 1 | -2/+2 |
| | |||||
* | Ommited a ;; in va_arg_start macro | Cyril SIX | 2019-01-17 | 1 | -0/+1 |
| | |||||
* | Corrected a bug in Pallocframe expansion with va_args | Cyril SIX | 2019-01-17 | 2 | -3/+7 |
| | |||||
* | Merge corrections | Cyril SIX | 2019-01-17 | 2 | -74/+75 |
| | |||||
* | Merge branch 'mppa_k1c' into mppa_postpass | Cyril SIX | 2019-01-17 | 4 | -79/+80 |
|\ | |||||
| * | Added an error message for 32-bits division and modulo | Cyril SIX | 2018-12-11 | 1 | -13/+13 |
| | | |||||
| * | Fixed div64 and mod64 | Cyril SIX | 2018-12-11 | 1 | -0/+1 |
| | | |||||
| * | Fixed that fnegd and negd had been inverted | Cyril SIX | 2018-12-07 | 1 | -1/+1 |
| | | |||||
| * | Fixed bundles (back to 1 instruction per bundle) | Cyril SIX | 2018-12-07 | 1 | -65/+65 |
| | | |||||
* | | Corrected a bug in PostlassSchedulingOracle:intlist provoking cycles | Cyril SIX | 2019-01-17 | 1 | -1/+1 |
| | |