summaryrefslogtreecommitdiff
path: root/README
Commit message (Collapse)AuthorAge
* Updates for release 2.2Gravatar xleroy2014-02-21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2415 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for release 1.12Gravatar xleroy2013-01-09
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2097 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Minor updatesGravatar xleroy2012-03-11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1848 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* UpdateGravatar xleroy2012-03-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1834 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "volatile" branch:Gravatar xleroy2012-02-04
| | | | | | | | | | | | - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).Gravatar xleroy2011-05-08
| | | | | | | | | | Added -dmach option and corresponding printer for Mach code. CleanupLabelsproof.v: fixed for ARM Driver.ml: -E sends output to stdout; support for .s and .S source files. cparser/Elab.ml: spurious comment deleted. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for 1.8.1 releaseGravatar xleroy2011-03-14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1607 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for release 1.8Gravatar xleroy2010-09-21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1512 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* UpdatedGravatar xleroy2010-09-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1505 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates for release 1.7Gravatar xleroy2010-03-30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1305 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for release 1.5Gravatar xleroy2009-08-27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1141 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* message macosx en accord avec configureGravatar blazy2009-06-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1079 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* UpdatesGravatar xleroy2009-01-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e