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
...
*
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
*
Merge of branch seq-and-or. See Changelog for details.
xleroy
2012-10-06
47
-2816
/
+2739
*
Fixed 2 errors in revised builtin_vstore.
xleroy
2012-08-22
1
-2
/
+3
*
Wrong usage of temps in builtin_volatile_write.
xleroy
2012-08-17
1
-12
/
+7
*
Define useful functions instr_defs and instr_uses
xleroy
2012-08-10
1
-0
/
+35
*
Remove Val.is_true and Val.is_false, no longer used.
xleroy
2012-08-06
5
-103
/
+74
*
Updated documentation
xleroy
2012-08-02
1
-28
/
+19
*
Removed old, commented-out definitions.
xleroy
2012-08-01
1
-292
/
+30
*
More aggressive elimination of conditional branches during constant
xleroy
2012-08-01
3
-201
/
+234
*
Forgot to collect types of expressions
xleroy
2012-07-28
2
-2
/
+6
*
- Revised non-overflow constraints on memory injections so that
xleroy
2012-07-23
38
-183
/
+331
*
Remove the PowerPC/MacOS X port, as MacOS no longer supports PowerPC.
xleroy
2012-07-14
4
-937
/
+21
*
Support for indirect symbols under MacOS X (final).
xleroy
2012-07-14
16
-112
/
+53
*
Support for MacOS X's indirect symbols. (first try)
xleroy
2012-07-13
10
-41
/
+102
*
Late update for 1.11
xleroy
2012-07-13
1
-4
/
+6
*
Preparation for release 1.11
v1.11
xleroy
2012-07-13
2
-6
/
+6
*
checklink: dead and debug code elimination
varobert
2012-07-12
2
-3
/
+0
*
checklink: simplifications
varobert
2012-07-12
2
-67
/
+73
*
checklink: allow other number formats in configuration
varobert
2012-07-12
1
-1
/
+1
*
checklink: minor fixes
varobert
2012-07-12
2
-7
/
+9
*
checklink: configuration, indicate external symbols
varobert
2012-07-12
3
-66
/
+84
*
checklink: added configurability
varobert
2012-07-11
3
-64
/
+180
*
checklink: more stringent compilation
varobert
2012-07-11
2
-2
/
+2
*
Strip quotes from section names during #pragma parsing.
xleroy
2012-07-11
4
-9
/
+9
*
Updated ARM port.
xleroy
2012-07-10
5
-29
/
+20
*
Accept long double literals if -flongdouble is given.
xleroy
2012-07-10
1
-1
/
+1
*
checklink: fixed SDA inference, passes test
varobert
2012-07-10
1
-6
/
+4
*
Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.
xleroy
2012-07-09
3
-16
/
+77
*
Revert unintentional commit #1955
xleroy
2012-07-06
5
-16
/
+12
*
checklink: minor changes
varobert
2012-07-05
1
-8
/
+9
*
Ajout trunk CompCert
blazy
2012-07-04
5
-12
/
+16
*
checklink: better diagnosis
varobert
2012-07-04
1
-112
/
+103
[prev]
[next]