aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
...
* Proving verify_schedule_correct with axiomsCyril SIX2019-02-142-17/+132
* Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-02-1332-117/+5049
|\
| * Added AbstractBasicBlock files to the Coq build processCyril SIX2019-02-1325-0/+4692
| * Added Olongoffloat, Ofloatoflong and doubleconv testCyril SIX2019-02-125-3/+25
| * Added Ointofsingle + floatconv unit testCyril SIX2019-02-126-6/+17
| * Added OsingleofintCyril SIX2019-02-126-16/+28
| * Added Pmakefs and Pmakef to the schedulerCyril SIX2019-02-121-3/+9
| * Added Ofloatconst and Osingleconst (not integrated in scheduler yet)Cyril SIX2019-02-125-10/+53
| * Minor refactorizationCyril SIX2019-02-122-12/+12
| * Proof of axiom verified_schedule_headerCyril SIX2019-02-122-59/+133
| * Proving the axiom verified_schedule_single_instCyril SIX2019-02-122-5/+35
| * Proving verified_schedule_size axiomCyril SIX2019-02-112-16/+58
* | We have one example that exceeds a total latency of 5000, better simply not c...David Monniaux2019-02-131-1/+1
|/
* Fix for immediate size miscomputation in postpass oracle.Cyril SIX2019-02-081-12/+11
* Added indirect tailcallsCyril SIX2019-02-086-6/+38
* OshrxlimmCyril SIX2019-02-082-17/+24
* Un peu de refactorisationCyril SIX2019-02-072-82/+67
* Removing the low_half axiomCyril SIX2019-02-054-53/+46
* Fix pour le register allocationCyril SIX2019-02-051-2/+2
* Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-02-041-22/+152
|\
| * Preuves (en dehors du verified_schedule) terminées dans PostpassSchedulingproofCyril SIX2019-02-041-6/+44
| * Proof of transf_exec_control \o/Cyril SIX2019-02-041-2/+5
| * Proof of label_pos related things in PostpassSchedulingproofCyril SIX2019-02-041-15/+104
* | commentDavid Monniaux2019-02-021-0/+1
|/
* new version of the scheduler, interface to GurobiDavid Monniaux2019-02-012-37/+96
* Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-02-011-10/+137
|\
| * Encore de la tuyauterieCyril SIX2019-02-011-1/+91
| * Proof of transf_blocks_verifiedCyril SIX2019-02-011-9/+46
* | Ugly hack to get at the k1c standard library stdin/stdout/stderrDavid Monniaux2019-02-011-1/+6
|/
* implemented builtin memcpyDavid Monniaux2019-02-014-98/+56
* Décomposition de transf_find_bblock en lemmesCyril SIX2019-01-311-1/+22
* Adding a "check_size" in concat2Cyril SIX2019-01-311-13/+30
* idee de refactoringSylvain Boulmé2019-01-311-24/+54
* Rajouté des erreurs plus explicites dans Asmblockgen.vCyril SIX2019-01-301-13/+57
* synchronized with David's scheduling workDavid Monniaux2019-01-302-37/+249
* give meaningful "unhandled instr" messagesDavid Monniaux2019-01-291-11/+7
* Adding indirect calls (icall instruction)Cyril SIX2019-01-296-7/+36
* 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
* give meaningful messages pleaseDavid Monniaux2019-01-271-2/+12
* Avancement PostpassSchedulingproofCyril SIX2019-01-251-5/+69
* Progrès dans PostpassSchedulingproofCyril SIX2019-01-251-6/+46
* Un peu d'avancement sur PostpassSchedulingproofCyril SIX2019-01-241-9/+27
* 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
* Changement de modèle de preuve pour le 1er cas du tranf_step_correct de Post...Cyril SIX2019-01-231-14/+47
* Léger avancement PostpassSchedulingproof.vCyril SIX2019-01-221-1/+7
* Added sxwd and zxwd supportCyril SIX2019-01-227-36/+30
generated by cgit (git 2.34.1) at 2024-07-12 06:55:03 +0000