Commits

Breadcrumbs

History for

onmaster

User selector

All users

All time

Commit History

Commits on Jan 23, 2015

• Merge branch 'named-structs'

  Show description for d594c5d
  xavierleroy

  committed
  d594c5d

  Copy full SHA for d594c5d

Commits on Jan 20, 2015

• Protect against redefinition of the __i64_xxx helper library functions.

  Show description for 9f2ca10
  xavierleroy

  committed
  9f2ca10

  Copy full SHA for 9f2ca10

Commits on Dec 31, 2014

• Add a type system for CompCert C and type-checking constructor functions.

  Show description for 67b13ec
  xavierleroy

  committed
  67b13ec

  Copy full SHA for 67b13ec

Commits on Dec 22, 2014

• Represent struct and union types by name instead of by structure.

  xavierleroy

  committed
  e89f1e6

  Copy full SHA for e89f1e6

Commits on Nov 16, 2014

• Add flags to control individual optimization passes + flag -O0 for turning them off.

  xavierleroy

  committed
  bda5ee2

  Copy full SHA for bda5ee2

Commits on Sep 29, 2014

• Moved the timing facility to a seperate file.

  bschommer

  committed
  e5b59af

  Copy full SHA for e5b59af

Commits on Sep 21, 2014

• Add .gitignore files.

  xavierleroy

  committed
  0899260

  Copy full SHA for 0899260

Commits on Aug 19, 2014

• Rename "-fthumb" option into "-mthumb" for GCC compatibility.

  Show description for c58233b
  

  xleroy

  committed
  c58233b

  Copy full SHA for c58233b

Commits on Aug 17, 2014

• - Support "switch" statements over 64-bit integers

  Show description for 17f5196
  

  xleroy

  committed
  17f5196

  Copy full SHA for 17f5196

Commits on Jul 28, 2014

• PowerPC port: refactored the expansion of built-in functions and

  Show description for 04d0d60
  

  xleroy

  committed
  04d0d60

  Copy full SHA for 04d0d60

Commits on Jul 27, 2014

• ARM port: add support for Thumb2. To be tested.

  Show description for f4e106d
  

  xleroy

  committed
  f4e106d

  Copy full SHA for f4e106d

Commits on May 12, 2014

• Assorted fixes to fix parsing issues and be more GCC-like:

  Show description for edc00e0
  

  xleroy

  committed
  edc00e0

  Copy full SHA for edc00e0

Commits on Apr 29, 2014

• Integration of Jacques-Henri Jourdan's verified parser.

  Show description for f1d236b
  

  xleroy

  committed
  f1d236b

  Copy full SHA for f1d236b

Commits on Apr 23, 2014

• Clean-up pass on C types:

  Show description for 2f643e4
  

  xleroy

  committed
  2f643e4

  Copy full SHA for 2f643e4

Commits on Apr 6, 2014

• Merge of branch linear-typing:

  Show description for 56579f8
  

  xleroy

  committed
  56579f8

  Copy full SHA for 56579f8

Commits on Feb 23, 2014

• In Regalloc, dead code elimination, don't eliminate move operations

  Show description for 11db383
  

  xleroy

  committed
  11db383

  Copy full SHA for 11db383

Commits on Feb 19, 2014

• Add option -Os to optimize for code size rather than for execution speed.

  Show description for 3ec0229
  

  xleroy

  committed
  3ec0229

  Copy full SHA for 3ec0229

Commits on Jan 12, 2014

• - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.

  Show description for 7998ccf
  

  xleroy

  committed
  7998ccf

  Copy full SHA for 7998ccf

Commits on Jan 3, 2014

• Introduce and use the platform-specific Archi module giving:

  Show description for 362f2f3
  

  xleroy

  committed
  362f2f3

  Copy full SHA for 362f2f3

Commits on Dec 20, 2013

• Merge of branch value-analysis.

  Show description for 7698300
  

  xleroy

  committed
  7698300

  Copy full SHA for 7698300

Commits on Nov 18, 2013

• Revised semantics of external functions, continued:

  Show description for 726c815
  

  xleroy

  committed
  726c815

  Copy full SHA for 726c815

Commits on Nov 17, 2013

• Revised modeling of external functions and built-in functions: just axiomatize

  Show description for 0be44be
  

  xleroy

  committed
  0be44be

  Copy full SHA for 0be44be

Commits on Sep 14, 2013

• Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms

  Show description for 76ea110
  

  xleroy

  committed
  76ea110

  Copy full SHA for 76ea110

Commits on Aug 2, 2013

• Merge of Flocq version 2.2.0.

  Show description for 4ee0544
  

  xleroy

  committed
  4ee0544

  Copy full SHA for 4ee0544

Commits on May 17, 2013

• Add option -fno-tailcalls to turn off tailcall elimination (causes problem with some static analysis tools).

  Show description for a3f1744
  

  xleroy

  committed
  a3f1744

  Copy full SHA for a3f1744

Commits on May 1, 2013

• Oops, removed a crucial declaration for Allocation.

  Show description for 3a25338
  

  xleroy

  committed
  3a25338

  Copy full SHA for 3a25338

• Coq-defined equality functions for Allocation.

  Show description for 7717d9e
  

  xleroy

  committed
  7717d9e

  Copy full SHA for 7717d9e

Commits on Apr 20, 2013

• Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

  Show description for 255cee0
  

  xleroy

  committed
  255cee0

  Copy full SHA for 255cee0

Commits on Mar 22, 2013

• RTLtyping: now performed entirely in Coq, no need for an external Caml oracle + a validator.

  Show description for e57315d
  

  xleroy

  committed
  e57315d

  Copy full SHA for e57315d

Commits on Jan 29, 2013

• Ported to Coq 8.4pl1. Merge of branches/coq-8.4.

  Show description for 056068a
  

  xleroy

  committed
  056068a

  Copy full SHA for 056068a

Commits on Dec 29, 2012

• Merge of the clightgen branch:

  Show description for 8539759
  

  xleroy

  committed
  8539759

  Copy full SHA for 8539759

Commits on Jul 14, 2012

• Support for indirect symbols under MacOS X (final).

  Show description for bd85aba
  

  xleroy

  committed
  bd85aba

  Copy full SHA for bd85aba

Commits on Jul 13, 2012

• Support for MacOS X's indirect symbols. (first try)

  Show description for 48b839d
  

  xleroy

  committed
  48b839d

  Copy full SHA for 48b839d

Commits on Jun 28, 2012

• Use Flocq for floats

  Show description for 5312915
  

  xleroy

  committed
  5312915

  Copy full SHA for 5312915

Commits on May 21, 2012

• Merge of the newmem branch:

  Show description for 0053b1a
  

  xleroy

  committed
  0053b1a

  Copy full SHA for 0053b1a