summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Fix "clean" rule.Gravatar xleroy2012-12-29
* Composition properties between injections and extensions.Gravatar xleroy2012-12-29
* Integers: specialized function to compute x mod 2^N; used in "repr" toGravatar xleroy2012-12-21
* Separate interference graphs for ints and floats, i.e. don't record interfere...Gravatar xleroy2012-12-20
* Test bitfields of enum typeGravatar xleroy2012-12-18
* Support for inline assembly (asm statements).Gravatar xleroy2012-12-18
* Test for __builtin_fctiGravatar xleroy2012-11-24
* Add __builtin_fcti (double -> int conversion w/ round to nearest)Gravatar xleroy2012-11-24
* Globalenvs: allocate one-byte block with permissions Nonempty for eachGravatar xleroy2012-11-12
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)Gravatar xleroy2012-11-03
* Update cparser/Makefile (fix by Jacques-Henri Jourdan)Gravatar xleroy2012-11-03
* Clight: split off the big step semantics in ClightBigstep.Gravatar xleroy2012-10-14
* Generate output files in current directory; can be overriden with -o optionGravatar xleroy2012-10-08
* Make Clight independent of CompCert C.Gravatar xleroy2012-10-08
* Merge of branch seq-and-or. See Changelog for details.Gravatar xleroy2012-10-06
* Fixed 2 errors in revised builtin_vstore. Gravatar xleroy2012-08-22
* Wrong usage of temps in builtin_volatile_write.Gravatar xleroy2012-08-17
* Define useful functions instr_defs and instr_usesGravatar xleroy2012-08-10
* Remove Val.is_true and Val.is_false, no longer used.Gravatar xleroy2012-08-06
* Updated documentationGravatar xleroy2012-08-02
* Removed old, commented-out definitions.Gravatar xleroy2012-08-01
* More aggressive elimination of conditional branches during constantGravatar xleroy2012-08-01
* Forgot to collect types of expressionsGravatar xleroy2012-07-28
* - Revised non-overflow constraints on memory injections so that Gravatar xleroy2012-07-23
* Remove the PowerPC/MacOS X port, as MacOS no longer supports PowerPC.Gravatar xleroy2012-07-14
* Support for indirect symbols under MacOS X (final).Gravatar xleroy2012-07-14
* Support for MacOS X's indirect symbols. (first try)Gravatar xleroy2012-07-13
* Late update for 1.11Gravatar xleroy2012-07-13
* Preparation for release 1.11Gravatar xleroy2012-07-13
* checklink: dead and debug code eliminationGravatar varobert2012-07-12
* checklink: simplificationsGravatar varobert2012-07-12
* checklink: allow other number formats in configurationGravatar varobert2012-07-12
* checklink: minor fixesGravatar varobert2012-07-12
* checklink: configuration, indicate external symbolsGravatar varobert2012-07-12
* checklink: added configurabilityGravatar varobert2012-07-11
* checklink: more stringent compilationGravatar varobert2012-07-11
* Strip quotes from section names during #pragma parsing.Gravatar xleroy2012-07-11
* Updated ARM port.Gravatar xleroy2012-07-10
* Accept long double literals if -flongdouble is given.Gravatar xleroy2012-07-10
* checklink: fixed SDA inference, passes testGravatar varobert2012-07-10
* Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.Gravatar xleroy2012-07-09
* Revert unintentional commit #1955Gravatar xleroy2012-07-06
* checklink: minor changesGravatar varobert2012-07-05
* Ajout trunk CompCertGravatar blazy2012-07-04
* checklink: better diagnosisGravatar varobert2012-07-04
* checklink: some more debug tracingGravatar varobert2012-07-04
* checklink: more defensive is_paddingGravatar varobert2012-07-04
* checklink: fixed bits/bytes mistakeGravatar varobert2012-07-04
* Update CombineOp for arm and ia32.Gravatar xleroy2012-07-03
* checklink: adaptation to the new floatsGravatar varobert2012-07-03