aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* MAJ docv1.10xleroy2012-03-123-12/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1850 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Option -randvol to expose randomization of volatiles in Interp.mlxleroy2012-03-121-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1849 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Minor updatesxleroy2012-03-114-198/+19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1848 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Proof didn't go through for ARMxleroy2012-03-111-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1847 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another update from Andrew Tolmachxleroy2012-03-091-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1840 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PrintCminor: printing Sskipxleroy2012-03-094-6/+6
| | | | | | | test/cminor: updating git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1839 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of Andrew Tolmach's HASP-related changesxleroy2012-03-0912-125/+913
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1838 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cprint: export Cprint.attributesxleroy2012-03-073-10/+41
| | | | | | | | PackedStructs: honor 'aligned' attribute on packed struct fields C2C: warn for ignored 'aligned' attributes git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1837 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC: remove the fmadd and fmsub operators/Asm instructionsxleroy2012-03-0715-67/+27
| | | | | | | | (definitely not semantics-preserving; hard to justify). CPragmas: make sure SDAs are not recognized on MacOSX. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1836 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add -toolprefixxleroy2012-03-061-37/+41
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1835 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updatexleroy2012-03-061-3/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1834 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove 'near-code' access mode, makes no sense in CompCertxleroy2012-03-061-2/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1833 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* 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
generated by cgit (git 2.34.1) at 2024-06-11 21:16:30 +0000