index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
backend
/
Selectionproof.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...
David Monniaux
2019-09-20
1
-2
/
+2
|
\
|
*
AArch64 port
Xavier Leroy
2019-08-08
1
-2
/
+2
*
|
various fixes
David Monniaux
2019-07-19
1
-3
/
+3
*
|
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...
David Monniaux
2019-07-19
1
-36
/
+125
|
\
|
|
*
Give formal semantics to some built-in functions and run-time functions
Xavier Leroy
2019-07-17
1
-34
/
+123
|
*
If-conversion optimization
Xavier Leroy
2019-06-06
1
-63
/
+323
*
|
Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...
David Monniaux
2019-06-03
1
-67
/
+327
|
\
\
|
*
|
If-conversion optimization
Xavier Leroy
2019-05-31
1
-63
/
+323
|
|
/
|
*
lib/Coqlib.v: remove defns about multiplication, division, modulus
Xavier Leroy
2019-04-23
1
-1
/
+1
|
*
Fix typo in section name in Selectionproof.v
Alix Trieu
2019-04-15
1
-2
/
+2
*
|
itemize the proof (better for debugging)
David Monniaux
2019-04-05
1
-10
/
+10
*
|
removed the unproved hack to get builtins, will be reinstated later
David Monniaux
2019-04-05
1
-6
/
+0
*
|
some more on builtins
David Monniaux
2019-04-03
1
-0
/
+6
*
|
ça recompile sur x86
David Monniaux
2019-03-22
1
-0
/
+1
*
|
Proof of div32/mod32/divf32/divf64 lemmas
Cyril SIX
2019-03-20
1
-3
/
+3
|
/
*
Merge pull request #191 from sigurdschneider/master
Xavier Leroy
2017-10-20
1
-0
/
+1
|
\
|
*
Ensure FunInd or Recdef is imported if functional induction is used
Sigurd Schneider
2017-07-20
1
-0
/
+1
*
|
Remove coq warnings (#28)
Bernhard Schommer
2017-09-22
1
-3
/
+3
|
/
*
Hybrid 64bit/32bit PowerPC port
Bernhard Schommer
2017-05-03
1
-25
/
+38
*
Improve code generation for 64-bit signed integer division
Xavier Leroy
2016-10-02
1
-2
/
+2
*
Support for 64-bit architectures: generic support
Xavier Leroy
2016-10-01
1
-100
/
+57
*
Port to Coq 8.5pl2
Xavier Leroy
2016-07-08
1
-2
/
+2
*
Update the back-end proofs to the new linking framework.
Xavier Leroy
2016-03-06
1
-231
/
+329
*
Updated PR by removing whitespaces. Bug 17450.
Bernhard Schommer
2015-10-20
1
-118
/
+118
*
Use Coq strings instead of idents to name external and builtin functions.
Xavier Leroy
2015-10-11
1
-52
/
+110
*
Refactoring of builtins and annotations in the back-end.
Xavier Leroy
2015-08-21
1
-55
/
+38
*
Merge pull request #34 from AbsInt/extended-annotations
Xavier Leroy
2015-04-01
1
-2
/
+71
|
\
|
*
Updated the Caml part. Added some more tests in annot1.c.
Xavier Leroy
2015-03-27
1
-5
/
+26
|
*
Extend annotations so that they can keep track of global variables and local ...
Xavier Leroy
2015-03-27
1
-2
/
+50
*
|
Revised semantics of comparisons between a pointer and 0.
Xavier Leroy
2015-03-15
1
-1
/
+1
|
/
*
Protect against redefinition of the __i64_xxx helper library functions.
Xavier Leroy
2015-01-20
1
-57
/
+57
*
Add Genv.public_symbol operation.
Xavier Leroy
2014-11-24
1
-6
/
+12
*
- Support "switch" statements over 64-bit integers
xleroy
2014-08-17
1
-123
/
+336
*
Merge of "newspilling" branch:
xleroy
2014-07-23
1
-0
/
+15
*
Refactoring: move symbol_offset into Genv.
xleroy
2014-05-24
1
-1
/
+1
*
Optimize integer divisions by positive constants, turning them into
xleroy
2013-07-29
1
-0
/
+2
*
Treat casts int64 -> float32 as primitive operations instead of two
xleroy
2013-07-03
1
-0
/
+2
*
Expand 64-bit integer comparisons into 32-bit integer comparisons.
xleroy
2013-04-29
1
-19
/
+13
*
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
xleroy
2013-04-20
1
-90
/
+162
*
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
xleroy
2013-01-29
1
-3
/
+3
*
Remove some useless "Require".
xleroy
2012-12-30
1
-1
/
+0
*
Merge of the clightgen branch:
xleroy
2012-12-29
1
-2
/
+1
*
Merge of branch seq-and-or. See Changelog for details.
xleroy
2012-10-06
1
-126
/
+18
*
Remove Val.is_true and Val.is_false, no longer used.
xleroy
2012-08-06
1
-16
/
+6
*
CSE: add recognition of some combined operators, conditions, and addressing m...
xleroy
2012-05-26
1
-2
/
+2
*
Merge of the newmem branch:
xleroy
2012-05-21
1
-24
/
+43
*
Proof didn't go through for ARM
xleroy
2012-03-11
1
-2
/
+2
*
Take advantage of Cmaskzero and Cmasknotzero.
xleroy
2012-02-24
1
-10
/
+10
*
Merge of the "volatile" branch:
xleroy
2012-02-04
1
-0
/
+10
*
Merge of the nonstrict-ops branch:
xleroy
2012-01-14
1
-138
/
+288
[next]