aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* code for checking IEEE-754 exceptionsDavid Monniaux2019-04-131-0/+41
|
* experiments with rounding modesDavid Monniaux2019-04-131-5/+21
|
* test for rounding modesDavid Monniaux2019-04-131-0/+20
|
* dirty fix for issue #112David Monniaux2019-04-131-3/+7
| | | | That should not be the final say on this.
* test breaksDavid Monniaux2019-04-121-0/+44
|
* better #include handlingDavid Monniaux2019-04-121-1/+5
|
* workaround for non-standard C isfinite macro in math.hDavid Monniaux2019-04-122-1/+4
|
* 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-128-1209/+17
|
* some more simplificationsDavid Monniaux2019-04-122-3/+25
|
* some more simplificationsDavid Monniaux2019-04-122-11/+17
|
* more simplificationsDavid Monniaux2019-04-122-0/+6
|
* simplification of the varargs procedure: they are leaf procedures, there is ↵David Monniaux2019-04-121-40/+1
| | | | no need to save $ra
* fix wrongly removed builtinsDavid Monniaux2019-04-121-1/+3
|
* more builtinsDavid Monniaux2019-04-118-20/+59
|
* experiments on the meaning of sbmm8David Monniaux2019-04-112-0/+24
|
* __builtin_k1_acswapwDavid Monniaux2019-04-114-1/+38
|
* builtin acswapdDavid Monniaux2019-04-113-2/+29
|
* 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-116-3/+29
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | refactor for #92Sylvain Boulmé2019-04-113-790/+336
| | |
* | | cleaner: put all the special types, defines etc. in one header fileDavid Monniaux2019-04-113-1/+15
| | |
* | | adjust list of builtins according to documentationDavid Monniaux2019-04-111-5/+5
| |/ |/|
* | afaddd / afaddwDavid Monniaux2019-04-116-3/+29
|/
* demo of instruction cache flushDavid Monniaux2019-04-111-0/+27
|
* instruction cache builtinsDavid Monniaux2019-04-115-3/+23
|
* data cache builtinsDavid Monniaux2019-04-115-5/+28
|
* some more builtinsDavid Monniaux2019-04-115-5/+38
|
* __builtin_k1_lduDavid Monniaux2019-04-115-9/+20
|
* wfxl / wfxmDavid Monniaux2019-04-116-6/+35
|
* fix types for k1 builtinsDavid Monniaux2019-04-112-2/+57
|
* __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
|
* Merge branch 'mppa-work' of ↵David Monniaux2019-04-101-185/+47
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * achieve issue #89 ?Sylvain Boulmé2019-04-101-185/+47
| |
* | now compiles with pthread.hDavid Monniaux2019-04-101-4/+1
| |
* | Merge branch 'mppa-work' of ↵David Monniaux2019-04-105-14/+12
|\| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * Fixing missing features in Asmexpand.ml (EF_annot, EF_annot_val, EF_inline_asm)Cyril SIX2019-04-091-9/+6
| |
| * Disabling the packedstruct tests from test/regressionCyril SIX2019-04-091-1/+2
| |
| * All CompCert tests can be compiledCyril SIX2019-04-093-4/+4
| |
* | for killing _PragmaDavid Monniaux2019-04-081-0/+1
|/
* exemples d'accès mémoire lentsDavid Monniaux2019-04-083-0/+31
|
* moving iandb from ImpCore to ImpPreludeSylvain Boulmé2019-04-082-23/+18
|
* better explanationDavid Monniaux2019-04-081-4/+26
|