aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Expand)AuthorAgeFilesLines
* 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
* | Added missing , in PrintCsyntax. Bug 19599Bernhard Schommer2016-08-221-1/+1
|/
* Port to Coq 8.5pl2Xavier Leroy2016-07-082-2/+1
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-211-1/+1
* fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert can...Michael Schmidt2016-06-071-1/+1
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-172-3/+3
* Merge branch 'master' into cleanupBernhard Schommer2016-03-2123-989/+1493
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-2018-649/+1093
| |\
| | * Update the proofs of the C front-end to the new linking framework.Xavier Leroy2016-03-0611-533/+559
| | * Define linking for Csyntax and Clight programs.Xavier Leroy2016-03-063-114/+523
| | * Add support for EF_runtime externalsXavier Leroy2016-03-064-2/+11
| * | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-152-6/+6
| * | Merge pull request #90 from AbsInt/sem-castsXavier Leroy2016-03-1114-323/+368
| |\ \
| | * | Make casts of pointers to _Bool semantically well defined (again).Xavier Leroy2016-03-0214-323/+368
| | |/
| * / Relaxing the semantics of pointer arithmetic.Xavier Leroy2016-02-291-6/+21
| |/
* | Removed not needed env.Bernhard Schommer2016-03-151-5/+5
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-153-38/+38
* | Revert "Removed unused parameter from is_small/rel_data."Bernhard Schommer2016-03-151-3/+3
* | Removed unused parameter from is_small/rel_data.Bernhard Schommer2016-03-111-3/+3
* | Code cleanup.Bernhard Schommer2016-03-103-102/+93
|/
* Restart the name generator at first_unused_ident for every function.Xavier Leroy2016-02-053-58/+38
* Revise and simplify the -fstruct-return and -fstruct-passing options.Xavier Leroy2015-12-081-11/+18
* Handle large static initializers for global arraysXavier Leroy2015-11-093-118/+205
generated by cgit (git 2.34.1) at 2024-06-02 18:52:38 +0000