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
...
*
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
*
|
|
Release 3.0.1 here we come
v3.0.1
Xavier Leroy
2017-02-14
2
-1
/
+7
*
|
|
Give explicit scopes to notations a#b and a##b and a#b<-c
Xavier Leroy
2017-02-13
4
-13
/
+21
*
|
|
Turn warning "deprecated-implicit-arguments" off while compiling Flocq
Xavier Leroy
2017-02-13
1
-1
/
+4
*
|
|
Replace "Implicit Arguments" with "Arguments"
Xavier Leroy
2017-02-13
8
-19
/
+17
*
|
|
Use "Local" as prefix
Xavier Leroy
2017-02-13
22
-38
/
+36
*
|
|
ARM, PowerPC: update Asmgenproof for Coq 8.6
Xavier Leroy
2017-02-13
2
-14
/
+21
*
|
|
Update Flocq to version 2.5.2
Xavier Leroy
2017-02-13
8
-132
/
+91
*
|
|
Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into maxime...
Xavier Leroy
2017-02-13
9
-19
/
+22
|
\
\
\
|
|
_
|
/
|
/
|
|
|
*
|
Bump required version of Menhir to 20161201.
Maxime Dénès
2017-01-09
1
-1
/
+1
[prev]
[next]