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
*
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
*
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
[next]