index
:
debian-compcert
master
pristine-tar
upstream
Debian packaging for CompCert
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Some more properties. Refactored some proofs.
xleroy
2013-02-04
*
Typo in compare_mem causing merging of different states.
xleroy
2013-02-02
*
Errors for excessively large global variables or stack frames.
xleroy
2013-02-02
*
Camlcoq.ml: bug in conversion Z to string
xleroy
2013-01-29
*
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
xleroy
2013-01-29
*
Updated documentation
xleroy
2013-01-11
*
Update for release 1.12
xleroy
2013-01-09
*
Quote idents for safe re-parsing
xleroy
2013-01-08
*
Updated to new external functions and new representation of programs
xleroy
2013-01-08
*
More correct exportclight/ dependencies
xleroy
2013-01-08
*
Avoid generating some obviously useless casts.
xleroy
2013-01-08
*
Better treatment of volatile accesses in the reference interpreter.
xleroy
2013-01-08
*
Update Cminor parser and printer so that the parser can parse the whole Cmino...
xleroy
2013-01-07
*
Put clighgen files in exportclight/
xleroy
2013-01-05
*
Print Swhile loops. Fix indentation.
xleroy
2013-01-05
*
RTLgenaux: heuristic to orient if-then-else statements based on sizes.
xleroy
2012-12-31
*
Remove some useless "Require".
xleroy
2012-12-30
*
Make "all" the defaut target.
xleroy
2012-12-29
*
Merge of the clightgen branch:
xleroy
2012-12-29
*
Fix "clean" rule.
xleroy
2012-12-29
*
Composition properties between injections and extensions.
xleroy
2012-12-29
*
Integers: specialized function to compute x mod 2^N; used in "repr" to
xleroy
2012-12-21
*
Separate interference graphs for ints and floats, i.e. don't record interfere...
xleroy
2012-12-20
*
Test bitfields of enum type
xleroy
2012-12-18
*
Support for inline assembly (asm statements).
xleroy
2012-12-18
*
Test for __builtin_fcti
xleroy
2012-11-24
*
Add __builtin_fcti (double -> int conversion w/ round to nearest)
xleroy
2012-11-24
*
Globalenvs: allocate one-byte block with permissions Nonempty for each
xleroy
2012-11-12
*
Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)
xleroy
2012-11-03
*
Update cparser/Makefile (fix by Jacques-Henri Jourdan)
xleroy
2012-11-03
*
Clight: split off the big step semantics in ClightBigstep.
xleroy
2012-10-14
*
Generate output files in current directory; can be overriden with -o option
xleroy
2012-10-08
*
Make Clight independent of CompCert C.
xleroy
2012-10-08
*
Merge of branch seq-and-or. See Changelog for details.
xleroy
2012-10-06
*
Fixed 2 errors in revised builtin_vstore.
xleroy
2012-08-22
*
Wrong usage of temps in builtin_volatile_write.
xleroy
2012-08-17
*
Define useful functions instr_defs and instr_uses
xleroy
2012-08-10
*
Remove Val.is_true and Val.is_false, no longer used.
xleroy
2012-08-06
*
Updated documentation
xleroy
2012-08-02
*
Removed old, commented-out definitions.
xleroy
2012-08-01
*
More aggressive elimination of conditional branches during constant
xleroy
2012-08-01
*
Forgot to collect types of expressions
xleroy
2012-07-28
*
- Revised non-overflow constraints on memory injections so that
xleroy
2012-07-23
*
Remove the PowerPC/MacOS X port, as MacOS no longer supports PowerPC.
xleroy
2012-07-14
*
Support for indirect symbols under MacOS X (final).
xleroy
2012-07-14
*
Support for MacOS X's indirect symbols. (first try)
xleroy
2012-07-13
*
Late update for 1.11
xleroy
2012-07-13
*
Preparation for release 1.11
xleroy
2012-07-13
*
checklink: dead and debug code elimination
varobert
2012-07-12
*
checklink: simplifications
varobert
2012-07-12
[prev]
[next]