aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* Typosxleroy2011-04-191-8/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1640 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed some typos.xleroy2011-04-171-13/+26
| | | | | | | Avoid generation of stubs for external functions without float arguments. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1639 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use memcpy_word only if alignment AND size are multiples of word size.xleroy2011-04-171-3/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1638 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed some typosxleroy2011-04-161-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1637 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/Elab: __attribute, not attributexleroy2011-04-165-4/+47
| | | | | | | | ia32/PrintAsm: wrong section name regression: added test attribs1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1636 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preliminary support for 'aligned' and 'section' attributes, gcc-style. ↵xleroy2011-04-166-71/+155
| | | | | | New-style handling of sections for IA32 and ARM. Work in progress, to be tested. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1635 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of GCC attributes. Preliminary, untested support for ↵xleroy2011-04-143-17/+34
| | | | | | __aligned__ attribute git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1634 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Renamed Machconcr into Machsem.xleroy2011-04-0918-1699/+202
| | | | | | | | Removed Machabstr and Machabstr2concr, now useless following the reengineering of Stacking. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1633 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch "unsigned-offsets":xleroy2011-04-0980-2683/+4487
| | | | | | | | | | | | | | - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of sizeof(string-literal)xleroy2011-03-156-7/+41
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Special case for while(1), for(..., 1, ...) and do ... while(0) loops.xleroy2011-03-152-22/+69
| | | | | | | | Don't wait until Constprop to get rid of trivial loop tests; instead, produces better-looking Cminor. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1610 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for 1.8.1xleroy2011-03-141-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1609 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for 1.8.1 releasev1.8.1xleroy2011-03-142-5/+31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1607 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Incompatibility 8.3 / 8.3pl1xleroy2011-03-141-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1606 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Comment char for Diabxleroy2011-03-131-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1605 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Slightly nicer semantics for initializationxleroy2011-03-131-28/+29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More global initialization work done and proved in Coq.xleroy2011-03-134-80/+410
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1603 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Initializers for global variables: compile-time evaluation of expressions ↵xleroy2011-03-1211-159/+891
| | | | | | done in Coq (module Initializers), using the same primitives as those for CompCert C's semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1602 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Undesirable optimization of 'print'xleroy2011-03-101-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1601 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bitfields: MSB-to-LSB in addition to LSB-to-MSBxleroy2011-03-103-11/+39
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1600 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised signed/unsigned char handling.xleroy2011-03-104-18/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1599 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved test harnessxleroy2011-03-103-0/+14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1598 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-0918-85/+70
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Treat "char" as unsigned OR signed depending on the configuration.xleroy2011-03-098-10/+58
| | | | | | | Fixed infinite expansion of some recursive struct type where recursion goes through a typeded. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1596 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use movapd instead of movsd for xmm reg-reg move: it avoids partial register ↵xleroy2010-11-281-1/+1
| | | | | | stalls, resulting in tiny speedups. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1556 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In StructAssign: be careful not to duplicate accesses to a volatile variable.xleroy2010-11-103-9/+24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1551 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* float->int conversions, continued: weaker axiomatization.xleroy2010-10-295-29/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1545 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-2821-62/+139
| | | | | | | (May fail if float is too big to be converted.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Various algorithmic improvements that reduce compile times (thanks Alexandre ↵xleroy2010-10-2719-141/+965
| | | | | | | | | | | | | | Pilkiewicz): - Lattice: preserve sharing in "combine" operation - Kildall: use splay heaps (lib/Heaps.v) for node sets - RTLgen: add a "nop" before loops so that natural enumeration of nodes coincides with (reverse) postorder - Maps: add PTree.map1 operation, use it in RTL and LTL. - Driver: increase minor heap size git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* License for Floataux.mlxleroy2010-10-272-1/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1542 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Inconsistent treatment of "lone" zero-width bit fieldsxleroy2010-09-245-24/+53
| | | | | | | (i.e. not preceded by another bit field). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1516 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bizarre use of struct valuev1.8xleroy2010-09-212-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1513 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for release 1.8xleroy2010-09-213-18/+42
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1512 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in doc commentxleroy2010-09-211-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1511 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Memory.v: added drop_perm operationxleroy2010-09-213-46/+427
| | | | | | | | Globalenvs.v: used drop_perm to set appropriate permissions on global variables (Notempty if volatile; Readable if readonly; Writable otherwise) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1510 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* No crash if nonexistent input file.xleroy2010-09-142-2/+3
| | | | | | | Heuristic to choose test data. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1509 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Commentsxleroy2010-09-101-8/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1508 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improvements for int8 and int16 storesxleroy2010-09-104-11/+53
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1507 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates for IA32-Cygwin.xleroy2010-09-085-33/+63
| | | | | | | | cparser/Elab.ml: tolerate changes in qualifiers in ?: cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1506 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updatedxleroy2010-09-042-12/+43
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1505 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ++ on volatile not supported.xleroy2010-09-041-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1504 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update: adding __builtin_annotationxleroy2010-09-041-1/+36
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplified stdlib wrapper; use it only under MacOS Xxleroy2010-09-047-278/+76
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for __builtin_fmax and __builtin_fminxleroy2010-09-042-1/+22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1501 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better emulation of long long as a struct.xleroy2010-09-042-16/+51
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1500 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the reuse-temps branch:xleroy2010-09-0289-2579/+12842
| | | | | | | | | | | | - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Semantics of annotationsxleroy2010-09-021-5/+69
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1498 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Adding __builtin_annotationxleroy2010-09-018-12/+219
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of ↵xleroy2010-09-0110-15/+119
| | | | | | reading a small unsigned bitfield git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1496 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_extxleroy2010-08-217-1121/+1148
| | | | | | | | | as bitwise operations rather than arithmetic ones. CastOptimproof: fixed for ARM port. Other files: adapted to changes in Integers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1472 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-05 16:57:11 +0000