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
/
Selectionproof.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
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
*
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
*
Merge of branch new-semantics: revised and strengthened top-level statements ...
xleroy
2011-07-15
1
-4
/
+3
*
Merge of branch "unsigned-offsets":
xleroy
2011-04-09
1
-13
/
+16
*
Float.intoffloat and Float.intuoffloat are now partial functions.
xleroy
2010-10-28
1
-2
/
+2
*
Support for inlined built-ins.
xleroy
2010-06-29
1
-34
/
+91
*
More faithful semantics for volatile reads and writes.
xleroy
2010-05-23
1
-1
/
+9
*
- Extended traces so that pointers within globals are supported as event values.
xleroy
2010-05-10
1
-0
/
+4
*
Merge of the newmem and newextcalls branches:
xleroy
2010-03-07
1
-8
/
+9
*
Revised lib/Integers.v to make it parametric w.r.t. word size.
xleroy
2009-11-19
1
-3
/
+3
*
Forgot to add some files
xleroy
2009-08-18
1
-0
/
+505
*
Reorganized the development, modularizing away machine-dependent parts.
xleroy
2008-12-30
1
-1398
/
+0
*
Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.
xleroy
2008-12-29
1
-8
/
+12
*
Revised back-end so that only 2 integer registers are reserved for reloading.
xleroy
2008-12-21
1
-1
/
+1
*
Flag to turn on/off the recognition of fused multiply-add and multiply-sub
xleroy
2008-07-31
1
-6
/
+9
[next]