Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | David Monniaux | 2019-04-11 | 4 | -818/+368 | |
|\ | ||||||
| * | update from Impure Library | Sylvain Boulmé | 2019-04-11 | 1 | -20/+22 | |
| * | more robust pattern-matching in *op_eq | Sylvain Boulmé | 2019-04-11 | 1 | -8/+10 | |
| * | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | Sylvain Boulmé | 2019-04-11 | 5 | -3/+18 | |
| |\ | ||||||
| * | | refactor for #92 | Sylvain Boulmé | 2019-04-11 | 3 | -790/+336 | |
* | | | adjust list of builtins according to documentation | David Monniaux | 2019-04-11 | 1 | -5/+5 | |
| |/ |/| | ||||||
* | | afaddd / afaddw | David Monniaux | 2019-04-11 | 5 | -3/+18 | |
|/ | ||||||
* | instruction cache builtins | David Monniaux | 2019-04-11 | 4 | -3/+18 | |
* | data cache builtins | David Monniaux | 2019-04-11 | 4 | -5/+25 | |
* | some more builtins | David Monniaux | 2019-04-11 | 4 | -5/+30 | |
* | __builtin_k1_ldu | David Monniaux | 2019-04-11 | 4 | -9/+16 | |
* | wfxl / wfxm | David Monniaux | 2019-04-11 | 5 | -6/+27 | |
* | fix types for k1 builtins | David Monniaux | 2019-04-11 | 1 | -2/+2 | |
* | __builtin_k1_get and __builtin_k1_set with safeguards, work for clock | David Monniaux | 2019-04-11 | 1 | -3/+10 | |
* | get / set k1 | David Monniaux | 2019-04-10 | 5 | -3/+23 | |
* | achieve issue #89 ? | Sylvain Boulmé | 2019-04-10 | 1 | -185/+47 | |
* | Fixing missing features in Asmexpand.ml (EF_annot, EF_annot_val, EF_inline_asm) | Cyril SIX | 2019-04-09 | 1 | -9/+6 | |
* | moving iandb from ImpCore to ImpPrelude | Sylvain Boulmé | 2019-04-08 | 2 | -23/+18 | |
* | improving comments on Asmvliw | Sylvain Boulmé | 2019-04-08 | 1 | -17/+29 | |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-refactor | Cyril SIX | 2019-04-08 | 15 | -87/+1202 | |
|\ | ||||||
| * | no need for this to be in two_address_op | David Monniaux | 2019-04-06 | 1 | -1/+1 | |
| * | reinstated the orl selectl construct | David Monniaux | 2019-04-05 | 2 | -10/+7 | |
| * | Oselectf, Oselectfs with condition | David Monniaux | 2019-04-05 | 7 | -123/+323 | |
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary | David Monniaux | 2019-04-05 | 1 | -1/+1 | |
| |\ | ||||||
| * | | selectl with condition | David Monniaux | 2019-04-05 | 7 | -64/+171 | |
| * | | Select cmplu | David Monniaux | 2019-04-05 | 2 | -1/+32 | |
| * | | select cmpu | David Monniaux | 2019-04-05 | 7 | -5/+60 | |
| * | | factor out some proofs | David Monniaux | 2019-04-05 | 1 | -6/+3 | |
| * | | some more Oselect comparisons | David Monniaux | 2019-04-04 | 2 | -1/+14 | |
| * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary | David Monniaux | 2019-04-04 | 2 | -352/+187 | |
| |\ \ | ||||||
| * | | | ternary ops work on (unsigned/signed) int with test on signed int | David Monniaux | 2019-04-04 | 1 | -3/+3 | |
| * | | | more on select | David Monniaux | 2019-04-04 | 1 | -0/+5 | |
| * | | | Oselect | David Monniaux | 2019-04-04 | 2 | -5/+16 | |
| * | | | progress on Oselect | David Monniaux | 2019-04-04 | 1 | -19/+35 | |
| * | | | select_sound | David Monniaux | 2019-04-04 | 3 | -38/+102 | |
| * | | | some more progress on select | David Monniaux | 2019-04-04 | 4 | -59/+84 | |
| * | | | progressing on select | David Monniaux | 2019-04-04 | 2 | -17/+11 | |
| * | | | working on select | David Monniaux | 2019-04-04 | 1 | -3/+24 | |
| * | | | working on select | David Monniaux | 2019-04-04 | 1 | -28/+58 | |
| * | | | prepare for conditions in cmove | David Monniaux | 2019-04-04 | 4 | -19/+34 | |
| * | | | ternary ops for float/double | David Monniaux | 2019-04-03 | 3 | -2/+72 | |
| * | | | for floats and doubles, asmgen support | David Monniaux | 2019-04-03 | 3 | -15/+92 | |
| * | | | ternary ops in AES and TEA | David Monniaux | 2019-04-03 | 4 | -8/+9 | |
| * | | | problem in ValueAOp | David Monniaux | 2019-04-03 | 4 | -9/+12 | |
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary | David Monniaux | 2019-04-03 | 30 | -2245/+1299 | |
| |\ \ \ | ||||||
| * \ \ \ | merge VLIW proofs | David Monniaux | 2019-03-28 | 7 | -23/+1073 | |
| |\ \ \ \ | ||||||
| | * \ \ \ | merge proof of VLIW | David Monniaux | 2019-03-28 | 7 | -23/+1073 | |
| | |\ \ \ \ | ||||||
| * | | | | | | improvements on cmoved etc. | David Monniaux | 2019-03-27 | 2 | -93/+7 | |
| * | | | | | | match some 'and' | David Monniaux | 2019-03-27 | 2 | -10/+34 | |
| * | | | | | | selectl generation | David Monniaux | 2019-03-26 | 6 | -14/+205 |