aboutsummaryrefslogtreecommitdiffstats
path: root/test
Commit message (Collapse)AuthorAgeFilesLines
* FIXME: Jumptables have linking issues.David Monniaux2019-03-293-0/+1241
|
* Merge branch 'mppa_k1c' of ↵David Monniaux2019-03-291-8/+8
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul
| * Merge branch 'mppa-mul' into mppa_k0cDavid Monniaux2019-03-2921-1082/+1916
| |\
| * | rm rules that conflictDavid Monniaux2019-03-291-8/+8
| | |
* | | Merge remote-tracking branch 'origin/mppa_k1c' into mppa-mulDavid Monniaux2019-03-291-1/+1
|\| |
| * | use C99 modeDavid Monniaux2019-03-291-1/+1
| | |
| * | for testing with questDavid Monniaux2019-03-221-0/+24
| | |
| * | check that gcc and ccomp compiled k1c code return the sameDavid Monniaux2019-03-221-2/+6
| | |
| * | improved testingDavid Monniaux2019-03-221-5/+16
| | |
| * | uses yarpgen random generatorDavid Monniaux2019-03-221-0/+37
| | |
| * | some more testingDavid Monniaux2019-03-221-1/+1
| | |
* | | missing config.hDavid Monniaux2019-03-291-0/+3
| | |
* | | Makefile for picosatDavid Monniaux2019-03-293-62/+0
| |/ |/|
* | ocaml benchmarkDavid Monniaux2019-03-283-8/+22
| |
* | MakefileDavid Monniaux2019-03-285-1025/+35
| |
* | NDEBUGDavid Monniaux2019-03-281-0/+6
| |
* | some more inlineDavid Monniaux2019-03-282-12/+13
| |
* | add some INLINE markersDavid Monniaux2019-03-281-36/+38
| |
* | picosat now uses the same Makefile system as the restDavid Monniaux2019-03-283-3/+49
| | | | | | | | we are 27% slower than gcc
* | some more ternaryDavid Monniaux2019-03-241-6/+6
| |
* | experiments with ternary operatorDavid Monniaux2019-03-241-1/+6
| |
* | experiments with ternaryDavid Monniaux2019-03-244-1526/+36
| |
* | another ternary implementationDavid Monniaux2019-03-241-1/+7
| |
* | demo ternary opDavid Monniaux2019-03-242-0/+49
| |
* | mysteriously slow codeDavid Monniaux2019-03-242-0/+70
| |
* | encore un essai de creduceDavid Monniaux2019-03-233-0/+1561
| |
* | system for comparing speedsDavid Monniaux2019-03-231-0/+12
| |
* | bitsliced AES in one fileDavid Monniaux2019-03-231-10/+85
| |
* | Test in one file only.David Monniaux2019-03-231-0/+1467
| |
* | for testing with questDavid Monniaux2019-03-221-0/+24
| |
* | check that gcc and ccomp compiled k1c code return the sameDavid Monniaux2019-03-221-2/+6
| |
* | improved testingDavid Monniaux2019-03-221-5/+16
| |
* | some more testingDavid Monniaux2019-03-221-1/+1
| |
* | uses yarpgen random generatorDavid Monniaux2019-03-221-0/+37
|/
* Merge branch 'mppa-mul' of ↵David Monniaux2019-03-2285-17/+259
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul
| * Rajout de tests test/mppa pour division/moduloCyril SIX2019-03-226-0/+34
| |
| * Merge branch 'mppa_postpass' into mppa-mulCyril SIX2019-03-2282-30/+238
| |\
| | * Reorganized the test/mppa/ tests to have fewer of themCyril SIX2019-03-2282-30/+238
| | |
* | | better patch for running the test suiteDavid Monniaux2019-03-221-0/+13
| | |
* | | Now we have division, simplify the patch.David Monniaux2019-03-221-50/+0
|/ /
* | csmith for testingDavid Monniaux2019-03-201-0/+23
| |
* | Makefile for ocamlrun testingDavid Monniaux2019-03-201-0/+7
| |
* | ocaml byterunner exampleDavid Monniaux2019-03-20119-0/+45174
| |
* | rm need for gccDavid Monniaux2019-03-202-4/+2
| |
* | use the original source codesDavid Monniaux2019-03-2030-5528/+5235
| |
* | picomus compile aussiDavid Monniaux2019-03-201-1/+1
| |
* | picosat fonctionneDavid Monniaux2019-03-202-3/+7
| |
* | vire des scories INT_DIV et INT_MODDavid Monniaux2019-03-205-6/+6
|/
* Merge branch 'mppa-madd' into mppa_postpassDavid Monniaux2019-03-202-5/+21
|\
| * maddl / maddlim are synthesized (but not for pointers it seems)David Monniaux2019-03-202-5/+21
| |
generated by cgit (git 2.34.1) at 2024-07-12 11:47:43 +0000