aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* New backend pass "RRE": optimize (somewhat) redundant reloads introduced by ↵xleroy2011-08-167-22/+938
| | | | | | 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 instructionxleroy2011-08-161-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1712 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Locations.v: add Loc.diff_dec.xleroy2011-08-147-144/+145
| | | | | | | | 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_bigxleroy2011-08-101-8/+20
| | | | 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.xleroy2011-08-103-1/+41
| | | | 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 ↵xleroy2011-08-091-2/+17
| | | | | | 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 structsxleroy2011-08-091-12/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1702 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved treatment of structs/unions as r-valuesxleroy2011-08-082-21/+47
| | | | 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.xleroy2011-08-0814-169/+356
| | | | | | | 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 conditionsxleroy2011-08-056-99/+311
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1699 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong ifdef PPCxleroy2011-08-051-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1698 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More builtins for ARM and PowerPCxleroy2011-08-055-3/+15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1697 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* arm/PrintAsm: bugs in expansion of new builtinsxleroy2011-08-052-17/+35
| | | | | | | 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 literalsxleroy2011-07-311-2/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1695 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Check fcmpd semanticsxleroy2011-07-311-10/+19
| | | | 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)xleroy2011-07-305-7/+84
| | | | | | | | 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 floatsxleroy2011-07-3016-629/+560
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Interp.ml: initialize PRNGxleroy2011-07-292-2/+15
| | | | | | | Cexec.v: comments git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1691 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in arm/PrintAsm.mlxleroy2011-07-281-2/+2
| | | | 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.xleroy2011-07-283-6/+6
| | | | 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)xleroy2011-07-2819-455/+2741
| | | | | | | | 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 definitionsxleroy2011-07-181-7/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1687 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More precise typechecking of statementsxleroy2011-07-171-33/+75
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1686 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved semantics of castsxleroy2011-07-175-66/+150
| | | | 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 ↵xleroy2011-07-1615-733/+598
| | | | | | | | | 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 ↵xleroy2011-07-1542-1848/+3307
| | | | | | 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 ↵xleroy2011-07-144-26/+19
| | | | | | Clight semantics git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1680 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Back from Oregon commit. xleroy2011-07-0513-598/+1533
| | | | | | | | | 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 notxleroy2011-06-221-5/+42
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1678 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to print Oroli opxleroy2011-06-221-0/+4
| | | | 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)xleroy2011-06-218-19/+92
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1676 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coloringaux: better cost estimate for annotation builtinsxleroy2011-06-142-3/+41
| | | | | | | 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 builtinxleroy2011-06-142-4/+21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1674 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to add new filexleroy2011-06-141-0/+40
| | | | 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 ↵xleroy2011-06-1345-469/+1140
| | | | | | 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)blazy2011-06-081-18/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1670 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Oaddrsymbol and small data areaxleroy2011-06-072-2/+13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1667 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout big-step Clight et preuve big-step -> small-stepblazy2011-05-251-1/+769
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1659 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot somethingxleroy2011-05-241-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1658 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for release 1.8.2xleroy2011-05-242-29/+41
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1656 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Nicer printing of annotations.xleroy2011-05-235-19/+45
| | | | | | | ia32: support builtins for reversed reads and writes (facilitates testing). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1655 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Silence a warning that happens all too often in MacOS Xxleroy2011-05-121-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1654 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another try for the ifdefxleroy2011-05-121-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1653 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong ifdefxleroy2011-05-121-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1652 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typoxleroy2011-05-121-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1651 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser: support for attributes over struct and union.xleroy2011-05-1228-149/+781
| | | | | | | | cparser: added experimental emulation of packed structs (PackedStruct.ml) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/StructAssign: always use __builtin_memcpy + alignment indicationxleroy2011-05-116-300/+443
| | | | | | | | | | (simpler and globally more efficient) cfrontend/C2C.ml: specialization of __builtin_memcpy over size */PrintAsm.ml: revised expansion of __builtin_memcpy_* ia32/Asm.ml: typo in comment git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1649 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).xleroy2011-05-0812-53/+218
| | | | | | | | | | 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
* Added pass CleanupLabels to remove unreferenced labels in a proved way.xleroy2011-05-089-27/+507
| | | | | | | | | | ia32/PrintAsm.ml: simplified accordingly; other PrintAsm.ml to be fixed. ia32/Asm.v: Pmov_ri can undef flags (if translated to xor) cparser/Ceval.ml: treat ~ in constant exprs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support compile-time constant expressions as arguments to gcc-style attributesxleroy2011-04-202-24/+31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1641 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-03 08:43:00 +0000