aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Changes to include a -O1 -fschedule-insns2 gcc run as wellCyril SIX2019-04-2624-290/+384
* simplify proof slightlyv3.5_k1c_1.1David Monniaux2019-04-251-20/+16
* read from bit fieldsDavid Monniaux2019-04-253-5/+41
* progressDavid Monniaux2019-04-2511-8/+104
* IT COMPILESDavid Monniaux2019-04-257-45/+48
* 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-246-1/+26
* make_prologue à partDavid Monniaux2019-04-242-6/+9
* identify bug from x86David Monniaux2019-04-131-2/+4
* various bugs in FPDavid Monniaux2019-04-131-0/+6
* some more examplesDavid Monniaux2019-04-131-4/+39
* Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-04-131-0/+15
|\
| * feclearexcept / fetestexceptDavid Monniaux2019-04-131-0/+15
* | 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
* 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 n...David Monniaux2019-04-121-40/+1
* 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 gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-04-114-818/+368
|\
| * 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 gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...Sylvain Boulmé2019-04-116-3/+29
| |\
| * | 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