Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | FIXME: Jumptables have linking issues. | David Monniaux | 2019-03-29 | 3 | -0/+1241 |
| | |||||
* | Merge branch 'mppa_k1c' of ↵ | David Monniaux | 2019-03-29 | 1 | -8/+8 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul | ||||
| * | Merge branch 'mppa-mul' into mppa_k0c | David Monniaux | 2019-03-29 | 21 | -1082/+1916 |
| |\ | |||||
| * | | rm rules that conflict | David Monniaux | 2019-03-29 | 1 | -8/+8 |
| | | | |||||
* | | | Merge remote-tracking branch 'origin/mppa_k1c' into mppa-mul | David Monniaux | 2019-03-29 | 1 | -1/+1 |
|\| | | |||||
| * | | use C99 mode | David Monniaux | 2019-03-29 | 1 | -1/+1 |
| | | | |||||
| * | | for testing with quest | David Monniaux | 2019-03-22 | 1 | -0/+24 |
| | | | |||||
| * | | check that gcc and ccomp compiled k1c code return the same | David Monniaux | 2019-03-22 | 1 | -2/+6 |
| | | | |||||
| * | | improved testing | David Monniaux | 2019-03-22 | 1 | -5/+16 |
| | | | |||||
| * | | uses yarpgen random generator | David Monniaux | 2019-03-22 | 1 | -0/+37 |
| | | | |||||
| * | | some more testing | David Monniaux | 2019-03-22 | 1 | -1/+1 |
| | | | |||||
* | | | missing config.h | David Monniaux | 2019-03-29 | 1 | -0/+3 |
| | | | |||||
* | | | Makefile for picosat | David Monniaux | 2019-03-29 | 3 | -62/+0 |
| |/ |/| | |||||
* | | ocaml benchmark | David Monniaux | 2019-03-28 | 3 | -8/+22 |
| | | |||||
* | | Makefile | David Monniaux | 2019-03-28 | 5 | -1025/+35 |
| | | |||||
* | | NDEBUG | David Monniaux | 2019-03-28 | 1 | -0/+6 |
| | | |||||
* | | some more inline | David Monniaux | 2019-03-28 | 2 | -12/+13 |
| | | |||||
* | | add some INLINE markers | David Monniaux | 2019-03-28 | 1 | -36/+38 |
| | | |||||
* | | picosat now uses the same Makefile system as the rest | David Monniaux | 2019-03-28 | 3 | -3/+49 |
| | | | | | | | | we are 27% slower than gcc | ||||
* | | some more ternary | David Monniaux | 2019-03-24 | 1 | -6/+6 |
| | | |||||
* | | experiments with ternary operator | David Monniaux | 2019-03-24 | 1 | -1/+6 |
| | | |||||
* | | experiments with ternary | David Monniaux | 2019-03-24 | 4 | -1526/+36 |
| | | |||||
* | | another ternary implementation | David Monniaux | 2019-03-24 | 1 | -1/+7 |
| | | |||||
* | | demo ternary op | David Monniaux | 2019-03-24 | 2 | -0/+49 |
| | | |||||
* | | mysteriously slow code | David Monniaux | 2019-03-24 | 2 | -0/+70 |
| | | |||||
* | | encore un essai de creduce | David Monniaux | 2019-03-23 | 3 | -0/+1561 |
| | | |||||
* | | system for comparing speeds | David Monniaux | 2019-03-23 | 1 | -0/+12 |
| | | |||||
* | | bitsliced AES in one file | David Monniaux | 2019-03-23 | 1 | -10/+85 |
| | | |||||
* | | Test in one file only. | David Monniaux | 2019-03-23 | 1 | -0/+1467 |
| | | |||||
* | | for testing with quest | David Monniaux | 2019-03-22 | 1 | -0/+24 |
| | | |||||
* | | check that gcc and ccomp compiled k1c code return the same | David Monniaux | 2019-03-22 | 1 | -2/+6 |
| | | |||||
* | | improved testing | David Monniaux | 2019-03-22 | 1 | -5/+16 |
| | | |||||
* | | some more testing | David Monniaux | 2019-03-22 | 1 | -1/+1 |
| | | |||||
* | | uses yarpgen random generator | David Monniaux | 2019-03-22 | 1 | -0/+37 |
|/ | |||||
* | better patch for running the test suite | David Monniaux | 2019-03-22 | 1 | -0/+13 |
| | |||||
* | Now we have division, simplify the patch. | David Monniaux | 2019-03-22 | 1 | -50/+0 |
| | |||||
* | csmith for testing | David Monniaux | 2019-03-20 | 1 | -0/+23 |
| | |||||
* | Makefile for ocamlrun testing | David Monniaux | 2019-03-20 | 1 | -0/+7 |
| | |||||
* | ocaml byterunner example | David Monniaux | 2019-03-20 | 119 | -0/+45174 |
| | |||||
* | rm need for gcc | David Monniaux | 2019-03-20 | 2 | -4/+2 |
| | |||||
* | use the original source codes | David Monniaux | 2019-03-20 | 30 | -5528/+5235 |
| | |||||
* | picomus compile aussi | David Monniaux | 2019-03-20 | 1 | -1/+1 |
| | |||||
* | picosat fonctionne | David Monniaux | 2019-03-20 | 2 | -3/+7 |
| | |||||
* | vire des scories INT_DIV et INT_MOD | David Monniaux | 2019-03-20 | 5 | -6/+6 |
| | |||||
* | maddl / maddlim are synthesized (but not for pointers it seems) | David Monniaux | 2019-03-20 | 2 | -5/+21 |
| | |||||
* | mul immediate begin | David Monniaux | 2019-03-19 | 1 | -0/+4 |
| | |||||
* | seems to work | David Monniaux | 2019-03-19 | 1 | -0/+7 |
| | |||||
* | test for madd | David Monniaux | 2019-03-19 | 1 | -0/+9 |
| | |||||
* | andn / orn long complete I think | David Monniaux | 2019-03-18 | 1 | -0/+16 |
| | |||||
* | stats on chunks etc. | David Monniaux | 2019-03-17 | 1 | -3/+5 |
| |