aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Fix arm compile broken by merge problems.Bernhard Schommer2018-03-061-4/+2
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-0615-73/+289
* Removed no longer needed struct passing.Bernhard Schommer2018-02-261-2/+0
* Support Coq 8.7.2Xavier Leroy2018-02-191-3/+3
* Merge pull request #60 from AbsIntPrivate/struct-abi-internalXavier Leroy2018-02-199-110/+80
|\
| * Struct return on OpenBSD now testedMichael Schmidt2018-02-191-1/+1
| * Renamed StructReturn to structPassingBernhard Schommer2018-02-163-1/+1
| * Removed struct passing/return from ConfigurationsBernhard Schommer2018-02-163-89/+0
| * Move struct passing/return style to Machine.Bernhard Schommer2018-02-164-18/+77
| * Rename abi for ppc-linux targets.Bernhard Schommer2018-02-161-2/+2
|/
* Fix typo in commentMichael Schmidt2018-02-161-1/+1
* Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)Xavier Leroy2018-02-168-51/+202
* Switching the cases seems to work on x86_32Bernhard Schommer2018-02-121-2/+2
* In "symbol + ofs" addressing modes, limit the range of "ofs" in 64 bitsXavier Leroy2018-02-123-11/+33
* Add support for x86_64 BSD (#56)Xavier Leroy2018-02-091-3/+19
* Added error summary in case of fatal error.Bernhard Schommer2018-02-093-1/+14
* Configure check for PIE (#55)Michael Schmidt2018-02-081-5/+12
* x86 ConstpropOp.addr_strength_reduction: always check validity of resulting a...Xavier Leroy2018-02-082-10/+15
* Truncation of array sizes when converting them to Coq's Z typeXavier Leroy2018-02-081-6/+8
* Extend the modorder tool to handle Coq files as well (#54)Bernhard Schommer2018-02-081-7/+9
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-0826-138/+147
* Removed superfluous check.Bernhard Schommer2018-02-061-4/+0
* Share code for common options.Bernhard Schommer2018-01-293-131/+120
* Don't depend on the judgmental behavior of Bool.eqb (#217)Jason Gross2018-01-171-1/+1
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2018-01-171-3/+9
|\
| * Added type annotations for exported program. (#50)v3.2Bernhard Schommer2018-01-151-2/+2
| * Use Ptrofs.repr instead of Int.repr for Init_addrof. (#51)Bernhard Schommer2018-01-151-1/+7
* | Added missing help and common options.Bernhard Schommer2018-01-171-1/+15
|/
* Preparations for release 3.2Xavier Leroy2018-01-132-6/+9
* Improved message recommending an OCaml version to useXavier Leroy2018-01-131-1/+1
* Add regression test for issue #211Xavier Leroy2018-01-133-1/+17
* Mention the RISC-V port as wellXavier Leroy2018-01-132-3/+3
* Bump to version 3.2Xavier Leroy2018-01-131-1/+1
* Move machine initialization to Frontend.init function. (#49)Bernhard Schommer2018-01-114-42/+30
* Update copyright sectionXavier Leroy2018-01-111-3/+4
* Update Changelog with recent changesXavier Leroy2018-01-111-1/+13
* Added option -o to clightgen.Bernhard Schommer2018-01-111-5/+47
* Add riscv and attributes to ClightgenBernhard Schommer2018-01-101-0/+4
* Minor improvements.Bernhard Schommer2018-01-101-2/+2
* Change README to markdown.Bernhard Schommer2018-01-101-15/+14
* Remove mnemonics not exported to JSON from mnemonics listMichael Schmidt2018-01-091-4/+4
* Update man page for new Diab target optionMichael Schmidt2018-01-081-6/+8
* Update man page for new Diab target optionMichael Schmidt2018-01-081-0/+6
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-0510-62/+87
* Added toolchain specific option for dcc. (#47)Bernhard Schommer2018-01-051-1/+16
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-0517-8/+60
* Handle dcompcertc and dparsedc like all dump opts.Bernhard Schommer2018-01-044-13/+18
* Remove duplicated code. Bug 20521Bernhard Schommer2018-01-041-46/+26
* Remove all temporary files at program exit (#46)Bernhard Schommer2018-01-034-19/+17
* ValueAnalysis: remove duplicate list_forall2_in_left (#212)Jérémie Koenig2018-01-031-13/+2