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
...
*
Error when calling un-prototyped function.
xleroy
2013-03-25
1
-6
/
+8
*
Better locations for error messages relative to type specifiers.
xleroy
2013-03-25
1
-14
/
+9
*
Watch out for behaviors exponential in the nesting of struct/union types.
xleroy
2013-03-23
6
-66
/
+78
*
RTLtyping: now performed entirely in Coq, no need for an external Caml oracle...
xleroy
2013-03-22
3
-374
/
+713
*
Update clightgen to changes in Camlcoq and in AST.
xleroy
2013-03-20
2
-15
/
+33
*
Diab asm syntax issue
xleroy
2013-03-20
1
-1
/
+1
*
For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a ...
xleroy
2013-03-18
2
-3
/
+13
*
Remove the C primitives for unsigned long long arithmetic, replaced
xleroy
2013-03-18
4
-53
/
+25
*
More aggressive CSE across Ibuiltin.
xleroy
2013-03-17
3
-7
/
+36
*
Assorted changes to reduce stack and heap requirements when compiling very bi...
xleroy
2013-03-16
35
-237
/
+534
*
Machsem: no longer useful.
xleroy
2013-03-14
1
-259
/
+0
*
Bind some local defs with Let, makes extracted code cleaner
v1.13
xleroy
2013-03-12
1
-2
/
+2
*
Maps: revised TREE interface; added mucho derived properties and operations i...
xleroy
2013-03-12
2
-63
/
+256
*
Suppress int64_unsigned_to_float, now unused.
xleroy
2013-03-11
2
-7
/
+0
*
More updates for 1.13
xleroy
2013-03-11
1
-2
/
+5
*
Fixed parsing of hex float literals 0xNNNpMMM.
xleroy
2013-03-11
5
-4
/
+81
*
Updated for version 1.13
xleroy
2013-03-11
2
-11
/
+24
*
Updating doc for 1.13
xleroy
2013-03-11
1
-8
/
+5
*
Useless Import
xleroy
2013-03-10
1
-1
/
+0
*
Glasnost: making transparent a number of definitions that were opaque
xleroy
2013-03-10
29
-120
/
+133
*
Assorted cleanups, esp. to avoid generating _rec and _rect recursors in
xleroy
2013-03-09
10
-215
/
+260
*
Improving the performance of exhaustive exploration (mode -all):
xleroy
2013-03-09
1
-18
/
+112
*
Finished backtracking (cf previous commit) for ARM and PowerPC.
xleroy
2013-03-04
7
-815
/
+593
*
Partial backtracking on previous commit: the "hole in Mach stack frame"
xleroy
2013-03-03
7
-857
/
+757
*
Updates to follow recent changes in PrintAsm.ml
xleroy
2013-03-01
1
-14
/
+43
*
Some builtins were renamed, updating
xleroy
2013-03-01
1
-4
/
+4
*
Bug in Pbtbl
xleroy
2013-03-01
1
-1
/
+1
*
No longer a dependency on Machtyping
xleroy
2013-03-01
2
-2
/
+1
*
Fix 'interp' entry
xleroy
2013-03-01
1
-1
/
+1
*
Testing dense switches
xleroy
2013-03-01
3
-1
/
+62
*
Revised Stacking and Asmgen passes and Mach semantics:
xleroy
2013-03-01
26
-7039
/
+4809
*
Updated ARM and PowerPC ports with new handling of __builtin_annot.
xleroy
2013-02-24
9
-90
/
+93
*
Constant propagation within __builtin_annot.
xleroy
2013-02-24
15
-124
/
+250
*
Pointers one past
xleroy
2013-02-15
21
-324
/
+565
*
Updated PowerPC port to new integers.
xleroy
2013-02-12
8
-29
/
+59
*
Be more like gcc in the way we display or not the usage message.
xleroy
2013-02-12
1
-8
/
+6
*
Forgot theorem "sign_ext_narrow".
xleroy
2013-02-12
1
-0
/
+12
*
lib/Integers.v: revised and extended, faster implementation based on
xleroy
2013-02-10
11
-1450
/
+1733
*
Some more properties. Refactored some proofs.
xleroy
2013-02-04
1
-21
/
+107
*
Typo in compare_mem causing merging of different states.
xleroy
2013-02-02
1
-1
/
+1
*
Errors for excessively large global variables or stack frames.
xleroy
2013-02-02
6
-14
/
+17
*
Camlcoq.ml: bug in conversion Z to string
v1.12.1
xleroy
2013-01-29
2
-4
/
+4
*
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
xleroy
2013-01-29
69
-1024
/
+1173
*
Updated documentation
v1.12
xleroy
2013-01-11
3
-15
/
+15
*
Update for release 1.12
xleroy
2013-01-09
4
-9
/
+27
*
Quote idents for safe re-parsing
xleroy
2013-01-08
1
-1
/
+1
*
Updated to new external functions and new representation of programs
xleroy
2013-01-08
1
-4
/
+15
*
More correct exportclight/ dependencies
xleroy
2013-01-08
2
-8
/
+9
*
Avoid generating some obviously useless casts.
xleroy
2013-01-08
2
-2
/
+36
*
Better treatment of volatile accesses in the reference interpreter.
xleroy
2013-01-08
2
-68
/
+83
[prev]
[next]