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
path:
root
/
backend
/
Kildall.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
bug 17392: remove trailing whitespace in source files
Michael Schmidt
2015-10-14
1
-162
/
+162
*
Merge of branch value-analysis.
xleroy
2013-12-20
1
-427
/
+740
*
Change interface of Kildall solvers to avoid precomputing the map pc -> list ...
xleroy
2013-08-12
1
-201
/
+266
*
Assorted cleanups, esp. to avoid generating _rec and _rect recursors in
xleroy
2013-03-09
1
-0
/
+4
*
Various algorithmic improvements that reduce compile times (thanks Alexandre ...
xleroy
2010-10-27
1
-42
/
+28
*
Cil2Csyntax: added goto and labels; added assignment between structs
xleroy
2009-08-16
1
-203
/
+264
*
Adapted to work with Coq 8.2-1
v1.4.1
xleroy
2009-06-05
1
-5
/
+5
*
Ajout license, README, copyright notices
xleroy
2008-01-27
1
-0
/
+12
*
Typo dans le pseudocode en commentaire
xleroy
2007-10-17
1
-1
/
+1
*
Importer OrderedPositive depuis Ordered.v
xleroy
2007-03-05
1
-30
/
+1
*
Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...
xleroy
2007-03-02
1
-11
/
+20
*
Meilleure representation des worklists dans l'algo de Kildall
xleroy
2006-09-11
1
-65
/
+206
*
Fusion de la branche "traces":
xleroy
2006-09-04
1
-214
/
+66
*
Initial import of compcert
xleroy
2006-02-09
1
-0
/
+1231