Commits · d2cf6277ac179c9e8432d4c11a79e9f906a19bbc · CertiCompil / Chamois-Arsene

Jan 29, 2013
- Camlcoq.ml: bug in conversion Z to string · d2cf6277
  xleroy authored 12 years ago
  View commits for tag v1.12.1 v1.12.1
  
  d2cf6277
- Ported to Coq 8.4pl1. Merge of branches/coq-8.4. · 056068ab
  xleroy authored 12 years ago
  056068ab
Jan 11, 2013
- Updated documentation · 34d58b78
  xleroy authored 12 years ago
  View commits for tag v1.12 v1.12
  
  34d58b78
Jan 09, 2013
- Update for release 1.12 · 93a33f71
  xleroy authored 12 years ago
  93a33f71
Jan 08, 2013
- Quote idents for safe re-parsing · fe983601
  xleroy authored 12 years ago
  fe983601
- Updated to new external functions and new representation of programs · d03cc7a4
  xleroy authored 12 years ago
  d03cc7a4
- More correct exportclight/ dependencies · 595c1e18
  xleroy authored 12 years ago
  595c1e18
- Avoid generating some obviously useless casts. · 0899bd69
  xleroy authored 12 years ago
  0899bd69
- Better treatment of volatile accesses in the reference interpreter. · f687301c
  xleroy authored 12 years ago
  f687301c
Jan 07, 2013
- Update Cminor parser and printer so that the parser can parse the whole Cminor... · 8e5f68c1
  xleroy authored 12 years ago
  8e5f68c1
Jan 05, 2013
- Put clighgen files in exportclight/ · 578cc2a5
  xleroy authored 12 years ago
  578cc2a5
- Print Swhile loops. Fix indentation. · ba8ad207
  xleroy authored 12 years ago
  ba8ad207
Dec 31, 2012
- RTLgenaux: heuristic to orient if-then-else statements based on sizes. · e72c8c43
  xleroy authored 12 years ago
  e72c8c43
Dec 30, 2012
- Remove some useless "Require". · 5bf13140
  xleroy authored 12 years ago
  5bf13140
Dec 29, 2012
- Make "all" the defaut target. · 71dfc9f2
  xleroy authored 12 years ago
  71dfc9f2
- Merge of the clightgen branch: · 85397590
  xleroy authored 12 years ago
  85397590
- Fix "clean" rule. · 7e9c6fc9
  xleroy authored 12 years ago
  7e9c6fc9
- Composition properties between injections and extensions. · 92b1c2aa
  xleroy authored 12 years ago
  92b1c2aa
Dec 21, 2012
- Integers: specialized function to compute x mod 2^N; used in "repr" to · 43974a16
  xleroy authored 12 years ago
  43974a16
Dec 20, 2012
- Separate interference graphs for ints and floats, i.e. don't record... · d4fe268a
  xleroy authored 12 years ago
  d4fe268a
Dec 18, 2012
- Test bitfields of enum type · 8ed2c113
  xleroy authored 12 years ago
  8ed2c113
- Support for inline assembly (asm statements). · 712f3cba
  xleroy authored 12 years ago
  712f3cba
Nov 24, 2012
- Test for __builtin_fcti · c6291611
  xleroy authored 12 years ago
  c6291611
- Add __builtin_fcti (double -> int conversion w/ round to nearest) · 09739ad7
  xleroy authored 12 years ago
  09739ad7
Nov 12, 2012
- Globalenvs: allocate one-byte block with permissions Nonempty for each · ce495154
  xleroy authored 12 years ago
  ce495154
Nov 03, 2012
- Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan) · dcb9f48f
  xleroy authored 12 years ago
  dcb9f48f
- Update cparser/Makefile (fix by Jacques-Henri Jourdan) · bd93aa7e
  xleroy authored 12 years ago
  bd93aa7e
Oct 14, 2012
- Clight: split off the big step semantics in ClightBigstep. · fccd14d2
  xleroy authored 12 years ago
  fccd14d2
Oct 08, 2012
- Generate output files in current directory; can be overriden with -o option · b7ece939
  xleroy authored 12 years ago
  b7ece939
- Make Clight independent of CompCert C. · c6d2ef0c
  xleroy authored 12 years ago
  c6d2ef0c
Oct 06, 2012
- Merge of branch seq-and-or. See Changelog for details. · f7693b3d
  xleroy authored 12 years ago
  f7693b3d
Aug 22, 2012
- Fixed 2 errors in revised builtin_vstore. · 261ef24f
  xleroy authored 12 years ago
  261ef24f
Aug 17, 2012
- Wrong usage of temps in builtin_volatile_write. · 9096c5c5
  xleroy authored 12 years ago
  9096c5c5
Aug 10, 2012
- Define useful functions instr_defs and instr_uses · 3b24f0e0
  xleroy authored 12 years ago
  3b24f0e0
Aug 06, 2012
- Remove Val.is_true and Val.is_false, no longer used. · 538f7ad4
  xleroy authored 12 years ago
  538f7ad4
Aug 02, 2012
- Updated documentation · f91e562a
  xleroy authored 12 years ago
  f91e562a
Aug 01, 2012
- Removed old, commented-out definitions. · f1ac5406
  xleroy authored 12 years ago
  f1ac5406
- More aggressive elimination of conditional branches during constant · f896088a
  xleroy authored 12 years ago
  f896088a
Jul 28, 2012
- Forgot to collect types of expressions · 5f61d897
  xleroy authored 12 years ago
  5f61d897
Jul 23, 2012
- - Revised non-overflow constraints on memory injections so that · 4297fcb8
  xleroy authored 12 years ago
  4297fcb8