aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Added command-line options -Wp,<opt> -Wa,<opt> -Wl,<opt>xleroy2012-02-293-3/+21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1832 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Problems with multiple declarations of publically-visible identifiersxleroy2012-02-293-20/+55
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1831 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better printing of pointer values and of locations.xleroy2012-02-292-26/+54
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1830 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* 'typeof' is not a keywordxleroy2012-02-291-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1829 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make CPragmas common to all ports.xleroy2012-02-274-71/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1828 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-2627-36/+134
| | | | | | | | | | and __alignof__(ty), __alignof__(expr) from GCC. - Resurrected __builtin_memcpy_aligned, useful for files generated by Scade KCG 6. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1827 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Translate CompCert C's "a ? b : c" to the equivalent simple Clight expr ifxleroy2012-02-255-100/+199
| | | | | | | b and c are simple. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1826 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Take advantage of Cmaskzero and Cmasknotzero.xleroy2012-02-248-12/+90
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1825 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved instruction selection for "notint".xleroy2012-02-247-11/+61
| | | | | | | powerpc/PrintAsm.ml: fixed MacOS X problems with malloc and free git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1824 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-239-231/+556
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1823 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplified and cleaned up the passing of information from C2C to PrintAsm, ↵xleroy2012-02-229-211/+191
| | | | | | as well as the handling of sections. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1822 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* The C declaration associated with __stringlit_N globals now has type const ↵xleroy2012-02-201-1/+2
| | | | | | char[N] instead of const char * as before (for no good reason). In particular, it means that string literals now have alignment 1, as they should. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1821 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Don't print external declarations for builtins.xleroy2012-02-182-4/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1818 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Work around limited excursion of conditional branchesxleroy2012-02-131-4/+86
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1817 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Interp: help debug stuck expressionsxleroy2012-02-104-7/+52
| | | | | | | | StructReturn: was building an ill-typed Ecomma expression Cutil: export "ecast" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1816 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Initializers: handle By_copy accesses (e.g. for &(glob.field))xleroy2012-02-078-57/+29
| | | | | | | | | C2C: insert the correct Evalof for structs; clean up unused memcpy stuff test/regression: run with interpreter test/regression: add test cas &(glob.field) to initializers.c git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1815 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "volatile" branch:xleroy2012-02-0464-3627/+4356
| | | | | | | | | | | | - 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
* Out-of-bounds error in testxleroy2012-01-212-16/+16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1802 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another typo in print_builtin_vstore_commonxleroy2012-01-211-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1801 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in print_builtin_vstore_commonxleroy2012-01-211-5/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1800 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a ↵xleroy2012-01-213-11/+50
| | | | | | | | | certain customer's code backend/Coloringaux: avoid spilling the dummy result registers for built-ins that have no result. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1799 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cosmetic cleanups.xleroy2012-01-153-12/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1793 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-1519-2858/+1528
| | | | | | | Finished updating IA32 and ARM ports. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the nonstrict-ops branch:xleroy2012-01-1465-12566/+9933
| | | | | | | | | | | - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updatev1.9.1xleroy2011-11-271-7/+26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1742 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More careful updating of current location for error msgs.xleroy2011-11-261-6/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1739 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/*: refactoring of the expansion of read-modify-write operatorsxleroy2011-11-2613-230/+428
| | | | | | | | | cparser/PackedStructs: treat r-m-w operations over byte-swapped fields cparser/PackedStructs: allow static initialization of packed structs test/regression: more packedstruct tests git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1738 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed serious bug in handling of volatile arrays.xleroy2011-11-264-4/+29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1737 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Interp: accommodate "int main(int, char **)".xleroy2011-10-192-11/+36
| | | | | | | Driver: dead code removed. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1733 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-1817-102/+80
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Corrected initialization of char arrays by string literals.xleroy2011-10-176-28/+53
| | | | | | | Added -flongdouble option (to turn long double into double) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1731 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More cleanups in packed struct emulation.xleroy2011-10-162-14/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1730 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised emulation of packed structsxleroy2011-10-168-76/+83
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1729 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Watch out for min_int / -1xleroy2011-08-271-1/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1727 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Doc fixesxleroy2011-08-232-2/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1726 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ licencexleroy2011-08-232-15/+21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1725 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Changelog, doc: updated for release 1.9v1.9xleroy2011-08-224-10/+24
| | | | | | | 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?xleroy2011-08-226-22/+33
| | | | | | | 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_movexleroy2011-08-221-7/+6
| | | | 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.xleroy2011-08-211-8/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1720 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaned up old commented-out partsxleroy2011-08-1916-326/+1
| | | | 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'xleroy2011-08-185-36/+24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1718 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Presimplification SimplVolatile: cleaned up and integrated.xleroy2011-08-1814-22/+171
| | | | | | 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 volatilesxleroy2011-08-1810-169/+265
| | | | | | | | 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_lvaluexleroy2011-08-173-41/+20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1715 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJxleroy2011-08-161-4/+12
| | | | 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 ↵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
generated by cgit (git 2.34.1) at 2024-07-03 05:03:45 +0000