aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Rajout d'opérateurs flottants, travail sur les tests --> à continuerCyril SIX2019-02-1575-182/+305
|
* FIX axiom to be realized issueCyril SIX2019-02-152-2/+35
|
* Generalizing state' in PostpassSchedulingCyril SIX2019-02-141-32/+23
|
* More lemmas in PostpassSchedulingCyril SIX2019-02-141-6/+26
|
* Some more lemma proving in PostpassSchedulingCyril SIX2019-02-141-10/+73
|
* Proving verify_schedule_correct with axiomsCyril SIX2019-02-142-17/+132
|
* HAS_FLOAT (constantes)David Monniaux2019-02-131-0/+1
|
* Merge branch 'mppa_postpass' of ↵David Monniaux2019-02-1335-121/+5073
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Added AbstractBasicBlock files to the Coq build processCyril SIX2019-02-1326-4/+4698
| |
| * Added Olongoffloat, Ofloatoflong and doubleconv testCyril SIX2019-02-126-3/+34
| |
| * Added Ointofsingle + floatconv unit testCyril SIX2019-02-127-6/+26
| |
| * 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 ↵David Monniaux2019-02-131-1/+1
|/ | | | constrain this limit.
* for mbedtlsDavid Monniaux2019-02-093-0/+114
|
* some more files compileDavid Monniaux2019-02-081-7/+9
|
* Fix for immediate size miscomputation in postpass oracle.Cyril SIX2019-02-081-12/+11
|
* removed 'KILL_TAIL_CALL()', no longer neededDavid Monniaux2019-02-0826-39/+2
|
* Merge branch 'mppa_postpass' of ↵David Monniaux2019-02-0810-24/+105
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Added indirect tailcallsCyril SIX2019-02-088-6/+87
| |
| * Réactivé l'optim mulhs pour 32-bits (Omulhs n'est jamais généré)Cyril SIX2019-02-082-16/+16
| |
| * Désactivé toutes les optim division par constante --> Omulhs etc..Cyril SIX2019-02-082-26/+26
| |
| * Desactivated Omulhs 32-bits optimization (division by constant)Cyril SIX2019-02-082-8/+8
| |
* | Merge branch 'mppa_postpass' of ↵David Monniaux2019-02-082-17/+24
|\| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * OshrxlimmCyril SIX2019-02-082-17/+24
| |
* | Merge branch 'mppa_postpass' of ↵David Monniaux2019-02-082-82/+67
|\| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Un peu de refactorisationCyril SIX2019-02-072-82/+67
| |
* | nft -> nttDavid Monniaux2019-02-072-7/+7
|/
* -g in C FLAGSDavid Monniaux2019-02-071-4/+7
|
* fix rulesDavid Monniaux2019-02-071-8/+8
|
* number theoretic transform (FFT in finite field)David Monniaux2019-02-072-0/+172
|
* float aussiDavid Monniaux2019-02-063-3/+17
|
* and now a call to lrintDavid Monniaux2019-02-061-2/+2
|
* test for float/double parameter passingDavid Monniaux2019-02-064-0/+40
|
* Makefiles now use rules.mk, and added a prohibition of unprototyped functionsDavid Monniaux2019-02-067-66/+21
|
* Better fix for register allocation?Cyril SIX2019-02-061-3/+4
|
* simplification des MakefileDavid Monniaux2019-02-058-179/+75
|
* streamlining the MakefileDavid Monniaux2019-02-051-0/+1
|
* regular MakefilesDavid Monniaux2019-02-053-67/+45
|
* Merge branch 'mppa_postpass' of ↵David Monniaux2019-02-054-53/+46
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Removing the low_half axiomCyril SIX2019-02-054-53/+46
| |
* | comparisons all aroundDavid Monniaux2019-02-051-4/+18
|/
* IDEA encryptionDavid Monniaux2019-02-053-0/+490
|
* Fix pour le register allocationCyril SIX2019-02-051-2/+2
|
* spill queue complaintsDavid Monniaux2019-02-041-0/+5
|
generated by cgit (git 2.34.1) at 2024-07-12 02:42:33 +0000