aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-0/+9
|\
| * begin installing profilingDavid Monniaux2020-04-081-1/+1
| * added EF_profilingDavid Monniaux2020-04-081-0/+9
* | Merge remote-tracking branch 'origin/mppa-expect3' into mppa-workDavid Monniaux2020-04-099-45/+86
|\ \
| * | expect operationDavid Monniaux2020-04-072-27/+35
| * | Oexpect in frontendDavid Monniaux2020-04-076-16/+47
| * | start implementing expect as exprDavid Monniaux2020-04-071-0/+1
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-expectDavid Monniaux2020-04-0611-124/+328
| |\|
| * | __builtin_expect defined as its first argumentDavid Monniaux2019-09-251-2/+3
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-082-31/+46
|\ \ \ | | |/ | |/|
| * | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-011-2/+2
| |\ \
| | * | Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-291-2/+2
| * | | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-031-29/+44
| |\| |
| | * | Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-021-29/+44
| * | | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-031-4/+36
| |\ \ \ | | |/ / | |/| |
* | | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-259-76/+232
|\ \ \ \
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-248-74/+229
| |\| | |
| | * | | Support re-normalization of values returned by function callsXavier Leroy2020-02-212-33/+137
| | * | | Refine the type of function results in AST.signatureXavier Leroy2020-02-216-39/+78
| | * | | More precise determination of small data accesses (#220)Bernhard Schommer2020-02-201-3/+15
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-132-2/+3
| |\| | | | | |/ / | |/| |
| | * | Take the sign into account for int to ptr cast.Bernhard Schommer2020-02-122-2/+3
* | | | thread local declarations now workDavid Monniaux2020-02-241-1/+5
* | | | it now works, no more ugly hack to access thread local dataDavid Monniaux2020-02-241-0/+9
* | | | seems to process _Thread_local but not till backendDavid Monniaux2020-02-241-7/+14
|/ / /
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-12-091-0/+5
|\| |
| * | Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-281-0/+5
* | | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...David Monniaux2019-09-202-17/+45
|\| | | |/ |/|
| * -dclight output: use nicer names for temporary variablesXavier Leroy2019-09-161-2/+11
| * clightgen -dclight: print function parameters correctlyXavier Leroy2019-09-162-15/+34
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-08-285-14/+17
|\|
| * bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-1/+3
| * Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-054-13/+14
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-196-65/+227
|\|
| * Make __builtin_sel available from C source codeXavier Leroy2019-07-175-31/+157
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-9/+34
| * Remove the cparser/Builtins moduleXavier Leroy2019-07-171-7/+10
| * Change the expected types for arguments to __builtin_annot, and extended asmXavier Leroy2019-06-191-5/+25
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-036-10/+9
|\|
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-312-2/+2
| * Csyntax.v: Fix a typo in a documentation comment (#292)Bart Jacobs2019-05-211-1/+1
| * lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-232-2/+1
| * Replace nat_of_Z with Z.to_natXavier Leroy2019-04-231-1/+1
| * Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-4/+4
* | ternary ops for float/doubleDavid Monniaux2019-04-031-0/+4
* | problem in ValueAOpDavid Monniaux2019-04-031-0/+1
* | attempts at generating builtins, startDavid Monniaux2019-04-031-1/+8
* | la division flottante fonctionneDavid Monniaux2019-03-201-2/+16
* | ça semble passerDavid Monniaux2019-03-201-2/+4
* | added helper functions but strangeDavid Monniaux2019-03-191-1/+17
|/
generated by cgit (git 2.34.1) at 2024-06-02 19:12:27 +0000