summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Watch out for min_int / -1Gravatar xleroy2011-08-27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1727 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Doc fixesGravatar xleroy2011-08-23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1726 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ licenceGravatar xleroy2011-08-23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1725 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Changelog, doc: updated for release 1.9Gravatar xleroy2011-08-22
| | | | | | | lib/Integers, Makefile: unsuccessful experiments with coqchk git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1723 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* arm/PrintAsm: don't generate "vfd" directive, useless?Gravatar xleroy2011-08-22
| | | | | | | cparser: distinguish more carefully between lvalues and modifiable lvalues. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1722 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Harden proof script against empty destroyed_at_moveGravatar xleroy2011-08-22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1721 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong check: &e must be rejected if e has array type and is not a l-value.Gravatar xleroy2011-08-21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1720 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaned up old commented-out partsGravatar xleroy2011-08-19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More careful treatment of 'load immediate 0' as 'xor self'Gravatar xleroy2011-08-18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1718 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Presimplification SimplVolatile: cleaned up and integrated.Gravatar xleroy2011-08-18
| | | | | | test/*/Makefile: normalized 'bench' target git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1717 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* SimplVolatile: new pass to eliminate read-modify-write ops over volatilesGravatar xleroy2011-08-18
| | | | | | | | Elsewhere: refactoring, moving common code into Cutil and Transform (to be continued) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1716 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Factor out bind_lvalueGravatar xleroy2011-08-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1715 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJGravatar xleroy2011-08-16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1714 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* New backend pass "RRE": optimize (somewhat) redundant reloads introduced by ↵Gravatar xleroy2011-08-16
| | | | | | the Reload pass. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1713 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to update: adding xchg instructionGravatar xleroy2011-08-16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1712 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Locations.v: add Loc.diff_dec.Gravatar xleroy2011-08-14
| | | | | | | | ia32: lift restriction that 1st arg of ops cannot be ECX (could be useful for a future, better reloading strategy) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1711 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* IA32 PrintAsm.ml: wrong moves generated in print_builtin_memcpy_bigGravatar xleroy2011-08-10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1706 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* IA32: wrong moves generated in print_builtin_memcpy_big.Gravatar xleroy2011-08-10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1705 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Treatment of volatiles: offer the choice between random reads and treating ↵Gravatar xleroy2011-08-09
| | | | | | volatile accesses like regular loads and stores. (The latter is needed e.g. for Csmith testing.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1703 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More vigorous scrubbing of r-value structsGravatar xleroy2011-08-09
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1702 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved treatment of structs/unions as r-valuesGravatar xleroy2011-08-08
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1701 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* IA32 port: more faithful treatment of pseudoregister ST0.Gravatar xleroy2011-08-08
| | | | | | | Related general change: support for destroyed_at_moves. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1700 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaned up handling of composite conditionsGravatar xleroy2011-08-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1699 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong ifdef PPCGravatar xleroy2011-08-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1698 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More builtins for ARM and PowerPCGravatar xleroy2011-08-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1697 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* arm/PrintAsm: bugs in expansion of new builtinsGravatar xleroy2011-08-05
| | | | | | | test/: testing the builtins git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1696 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flag long long and long double literalsGravatar xleroy2011-07-31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1695 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Check fcmpd semanticsGravatar xleroy2011-07-31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1694 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM: added reversed load/store builtins + bswap builtin (to be tested)Gravatar xleroy2011-07-30
| | | | | | | | IA32: added bswap builtin Updated Changelog git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1693 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM codegen ported to new ABI + VFD floatsGravatar xleroy2011-07-30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Interp.ml: initialize PRNGGravatar xleroy2011-07-29
| | | | | | | Cexec.v: comments git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1691 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in arm/PrintAsm.mlGravatar xleroy2011-07-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1690 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated Makefile and dependencies. Typo in powerpc/PrintAsm.ml.Gravatar xleroy2011-07-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1689 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added animation of the CompCert C semantics (ccomp -interp)Gravatar xleroy2011-07-28
| | | | | | | | test/regression: int main() so that interpretation works Revised once more implementation of __builtin_memcpy (to check for PPC & ARM) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Check for duplicate label definitionsGravatar xleroy2011-07-18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1687 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More precise typechecking of statementsGravatar xleroy2011-07-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1686 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved semantics of castsGravatar xleroy2011-07-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1685 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to ↵Gravatar xleroy2011-07-16
| | | | | | | | | the type of the whole conditional expression. Replaced predicates "cast", "is_true" and "is_false" by functions "sem_cast" and "bool_val". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1684 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch new-semantics: revised and strengthened top-level statements ↵Gravatar xleroy2011-07-15
| | | | | | of semantic preservation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix treatment of function pointers at function calls in the CompCert C and ↵Gravatar xleroy2011-07-14
| | | | | | Clight semantics git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1680 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Back from Oregon commit. Gravatar xleroy2011-07-05
| | | | | | | | | powerpc/*: better compilation of some comparisons; revised asmgenproof1. common/*: added Mem.storebytes; used to give semantics to memcpy builtin. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1679 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Relating neg and notGravatar xleroy2011-06-22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1678 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to print Oroli opGravatar xleroy2011-06-22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1677 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Recognition of rlwimi instruction (useful for bitfield assignment)Gravatar xleroy2011-06-21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1676 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coloringaux: better cost estimate for annotation builtinsGravatar xleroy2011-06-14
| | | | | | | Regression: more tests for annotations git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1675 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add preference for annot_val builtinGravatar xleroy2011-06-14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1674 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to add new fileGravatar xleroy2011-06-14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1673 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of annotation statements, and more generally built-in ↵Gravatar xleroy2011-06-13
| | | | | | functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Minor update in Clight (big-step)Gravatar blazy2011-06-08
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1670 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Oaddrsymbol and small data areaGravatar xleroy2011-06-07
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1667 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:37:40 +0000