aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
* read from bit fieldsDavid Monniaux2019-04-252-5/+21
|
* progressDavid Monniaux2019-04-2510-8/+90
|
* IT COMPILESDavid Monniaux2019-04-256-40/+43
|
* some progressDavid Monniaux2019-04-251-1/+5
|
* some more progressDavid Monniaux2019-04-252-2/+39
|
* some progress on bitfieldsDavid Monniaux2019-04-254-1/+33
|
* begin bitfieldsDavid Monniaux2019-04-245-1/+11
|
* make_prologue à partDavid Monniaux2019-04-242-6/+9
|
* dirty fix for issue #112David Monniaux2019-04-131-3/+7
| | | | That should not be the final say on this.
* some more simplificationsDavid Monniaux2019-04-122-0/+2
|
* some simplifications (long)David Monniaux2019-04-122-0/+58
|
* more simplificationsDavid Monniaux2019-04-122-8/+13
|
* some more simplificationDavid Monniaux2019-04-122-0/+16
|
* some more simplificationDavid Monniaux2019-04-122-0/+7
|
* some more simplificationsDavid Monniaux2019-04-122-0/+7
|
* some more simplificationsDavid Monniaux2019-04-122-3/+25
|
* some more simplificationsDavid Monniaux2019-04-122-11/+17
|
* more simplificationsDavid Monniaux2019-04-122-0/+6
|
* fix wrongly removed builtinsDavid Monniaux2019-04-121-1/+3
|
* more builtinsDavid Monniaux2019-04-114-4/+32
|
* Merge branch 'mppa-work' of ↵David Monniaux2019-04-114-818/+368
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * update from Impure LibrarySylvain Boulmé2019-04-111-20/+22
| |
| * more robust pattern-matching in *op_eqSylvain Boulmé2019-04-111-8/+10
| |
| * Merge branch 'mppa-work' of ↵Sylvain Boulmé2019-04-115-3/+18
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | refactor for #92Sylvain Boulmé2019-04-113-790/+336
| | |
* | | adjust list of builtins according to documentationDavid Monniaux2019-04-111-5/+5
| |/ |/|
* | afaddd / afaddwDavid Monniaux2019-04-115-3/+18
|/
* instruction cache builtinsDavid Monniaux2019-04-114-3/+18
|
* data cache builtinsDavid Monniaux2019-04-114-5/+25
|
* some more builtinsDavid Monniaux2019-04-114-5/+30
|
* __builtin_k1_lduDavid Monniaux2019-04-114-9/+16
|
* wfxl / wfxmDavid Monniaux2019-04-115-6/+27
|
* fix types for k1 builtinsDavid Monniaux2019-04-111-2/+2
|
* __builtin_k1_get and __builtin_k1_set with safeguards, work for clockDavid Monniaux2019-04-111-3/+10
|
* get / set k1David Monniaux2019-04-105-3/+23
|
* achieve issue #89 ?Sylvain Boulmé2019-04-101-185/+47
|
* Fixing missing features in Asmexpand.ml (EF_annot, EF_annot_val, EF_inline_asm)Cyril SIX2019-04-091-9/+6
|
* moving iandb from ImpCore to ImpPreludeSylvain Boulmé2019-04-082-23/+18
|
* improving comments on AsmvliwSylvain Boulmé2019-04-081-17/+29
|
* Merge remote-tracking branch 'origin/mppa-work' into mppa-refactorCyril SIX2019-04-0815-87/+1202
|\ | | | | | | | | | | Conflicts: mppa_k1c/Asm.v mppa_k1c/Asmblock.v
| * no need for this to be in two_address_opDavid Monniaux2019-04-061-1/+1
| |
| * reinstated the orl selectl constructDavid Monniaux2019-04-052-10/+7
| |
| * Oselectf, Oselectfs with conditionDavid Monniaux2019-04-057-123/+323
| |
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-051-1/+1
| |\
| * | selectl with conditionDavid Monniaux2019-04-057-64/+171
| | |
| * | Select cmpluDavid Monniaux2019-04-052-1/+32
| | |
| * | select cmpuDavid Monniaux2019-04-057-5/+60
| | |
| * | factor out some proofsDavid Monniaux2019-04-051-6/+3
| | |
| * | some more Oselect comparisonsDavid Monniaux2019-04-042-1/+14
| | |
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-042-352/+187
| |\ \
generated by cgit (git 2.34.1) at 2024-07-12 06:05:52 +0000