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 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
|
*
|
Some backward compatible Ltac fixes, necessary for 8.6.
Maxime Dénès
2017-01-09
1
-5
/
+7
|
*
|
Fix broken fragile automation.
Maxime Dénès
2017-01-09
1
-1
/
+2
|
*
|
Configure now expects to find Coq 8.6.0.
Maxime Dénès
2017-01-09
1
-3
/
+3
|
*
|
Subst's behavior on let-ins has changed.
Maxime Dénès
2017-01-09
1
-2
/
+2
|
*
|
An hypothesis has changed name.
Maxime Dénès
2017-01-09
1
-1
/
+1
|
*
|
The contradiction tactic has become more powerful.
Maxime Dénès
2017-01-09
1
-2
/
+1
|
*
|
Intro patterns have changed semantics...
Maxime Dénès
2017-01-09
1
-0
/
+1
|
*
|
The subst tactic has become more powerful.
Maxime Dénès
2017-01-09
3
-4
/
+4
*
|
|
Release 3.0 here we come
v3.0
Xavier Leroy
2017-02-10
2
-2
/
+3
*
|
|
OS X: emit jumptables in .text segment, not .const segment
Xavier Leroy
2017-02-10
1
-1
/
+1
*
|
|
Use Printf.sprintf instead of Format.sprintf when possible
Xavier Leroy
2017-02-09
1
-4
/
+4
*
|
|
More tweaking of module 'open'
Xavier Leroy
2017-02-09
1
-8
/
+10
*
|
|
Merge branch 'master' of github.com:AbsInt/CompCert
Bernhard Schommer
2017-02-08
1
-0
/
+7
|
\
\
\
[next]