aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into cleanupBernhard Schommer2016-03-2188-5401/+6282
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-2073-5026/+5836
| |\
| | * Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-065-39/+44
| | * Strengthen the main compiler correctness results to account for separate comp...Xavier Leroy2016-03-061-149/+250
| | * 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
| | * Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-0636-2188/+2093
| | * Put forward_simulation and backward_simulation in Prop instead of TypeXavier Leroy2016-03-062-303/+323
| | * Add support for EF_runtime externalsXavier Leroy2016-03-069-57/+47
| | * Globalenvs: adapt to new linking framework, and revise.Xavier Leroy2016-03-061-1146/+729
| | * AST: extend and adapt to the new linking framework.Xavier Leroy2016-03-061-460/+116
| | * The basic framework for linking and separate compilation.Xavier Leroy2016-03-061-0/+905
| | * Preliminaries: minor extensions to MemoryXavier Leroy2016-03-061-3/+58
| | * Preliminaries: extend the Coqlib and Maps libraries.Xavier Leroy2016-03-062-34/+189
| * | Add -Xalign-value to enforce correct alignment.Bernhard Schommer2016-03-181-2/+3
| * | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-159-22/+22
| * | GPR#84: extend Cminor parser to handle single-precision FP operationsXavier Leroy2016-03-152-3/+20
| * | GPR#84: add missing IA32 operators to PrintOpXavier Leroy2016-03-151-0/+3
| * | 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
| * | | Merge branch 'relaxed-pointer-arithmetic'Bernhard Schommer2016-03-111-6/+21
| |\ \ \
| | * | | Relaxing the semantics of pointer arithmetic.Xavier Leroy2016-02-291-6/+21
* | | | | Revert "Add the -Xalign-value options for diab."Bernhard Schommer2016-03-181-1/+0
* | | | | Add the -Xalign-value options for diab.Bernhard Schommer2016-03-181-0/+1
* | | | | Added an interface file for DebugInformation.Bernhard Schommer2016-03-185-43/+183
* | | | | Added interface for the Asmexpansion.Bernhard Schommer2016-03-165-10/+55
* | | | | Change atom printer to use the common function.Bernhard Schommer2016-03-161-1/+1
* | | | | Cleanup of AsmToJSON.Bernhard Schommer2016-03-166-128/+140
* | | | | Removed not needed env.Bernhard Schommer2016-03-151-5/+5
* | | | | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-1547-447/+449
* | | | | Added back invariant checks for IRC.Bernhard Schommer2016-03-151-0/+36
* | | | | Revert "Removed unused parameter from is_small/rel_data."Bernhard Schommer2016-03-156-26/+28
* | | | | Removed unused parameter from is_small/rel_data.Bernhard Schommer2016-03-116-28/+26
* | | | | Cleanup of Clightgen code.Bernhard Schommer2016-03-102-45/+41
* | | | | Clean up of ia32 target dependend code.Bernhard Schommer2016-03-104-58/+18
* | | | | Cleanup of ARM dependedn code.Bernhard Schommer2016-03-102-66/+8
* | | | | Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-105-17/+21
* | | | | Code cleanup.Bernhard Schommer2016-03-1056-740/+590
|/ / / /
* | | / Fixed typo in equal types.Bernhard Schommer2016-03-101-1/+1
| |_|/ |/| |
* | | Added more support for gcc options.Bernhard Schommer2016-03-021-4/+75
| |/ |/|
* | Merge remote-tracking branch 'origin/configuration-split'Bernhard Schommer2016-02-293-23/+58
|\ \
| * | Split up tools and options.Bernhard Schommer2016-02-253-23/+58
* | | Added gcc's Xassembler option.Bernhard Schommer2016-02-291-3/+8
* | | Fixed typo. Bug 18066Bernhard Schommer2016-02-291-3/+4
* | | Added some gcc linker options.Bernhard Schommer2016-02-261-0/+22
|/ /
* | bug 18168, catch cases where variadic arguments are transfered via registersMichael Schmidt2016-02-241-2/+2
* | bug 18168, fix offset computation for var-args in ARM stacklayoutMichael Schmidt2016-02-241-1/+1
* | bug 18209, make message compatible to clangMichael Schmidt2016-02-231-1/+1
* | bug 18209, check that input files existMichael Schmidt2016-02-231-0/+14
|/
* PR#87: include the BSD license in the LICENSE file.Xavier Leroy2016-02-191-1/+28
generated by cgit (git 2.34.1) at 2024-07-03 13:56:54 +0000