aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Expand)AuthorAgeFilesLines
* 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
* Fix for switch was to eager.Bernhard Schommer2015-11-061-6/+8
* Remove debug stmts during grouping of switch.Bernhard Schommer2015-11-061-3/+5
* Added printing functions for debug annotations.Bernhard Schommer2015-11-061-0/+3
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-201-2/+2
|\
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1420-1989/+1989
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-143-41/+41
| * Unified function for adding the atom identifier.Bernhard Schommer2015-10-121-2/+2
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2023-2030/+2030
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-113-14/+15
|/
* Fixed minor issue with parameters that get put on the stack, madeBernhard Schommer2015-09-301-4/+6
* Added location for the formal parameters and move the end of allBernhard Schommer2015-09-281-0/+1
* Merge branch 'debugscopes' into debug_locationsBernhard Schommer2015-09-212-41/+39
|\
| * Experiment: track the scopes of local variables via __builtin_debug.Xavier Leroy2015-09-201-38/+36
| * Ctypes.composite_of_def: make sure it computes within Coq.Xavier Leroy2015-09-181-3/+3
* | Started implementing the scope for the Debug Informations.Bernhard Schommer2015-09-181-0/+1
* | First version with computation of dwarf info from debug info.Bernhard Schommer2015-09-171-1/+1
* | Move more functionality in the new interface.Bernhard Schommer2015-09-161-4/+7
* | XBernhard Schommer2015-09-064-77/+215
|\|
| * Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-232-26/+194
| * Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-221-1/+1
| * Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-50/+20
* | Added symbol functions for printing of the location for global variables.Bernhard Schommer2015-08-211-2/+8
|/
* Tighten and prove correct the underflow/overflow bounds for parsing of FP lit...Xavier Leroy2015-07-061-41/+29
* Added a fast test for too large exponents too avoid never ending computations.Bernhard Schommer2015-07-031-29/+42
* Merge branch 'master' of https://github.com/AbsInt/CompCertXavier Leroy2015-06-301-1/+26
|\
| * Check also the discarded part of the switch statements for cases outside of a...Bernhard Schommer2015-06-261-1/+26
* | Signedness issue in specification of subtraction between two pointers.Xavier Leroy2015-06-303-6/+19
|/
* In AST.calling_conventions, record whether the original C function was "old-s...Xavier Leroy2015-05-223-20/+24
* Missing case in type_conditional (long long vs. int or float).Xavier Leroy2015-05-221-6/+3
* Ctyping: better typing of conditional expressions.Xavier Leroy2015-05-213-50/+200
generated by cgit (git 2.34.1) at 2024-06-02 17:36:54 +0000