aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* Issues with invalid x86 addressing modes (Github issue #183)Xavier Leroy2017-05-173-18/+27
* Make redefinition of composite a fatal error.Bernhard Schommer2017-05-091-2/+1
* Print 64bit constants for rldimn and rldimi.Bernhard Schommer2017-05-051-2/+2
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2017-05-051-2/+4
|\
| * Bring RISC-V port up to dateXavier Leroy2017-05-051-2/+4
* | bug 20956, print correct error message depending on architectureMichael Schmidt2017-05-031-2/+8
|/
* More asserts.Bernhard Schommer2017-05-031-1/+1
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-03107-1436/+3975
* Tunnelingproof: Remove assumption destroyed_by_cond c = nil.Xavier Leroy2017-05-021-66/+210
* RISC-V vararg.S: a "sw" instruction should be "sptr"Xavier Leroy2017-04-291-1/+1
* Update Changelog with recent changesXavier Leroy2017-04-281-1/+7
* RISC-V port and assorted changesXavier Leroy2017-04-2880-102/+12962
* Issue #179: clightgen produces wrong abstract syntax for "switch" statementsXavier Leroy2017-04-282-3/+11
* Always generate .merlin and _CoqProject files.Bernhard Schommer2017-04-281-19/+7
* Modest optimization of leaf functions (continued)Xavier Leroy2017-04-283-159/+116
* Modest optimization of leaf functionsXavier Leroy2017-04-284-46/+241
* Assert instead of unit.Bernhard Schommer2017-04-101-6/+6
* Filter out functions earlier. Bug 21343Bernhard Schommer2017-04-101-24/+27
* Fix name of function. Bug 21378Bernhard Schommer2017-04-071-1/+1
* Do not generate code for "inline definitions"Bernhard Schommer2017-04-073-30/+41
* Add optimization option finline.Bernhard Schommer2017-04-074-1/+8
* Another optimization of empty if/else and other useless conditional branchesXavier Leroy2017-04-062-31/+41
* attempt to optimize empty if/then/else statementsMichael Schmidt2017-04-063-7/+32
* Replace 'decide equality' in powerpc/Op.v. Bug 21332Bernhard Schommer2017-04-031-4/+5
* Update the "make check-proof" entry for Coq 8.6Xavier Leroy2017-03-241-3/+2
* Added handling if s.sloc <> s1.slocBernhard Schommer2017-03-241-2/+6
* Emit line stmt after labels in general. Bug 21232Bernhard Schommer2017-03-241-10/+6
* Do not emit line info before case stmt.Bernhard Schommer2017-03-241-4/+9
* use 'f' as generic function-identifier instead of arbitraty identifier 1 for ...Michael Schmidt2017-03-231-1/+1
* Better fix for problems with quoting in files.Bernhard Schommer2017-03-202-4/+4
* Quote directory for comp_dir entry.Bernhard Schommer2017-03-201-2/+2
* Merge pull request #175 from silene/IZRXavier Leroy2017-03-0815-150/+121
|\
| * Adapt proofs to future handling of literal constants in Coq.Guillaume Melquiond2017-03-0815-150/+121
* | Added missing dltl to dall.Bernhard Schommer2017-03-081-0/+1
|/
* Add a switch to generate a _CoqProject file.Bernhard Schommer2017-02-232-1/+24
* Added check for large arrays.Bernhard Schommer2017-02-213-0/+14
* update manpage for new optionsMichael Schmidt2017-02-211-4/+16
* Added gcc noinline attribute.Bernhard Schommer2017-02-192-0/+2
* Added unused attribute and simplified checks.Bernhard Schommer2017-02-172-44/+84
* Adopted unused variable and attribtue checkBernhard Schommer2017-02-173-31/+55
* Extended unused vars check for params.Bernhard Schommer2017-02-173-2/+9
* Added a simple check for unused variables.Bernhard Schommer2017-02-175-2/+88
* Checks can be applied add several places.Bernhard Schommer2017-02-173-8/+5
* Also check the locals. Bug 19872.Bernhard Schommer2017-02-171-3/+7
* Added new module for checks on elaborated C codeBernhard Schommer2017-02-173-2/+114
* Do not optimize away the 'return 0' at end of 'main'Xavier Leroy2017-02-171-7/+5
* Control-flow analysis: bug in switch without defaultXavier Leroy2017-02-171-1/+30
* Merge pull request #172 from AbsInt/std_noreturn_funXavier Leroy2017-02-173-3/+14
|\
| * Added _exit.Bernhard Schommer2017-02-171-1/+1
| * Add longjmp. Bug 21009Bernhard Schommer2017-02-171-1/+1
generated by cgit (git 2.34.1) at 2024-06-01 14:24:03 +0000