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
/
arm
Commit message (
Expand
)
Author
Age
Files
Lines
*
Pretty strings
xleroy
2010-03-29
1
-3
/
+8
*
Updated ARM asm printer
xleroy
2010-03-28
1
-4
/
+67
*
Updating ARM port
xleroy
2010-03-28
4
-61
/
+41
*
Handling of volatile accesses through builtin functions.
xleroy
2010-03-08
1
-0
/
+27
*
Merge of the newmem and newextcalls branches:
xleroy
2010-03-07
9
-27
/
+27
*
Suppressed Init_pointer, now useless. Improved printing of strings in genera...
xleroy
2010-03-03
1
-17
/
+1
*
Updated ARM asm printer
xleroy
2010-01-25
1
-5
/
+10
*
Updated ARM port
xleroy
2010-01-25
1
-2
/
+4
*
Revised lib/Integers.v to make it parametric w.r.t. word size.
xleroy
2009-11-19
6
-53
/
+53
*
Added support for jump tables.
xleroy
2009-11-19
4
-1
/
+87
*
PowerPC/EABI port: preliminary support for #pragma section and
xleroy
2009-11-03
4
-75
/
+59
*
Support Clight initializers of the form "int * x = &y;".
xleroy
2009-11-01
1
-0
/
+2
*
Declaration of use_fused_mul, unused in this port but needed for extraction (...
xleroy
2009-08-18
1
-0
/
+4
*
"val_match_approx_increasing" moved from mach-dep part to mach-indep part.
xleroy
2009-08-18
1
-11
/
+0
*
Refactoring of Constprop and Constpropproof into a machine-dependent part and...
xleroy
2009-08-17
2
-667
/
+48
*
Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...
xleroy
2009-08-17
2
-766
/
+94
*
Cil2Csyntax: added goto and labels; added assignment between structs
xleroy
2009-08-16
2
-37
/
+19
*
Added 'going wrong' behaviors
xleroy
2009-08-05
3
-3
/
+3
*
Adapted to work with Coq 8.2-1
v1.4.1
xleroy
2009-06-05
7
-56
/
+52
*
Various clean-ups
v1.4
xleroy
2009-04-17
1
-2
/
+1
*
Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...
xleroy
2009-01-29
1
-1
/
+0
*
Elimination of "alloc" instruction in Caml files and test files.
xleroy
2009-01-11
1
-2
/
+0
*
- Added alignment constraints to memory loads and stores.
xleroy
2009-01-11
10
-424
/
+128
*
Cminor, CminorSel: removed useless premises in rules for Sreturn
xleroy
2009-01-04
1
-2
/
+2
*
Continuation of ARM port.
xleroy
2009-01-01
5
-30
/
+1209
*
Reorganized the development, modularizing away machine-dependent parts.
xleroy
2008-12-30
12
-0
/
+10625