aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).xleroy2013-12-3011-156/+237
| | | | | | | __builtin_memcpy_aligned now supports the case sz = 0. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2392 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Elab.ml: more warnings.xleroy2013-12-302-6/+16
| | | | | | | Cutil.ml: fix sizeof calculation of structs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2391 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved detection of variables with incomplete types.xleroy2013-12-302-5/+12
| | | | | | | Additional warnings for empty initializer braces and zero-sized arrays. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2390 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More tolerance for functions declared without a prototypexleroy2013-12-284-10/+31
| | | | | | | | (option -funprototyped, on by default). Error if call to vararg function and -fvararg-calls is off. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2389 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Check in C2C that packed structs were properly emulated.xleroy2013-12-282-5/+12
| | | | | | | PackedStructs.ml: remove "packed" attribute once processed. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2388 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Removed obsolete check on aligned fields.xleroy2013-12-281-8/+4
| | | | | | | More informative "unsupported" error messages. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-2845-497/+366
| | | | | | | | | | | | | | - C function types and Cminor signatures annotated by calling conventions. esp. vararg / not vararg - Cshmgen: generate correct code for function call where there are more arguments than listed in the function prototype. This is still undefined behavior according to the formal semantics, but correct code is generated. - C2C, */PrintAsm.ml: remove "printf$iif" hack. - powerpc/, checklink/: don't generate stubs for variadic functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Future-proofing: keep signature information in IA32 and PowerPC Asm, just ↵xleroy2013-12-2614-141/+146
| | | | | | like we already do in ARM Asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised parsing of command-line options, more GCC-like.xleroy2013-12-212-21/+45
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support "default" cases in the middle of a "switch", not just at the end.xleroy2013-12-2118-209/+373
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Hack StructReturn to better adhere to PowerPC and ARM calling conventions.xleroy2013-12-205-67/+162
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2382 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch value-analysis.xleroy2013-12-2051-4187/+12730
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Axioms: remove prop_ext, currently unused AND unsound in Coq 8.4.xleroy2013-12-152-25/+18
| | | | | | | VERSION: bump version number. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2379 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bring sizeof and alignof in sync with cfrontend/Ctypes.xleroy2013-12-111-22/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2378 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More tweaking re: builtin_memcpyxleroy2013-11-271-6/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2377 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Attempted update to cchecklink re: memcpy.xleroy2013-11-271-8/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2376 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Be more conservative in choosing the unrolled form of __builtin_memcpy.xleroy2013-11-271-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2375 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Rename "-fno-sse" into "-fno-fpu" and honor it on PowerPC as well.xleroy2013-11-274-5/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2374 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised semantics of external functions, continued:xleroy2013-11-185-185/+82
| | | | | | | | | - Also axiomatize the semantics of inline asm - In Cexec, revised parameterization over do_external_function - In Interp.ml, matching changes + suppression of Interp_ext.ml git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2370 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised modeling of external functions and built-in functions: just axiomatizexleroy2013-11-175-151/+171
| | | | | | | them. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2369 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/: new unary operation "addsymbol"xleroy2013-11-1721-92/+302
| | | | | | | | Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppress warning on derefering volatile composites, because of false positives.xleroy2013-11-101-4/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2365 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaner printing of global variables.xleroy2013-11-091-21/+30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2364 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Recognize __builtin_fabs as an operator, not just a builtin,xleroy2013-11-0614-6/+50
| | | | | | | | | enabling more aggressive optimizations. - Less aggressive CSE for EF_builtin builtins, causes problems for __builtin_write{16,32}_reversed. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2363 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised treatment of _Alignas, for better compatibility with GCC and Clang, ↵xleroy2013-11-0611-147/+320
| | | | | | and to avoid wasting global variable space by inflating their sizeof needlessly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2362 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make it possible to use the "__packed__" keyword as an attribute namexleroy2013-11-051-0/+1
| | | | | | | (same as for "const"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2361 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Error for 'switch' on a 64-bit integer argument.xleroy2013-11-041-0/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2360 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Late update for release 2.1.xleroy2013-10-281-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2359 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ release 2.1v2.1xleroy2013-10-281-10/+25
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2355 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better prepro options for XCode 5.0xleroy2013-10-281-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2354 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Eliminate unreferenced inline functionsxleroy2013-10-281-2/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2353 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revise parsing of character constants for conformance with ISO C 99.xleroy2013-10-252-12/+14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2352 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix doc comment for loc_arguments.xleroy2013-10-251-6/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2351 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert commit r2349 because it triggers a bug in GNU as.xleroy2013-10-242-18/+29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2350 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use register names under Linux.xleroy2013-10-242-29/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2349 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fine-tuning of the "andimm" case to generate a move rather than an andimm ↵xleroy2013-10-242-2/+13
| | | | | | when possible. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2348 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typing of integer literals: follow C99 rules exactly.xleroy2013-10-211-28/+29
| | | | | | | Comments: make reference to the C99 standard. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2347 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised renumbering of nodes and registers so that main function is not ↵xleroy2013-10-183-48/+114
| | | | | | shifted by 1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cminor parsing and printing (from Andrew Tolmach)xleroy2013-10-167-24/+175
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Warn for volatile accesses to compositesxleroy2013-10-161-0/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2344 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PackedStructs.ml: cleanups and bug-fixesxleroy2013-10-132-15/+17
| | | | | | | Ceval.ml: tolerate non-zero integers with pointer types. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2343 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "alignas" branch.xleroy2013-10-0526-428/+538
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Follow-up to commit 2339:xleroy2013-10-051-1/+1
| | | | | | | don't complain about parameter redefinition for unnamed parameters. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2340 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Elab:xleroy2013-10-042-29/+34
| | | | | | | | | | | - bad error recovery on bitfield with 'long long' type - check for redefinition of function parameters Bitfields: - when assigning to a bitfield, cast the RHS to "unsigned int" (it matters if the RHS is long long). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2339 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Do not use Format for faster printing of RTL, XTL, LTL, Machxleroy2013-09-262-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2338 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Do not use Format for faster printing of RTL, XTL, LTL, Machxleroy2013-09-266-137/+129
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2337 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MacOS X linker option galorexleroy2013-09-261-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2336 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Slightly more efficient conversion positive <-> intxleroy2013-09-261-17/+22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2335 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Small improvements in compilation times for the register allocation pass.xleroy2013-09-206-22/+86
| | | | | | | Maps.v: add a PTree.fold1 operation that doesn't maintain the key. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2329 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms xleroy2013-09-1420-107/+374
| | | | | | | | | are necessary, only two parameters (default_pl and choose_binop_pl). SelectDiv: optimize FP division by a power of 2. ConstpropOp: optimize 2.0 * x and x * 2.0 into x + x. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2326 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-02 23:29:46 +0000