aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
| * Added handling for noreturn std functions.Bernhard Schommer2017-02-163-3/+14
|/
* Reverted changes in Cutil and catch in Cflow.Bernhard Schommer2017-02-162-17/+5
* Fixed problem with local structs/unions in Cflow.Bernhard Schommer2017-02-161-4/+17
* drop .cm support from man pageMichael Schmidt2017-02-151-4/+0
* Merge pull request #167 from AbsInt/pipe_prerequisiteXavier Leroy2017-02-158-35/+27
|\
| * Introduced configuration variable for gnu systems.Bernhard Schommer2017-02-138-35/+27
* | Merge pull request #162 from AbsInt/return-analysis-2Xavier Leroy2017-02-155-32/+290
|\ \
| * | Cflow: analysis of "switch" was too impreciseXavier Leroy2017-02-071-2/+3
| * | Revised, more precise implementation of control-flow analysisXavier Leroy2017-02-071-48/+98
| * | Control-flow analysis: wrong flow for "case"/"default" statementsXavier Leroy2017-02-071-4/+6
| * | More precise warnings about function returnsXavier Leroy2017-02-075-32/+237
* | | Remove tests involving Cminor concrete syntax. Update ChangelogXavier Leroy2017-02-1529-3336/+3
* | | Merge pull request #170 from AbsInt/remove_cminorXavier Leroy2017-02-159-1379/+3
|\ \ \
| * | | Removed CMinor import. Bug 20992Bernhard Schommer2017-02-149-1379/+3
* | | | Removed superfluous semicolon.Bernhard Schommer2017-02-141-1/+1
|/ / /
generated by cgit (git 2.34.1) at 2024-06-30 23:30:23 +0000