summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Future-proofing: keep signature information in IA32 and PowerPC Asm, just ↵Gravatar xleroy2013-12-26
| | | | | | 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.Gravatar xleroy2013-12-21
| | | | 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.Gravatar xleroy2013-12-21
| | | | 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.Gravatar xleroy2013-12-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2382 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch value-analysis.Gravatar xleroy2013-12-20
| | | | 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.Gravatar xleroy2013-12-15
| | | | | | | 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.Gravatar xleroy2013-12-11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2378 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More tweaking re: builtin_memcpyGravatar xleroy2013-11-27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2377 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Attempted update to cchecklink re: memcpy.Gravatar xleroy2013-11-27
| | | | 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.Gravatar xleroy2013-11-27
| | | | 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.Gravatar xleroy2013-11-27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2374 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised semantics of external functions, continued:Gravatar xleroy2013-11-18
| | | | | | | | | - 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 axiomatizeGravatar xleroy2013-11-17
| | | | | | | them. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2369 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/: new unary operation "addsymbol"Gravatar xleroy2013-11-17
| | | | | | | | 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.Gravatar xleroy2013-11-10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2365 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaner printing of global variables.Gravatar xleroy2013-11-09
| | | | 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,Gravatar xleroy2013-11-06
| | | | | | | | | 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, ↵Gravatar xleroy2013-11-06
| | | | | | 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 nameGravatar xleroy2013-11-05
| | | | | | | (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.Gravatar xleroy2013-11-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2360 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Late update for release 2.1.Gravatar xleroy2013-10-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2359 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ release 2.1Gravatar xleroy2013-10-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2355 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better prepro options for XCode 5.0Gravatar xleroy2013-10-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2354 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Eliminate unreferenced inline functionsGravatar xleroy2013-10-28
| | | | 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.Gravatar xleroy2013-10-25
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2352 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix doc comment for loc_arguments.Gravatar xleroy2013-10-25
| | | | 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.Gravatar xleroy2013-10-24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2350 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use register names under Linux.Gravatar xleroy2013-10-24
| | | | 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 ↵Gravatar xleroy2013-10-24
| | | | | | 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.Gravatar xleroy2013-10-21
| | | | | | | 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 ↵Gravatar xleroy2013-10-18
| | | | | | 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)Gravatar xleroy2013-10-16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Warn for volatile accesses to compositesGravatar xleroy2013-10-16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2344 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PackedStructs.ml: cleanups and bug-fixesGravatar xleroy2013-10-13
| | | | | | | 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.Gravatar xleroy2013-10-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Follow-up to commit 2339:Gravatar xleroy2013-10-05
| | | | | | | 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:Gravatar xleroy2013-10-04
| | | | | | | | | | | - 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, MachGravatar xleroy2013-09-26
| | | | 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, MachGravatar xleroy2013-09-26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2337 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MacOS X linker option galoreGravatar xleroy2013-09-26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2336 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Slightly more efficient conversion positive <-> intGravatar xleroy2013-09-26
| | | | 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.Gravatar xleroy2013-09-20
| | | | | | | 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 Gravatar xleroy2013-09-14
| | | | | | | | | 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
* Change the way arguments to __builtin_annot are converted. Use the same ↵Gravatar xleroy2013-09-14
| | | | | | conventions as other variadic functions such as printf(). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2325 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Oops, wrong commit of generated files.Gravatar xleroy2013-08-24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2311 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to add these two files.Gravatar xleroy2013-08-24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2310 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplify LPMap by smashing bottoms.Gravatar xleroy2013-08-12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2306 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Change interface of Kildall solvers to avoid precomputing the map pc -> list ↵Gravatar xleroy2013-08-12
| | | | | | of successors. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2305 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add test for NaNsGravatar xleroy2013-08-02
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2304 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of Flocq version 2.2.0.Gravatar xleroy2013-08-02
| | | | | | | More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 09:48:57 +0000