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
...
*
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
*
Update Cminor parser and printer so that the parser can parse the whole Cmino...
xleroy
2013-01-07
5
-38
/
+107
*
Put clighgen files in exportclight/
xleroy
2013-01-05
6
-44
/
+99
*
Print Swhile loops. Fix indentation.
xleroy
2013-01-05
1
-8
/
+12
*
RTLgenaux: heuristic to orient if-then-else statements based on sizes.
xleroy
2012-12-31
2
-3
/
+62
*
Remove some useless "Require".
xleroy
2012-12-30
85
-235
/
+73
*
Make "all" the defaut target.
xleroy
2012-12-29
1
-18
/
+21
*
Merge of the clightgen branch:
xleroy
2012-12-29
34
-2718
/
+4800
*
Fix "clean" rule.
xleroy
2012-12-29
1
-1
/
+1
*
Composition properties between injections and extensions.
xleroy
2012-12-29
1
-8
/
+80
*
Integers: specialized function to compute x mod 2^N; used in "repr" to
xleroy
2012-12-21
2
-115
/
+179
*
Separate interference graphs for ints and floats, i.e. don't record interfere...
xleroy
2012-12-20
1
-13
/
+16
*
Test bitfields of enum type
xleroy
2012-12-18
2
-0
/
+28
*
Support for inline assembly (asm statements).
xleroy
2012-12-18
28
-76
/
+259
*
Test for __builtin_fcti
xleroy
2012-11-24
1
-1
/
+3
*
Add __builtin_fcti (double -> int conversion w/ round to nearest)
xleroy
2012-11-24
2
-0
/
+9
*
Globalenvs: allocate one-byte block with permissions Nonempty for each
xleroy
2012-11-12
38
-1637
/
+1301
*
Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)
xleroy
2012-11-03
14
-95
/
+180
*
Update cparser/Makefile (fix by Jacques-Henri Jourdan)
xleroy
2012-11-03
2
-28
/
+28
*
Clight: split off the big step semantics in ClightBigstep.
xleroy
2012-10-14
5
-563
/
+695
*
Generate output files in current directory; can be overriden with -o option
xleroy
2012-10-08
3
-34
/
+65
*
Make Clight independent of CompCert C.
xleroy
2012-10-08
22
-1385
/
+1522
[prev]
[next]