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
*
Refactoring of Constprop and Constpropproof into a machine-dependent part and...
xleroy
2009-08-17
8
-1327
/
+776
*
Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...
xleroy
2009-08-17
8
-1548
/
+325
*
Cil2Csyntax: added goto and labels; added assignment between structs
xleroy
2009-08-16
24
-523
/
+608
*
Distinguish two kinds of nonterminating behaviors: silent divergence
xleroy
2009-08-16
10
-657
/
+916
*
Unionfind data structure, used in new implementation of backend/Tunneling
xleroy
2009-08-16
1
-0
/
+702
*
Update spill costs when coalescing
xleroy
2009-08-16
1
-2
/
+3
*
Added 'going wrong' behaviors
xleroy
2009-08-05
26
-273
/
+449
*
Transition semantics for Clight and Csharpminor
xleroy
2009-08-03
11
-2365
/
+3013
*
Use Extraction Blacklist
xleroy
2009-07-25
4
-21
/
+7
*
MAJ
xleroy
2009-07-15
1
-11
/
+12
*
message macosx en accord avec configure
blazy
2009-06-05
1
-1
/
+1
*
Adapted to work with Coq 8.2-1
v1.4.1
xleroy
2009-06-05
71
-852
/
+795
*
Various clean-ups
v1.4
xleroy
2009-04-17
9
-75
/
+61
*
Use Configuration.system
xleroy
2009-03-29
1
-28
/
+38
*
Update creation Configuration.ml
xleroy
2009-03-29
1
-1
/
+2
*
cil.patch dir now useless
xleroy
2009-03-29
0
-0
/
+0
*
Cleaned up configure script.
xleroy
2009-03-29
296
-1356
/
+82317
*
Bug with overflow in line numbers
xleroy
2009-03-29
1
-0
/
+24
*
Honor "static" modifier on C globals.
xleroy
2009-03-28
3
-32
/
+104
*
Update
xleroy
2009-03-26
1
-0
/
+25
*
Added tail call optimization pass
xleroy
2009-03-26
9
-9
/
+889
*
Optimize redundant casts after memory loads
xleroy
2009-02-27
2
-0
/
+58
*
New linearization heuristic
xleroy
2009-02-27
1
-32
/
+72
*
make install: ./ccomp au lieu de ../ccomp
blazy
2009-02-27
1
-1
/
+2
*
Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...
xleroy
2009-02-26
10
-39
/
+156
*
Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...
xleroy
2009-01-29
11
-34
/
+25
*
Elimination of "alloc" instruction in Caml files and test files.
xleroy
2009-01-11
8
-30
/
+4
*
- Added alignment constraints to memory loads and stores.
xleroy
2009-01-11
67
-1488
/
+719
*
Fixed unary minus
xleroy
2009-01-07
1
-1
/
+1
*
Test for int/float conversions
xleroy
2009-01-07
3
-1
/
+140
*
Updates
xleroy
2009-01-05
3
-33
/
+58
*
Endianness in tests
xleroy
2009-01-05
4
-2
/
+20
*
Cminor, CminorSel: removed useless premises in rules for Sreturn
xleroy
2009-01-04
4
-8
/
+4
*
Some cleanups
xleroy
2009-01-02
1
-1
/
+10
*
Wrong dependencies
xleroy
2009-01-02
1
-4
/
+6
*
Continuation of ARM port.
xleroy
2009-01-01
7
-38
/
+1226
*
Cleanup
xleroy
2008-12-31
1
-105
/
+0
*
Continuation of PowerPC/EABI port
xleroy
2008-12-31
4
-149
/
+375
*
Turn off generation of libcil.a, which is not correct with OCaml 3.11
xleroy
2008-12-31
1
-2
/
+11
*
Removed vfprintf, because it was causing portability problems
xleroy
2008-12-31
2
-6
/
+0
*
Reorganized the development, modularizing away machine-dependent parts.
xleroy
2008-12-30
66
-1221
/
+12137
*
Extract Coq lists to Caml lists.
xleroy
2008-12-29
13
-146
/
+112
*
Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.
xleroy
2008-12-29
15
-367
/
+844
*
Revised back-end so that only 2 integer registers are reserved for reloading.
xleroy
2008-12-21
22
-421
/
+795
*
Clight: ajout Econdition, suppression Eindex.
xleroy
2008-09-27
8
-47
/
+160
*
Update for release 1.3
xleroy
2008-08-11
1
-1
/
+2
*
New file
xleroy
2008-08-11
1
-0
/
+25
*
Update
v1.3
xleroy
2008-08-09
1
-2
/
+2
*
Changes 1.2 -> 1.3
xleroy
2008-08-09
1
-0
/
+42
*
Ajout nouveaux tests
xleroy
2008-08-09
52
-0
/
+8446
[next]