index
:
compcert
FPcomp
aarch64
conditional-move
dev/michalis
floatofintu
inl-cse-const
master
no-pervasives
CompCert fork with minor modifications for Vericert.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
*
Assert instead of unit.
Bernhard Schommer
2017-04-10
1
-6
/
+6
*
Filter out functions earlier. Bug 21343
Bernhard Schommer
2017-04-10
1
-24
/
+27
*
Fix name of function. Bug 21378
Bernhard Schommer
2017-04-07
1
-1
/
+1
*
Do not generate code for "inline definitions"
Bernhard Schommer
2017-04-07
3
-30
/
+41
*
Add optimization option finline.
Bernhard Schommer
2017-04-07
4
-1
/
+8
*
Another optimization of empty if/else and other useless conditional branches
Xavier Leroy
2017-04-06
2
-31
/
+41
*
attempt to optimize empty if/then/else statements
Michael Schmidt
2017-04-06
3
-7
/
+32
*
Replace 'decide equality' in powerpc/Op.v. Bug 21332
Bernhard Schommer
2017-04-03
1
-4
/
+5
*
Update the "make check-proof" entry for Coq 8.6
Xavier Leroy
2017-03-24
1
-3
/
+2
*
Added handling if s.sloc <> s1.sloc
Bernhard Schommer
2017-03-24
1
-2
/
+6
*
Emit line stmt after labels in general. Bug 21232
Bernhard Schommer
2017-03-24
1
-10
/
+6
*
Do not emit line info before case stmt.
Bernhard Schommer
2017-03-24
1
-4
/
+9
*
use 'f' as generic function-identifier instead of arbitraty identifier 1 for ...
Michael Schmidt
2017-03-23
1
-1
/
+1
*
Better fix for problems with quoting in files.
Bernhard Schommer
2017-03-20
2
-4
/
+4
*
Quote directory for comp_dir entry.
Bernhard Schommer
2017-03-20
1
-2
/
+2
*
Merge pull request #175 from silene/IZR
Xavier Leroy
2017-03-08
15
-150
/
+121
|
\
|
*
Adapt proofs to future handling of literal constants in Coq.
Guillaume Melquiond
2017-03-08
15
-150
/
+121
*
|
Added missing dltl to dall.
Bernhard Schommer
2017-03-08
1
-0
/
+1
|
/
*
Add a switch to generate a _CoqProject file.
Bernhard Schommer
2017-02-23
2
-1
/
+24
*
Added check for large arrays.
Bernhard Schommer
2017-02-21
3
-0
/
+14
*
update manpage for new options
Michael Schmidt
2017-02-21
1
-4
/
+16
*
Added gcc noinline attribute.
Bernhard Schommer
2017-02-19
2
-0
/
+2
*
Added unused attribute and simplified checks.
Bernhard Schommer
2017-02-17
2
-44
/
+84
*
Adopted unused variable and attribtue check
Bernhard Schommer
2017-02-17
3
-31
/
+55
*
Extended unused vars check for params.
Bernhard Schommer
2017-02-17
3
-2
/
+9
*
Added a simple check for unused variables.
Bernhard Schommer
2017-02-17
5
-2
/
+88
*
Checks can be applied add several places.
Bernhard Schommer
2017-02-17
3
-8
/
+5
*
Also check the locals. Bug 19872.
Bernhard Schommer
2017-02-17
1
-3
/
+7
*
Added new module for checks on elaborated C code
Bernhard Schommer
2017-02-17
3
-2
/
+114
*
Do not optimize away the 'return 0' at end of 'main'
Xavier Leroy
2017-02-17
1
-7
/
+5
*
Control-flow analysis: bug in switch without default
Xavier Leroy
2017-02-17
1
-1
/
+30
*
Merge pull request #172 from AbsInt/std_noreturn_fun
Xavier Leroy
2017-02-17
3
-3
/
+14
|
\
|
*
Added _exit.
Bernhard Schommer
2017-02-17
1
-1
/
+1
|
*
Add longjmp. Bug 21009
Bernhard Schommer
2017-02-17
1
-1
/
+1
|
*
Added handling for noreturn std functions.
Bernhard Schommer
2017-02-16
3
-3
/
+14
|
/
*
Reverted changes in Cutil and catch in Cflow.
Bernhard Schommer
2017-02-16
2
-17
/
+5
*
Fixed problem with local structs/unions in Cflow.
Bernhard Schommer
2017-02-16
1
-4
/
+17
*
drop .cm support from man page
Michael Schmidt
2017-02-15
1
-4
/
+0
*
Merge pull request #167 from AbsInt/pipe_prerequisite
Xavier Leroy
2017-02-15
8
-35
/
+27
|
\
|
*
Introduced configuration variable for gnu systems.
Bernhard Schommer
2017-02-13
8
-35
/
+27
*
|
Merge pull request #162 from AbsInt/return-analysis-2
Xavier Leroy
2017-02-15
5
-32
/
+290
|
\
\
|
*
|
Cflow: analysis of "switch" was too imprecise
Xavier Leroy
2017-02-07
1
-2
/
+3
|
*
|
Revised, more precise implementation of control-flow analysis
Xavier Leroy
2017-02-07
1
-48
/
+98
|
*
|
Control-flow analysis: wrong flow for "case"/"default" statements
Xavier Leroy
2017-02-07
1
-4
/
+6
|
*
|
More precise warnings about function returns
Xavier Leroy
2017-02-07
5
-32
/
+237
*
|
|
Remove tests involving Cminor concrete syntax. Update Changelog
Xavier Leroy
2017-02-15
29
-3336
/
+3
*
|
|
Merge pull request #170 from AbsInt/remove_cminor
Xavier Leroy
2017-02-15
9
-1379
/
+3
|
\
\
\
|
*
|
|
Removed CMinor import. Bug 20992
Bernhard Schommer
2017-02-14
9
-1379
/
+3
*
|
|
|
Removed superfluous semicolon.
Bernhard Schommer
2017-02-14
1
-1
/
+1
|
/
/
/
*
|
|
Remove Optionsprinter. Bug 20993
Bernhard Schommer
2017-02-14
2
-155
/
+1
[next]