aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Expand)AuthorAgeFilesLines
* Do not generate code for "inline definitions"Bernhard Schommer2017-04-071-8/+15
* attempt to optimize empty if/then/else statementsMichael Schmidt2017-04-063-7/+32
* Added gcc noinline attribute.Bernhard Schommer2017-02-191-0/+1
* Added unused attribute and simplified checks.Bernhard Schommer2017-02-171-1/+2
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-131-2/+2
* Use "Local" as prefixXavier Leroy2017-02-132-3/+3
* Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into maxime...Xavier Leroy2017-02-132-7/+9
|\
| * Some backward compatible Ltac fixes, necessary for 8.6.Maxime Dénès2017-01-091-5/+7
| * An hypothesis has changed name.Maxime Dénès2017-01-091-1/+1
| * The subst tactic has become more powerful.Maxime Dénès2017-01-091-1/+1
* | More tweaking of module 'open'Xavier Leroy2017-02-091-8/+10
* | Merge branch 'elaboration-of-attributes'Xavier Leroy2017-02-061-1/+15
|\ \
| * | Preliminary support for the "noreturn" attributeXavier Leroy2017-02-061-1/+2
| * | Refactor the classification of attributesXavier Leroy2017-02-031-0/+13
| * | Revised elaboration of attributesXavier Leroy2017-01-311-1/+1
* | | Cleanup opensBernhard Schommer2017-02-061-69/+62
* | | Removed shadowing problems.Bernhard Schommer2017-02-061-9/+9
* | | Inlined open of ASTBernhard Schommer2017-02-061-7/+6
|/ /
* / Simplified C2C.error.Bernhard Schommer2017-01-182-19/+16
|/
* C2C: revise typing and translation of __builtin_memcpy_alignedXavier Leroy2016-11-171-12/+16
* Initializers: introduce 'constval_cast' to cast constant value to desired typeXavier Leroy2016-11-172-21/+25
* C2C: wrong translation of 'switch' over arguments of type 'long' if 'long' is...Xavier Leroy2016-11-171-4/+5
* fix va_arg for pointer types on 64bit targetMichael Schmidt2016-11-081-1/+7
* extend constant check for builtin_memcpy_aligned (bug 20320)Michael Schmidt2016-11-071-2/+2
* extend constant check for builtin_memcpy_aligned (bug 20320)Michael Schmidt2016-11-071-0/+2
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-2719-967/+1300
|\
| * Regression: handling of integer + pointer in CompCert CXavier Leroy2016-10-064-115/+112
| * Regression: compile-time evaluation of ((struct s *)0)->fieldXavier Leroy2016-10-062-4/+7
| * Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-0/+8
| * Remove usage of do.Bernhard Schommer2016-10-041-58/+58
| * Support for 64-bit architectures: generic supportXavier Leroy2016-10-0119-926/+1251
* | implement checks for parameters of '__builtin_memcpy_aligned' (bug 20222)Michael Schmidt2016-10-191-4/+4
* | implement checks for parameters of '__builtin_memcpy_aligned' (bug 20222)Michael Schmidt2016-10-191-3/+6
|/
* Improved error messages for wrong vararg calls.Bernhard Schommer2016-09-231-2/+7
* Catch case of zero in builtin debug.Bernhard Schommer2016-09-221-2/+2
* Merge pull request #142 from maximedenes/minor-fixesXavier Leroy2016-09-211-5/+8
|\
| * Fix minor issues in some proofs and tactics.Maxime Dénès2016-09-211-5/+8
* | Merge pull request #139 from AbsInt/advanced-diagnosticsBernhard Schommer2016-09-202-36/+34
|\ \
| * | Readded warning about ignored volatile. Bug 18004Bernhard Schommer2016-08-311-1/+1
| * | Added missing literal. Bug 18004Bernhard Schommer2016-08-311-1/+1
| * | Fixed typos.Bernhard Schommer2016-08-311-8/+8
| * | bug 18004, fix some typos/grammarMichael Schmidt2016-08-301-1/+1
| * | Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-292-3/+23
| |\ \
| * | | Classified all warnings and added various options.Bernhard Schommer2016-07-292-34/+33
| | |/ | |/|
* | | Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-171-31/+4
* | | Removed some implict arguments.Bernhard Schommer2016-09-051-13/+5
| |/ |/|
* | Simplify test. Bug 19629Bernhard Schommer2016-08-251-4/+1
* | Test for illegal first argument in __builtin_debug.Bernhard Schommer2016-08-251-2/+6
* | Print prototypes for malloc and free.Bernhard Schommer2016-08-231-1/+1
* | Also print declarations in CompCert C.Bernhard Schommer2016-08-221-0/+20
generated by cgit (git 2.34.1) at 2024-06-02 17:06:57 +0000