aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Merge of the clightgen branch:xleroy2012-12-2934-2718/+4800
| | | | | | | | | | | | | | | | | | - Alternate semantics for Clight where function parameters are temporaries, not variables - New pass SimplLocals that turns non-addressed local variables into temporaries - Simplified Csharpminor, Cshmgen and Cminorgen accordingly - SimplExpr starts its temporaries above variable names, therefoe Cminorgen no longer needs to encode variable names and temps names. - Simplified Cminor parser & printer, as well as Errors, accordingly. - New tool clightgen to produce Clight AST in Coq-parsable .v files. - Removed side condition "return type is void" on rules skip_seq in the semantics of CompCert C, Clight, C#minor, Cminor. - Adapted RTLgenproof accordingly (now uses a memory extension). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix "clean" rule.xleroy2012-12-291-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2082 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Composition properties between injections and extensions.xleroy2012-12-291-8/+80
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2081 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integers: specialized function to compute x mod 2^N; used in "repr" toxleroy2012-12-212-115/+179
| | | | | | | | avoid the cost of a general Zmod. Memdata: updated accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2077 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Separate interference graphs for ints and floats, i.e. don't record ↵xleroy2012-12-201-13/+16
| | | | | | interference edges between nodes of different types: this is useless and falsifies the heuristics based on node degree. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test bitfields of enum typexleroy2012-12-182-0/+28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2075 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inline assembly (asm statements).xleroy2012-12-1828-76/+259
| | | | | | | cparser: add primitive support for enum types. bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test for __builtin_fctixleroy2012-11-241-1/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2072 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add __builtin_fcti (double -> int conversion w/ round to nearest)xleroy2012-11-242-0/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2071 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-1238-1637/+1301
| | | | | | | | | | | function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)xleroy2012-11-0314-95/+180
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update cparser/Makefile (fix by Jacques-Henri Jourdan)xleroy2012-11-032-28/+28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2064 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Clight: split off the big step semantics in ClightBigstep.xleroy2012-10-145-563/+695
| | | | | | | Cstrategy: updated the big-step semantics with Eseqand and Eseqor. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2062 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Generate output files in current directory; can be overriden with -o optionxleroy2012-10-083-34/+65
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2061 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make Clight independent of CompCert C.xleroy2012-10-0822-1385/+1522
| | | | | | | Common parts are factored out in cfrontend/Ctypes.v and cfrontend/Cop.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2060 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-0647-2816/+2739
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed 2 errors in revised builtin_vstore. xleroy2012-08-221-2/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2035 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong usage of temps in builtin_volatile_write.xleroy2012-08-171-12/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2030 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Define useful functions instr_defs and instr_usesxleroy2012-08-101-0/+35
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove Val.is_true and Val.is_false, no longer used.xleroy2012-08-065-103/+74
| | | | | | | Simplified definition of Val.bool_of_val. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2015 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated documentationxleroy2012-08-021-28/+19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1989 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Removed old, commented-out definitions.xleroy2012-08-011-292/+30
| | | | | | | Removed axiom "traceinf_determ" and show uniqueness of behaviors up to similarity of infinite traces. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1988 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More aggressive elimination of conditional branches during constantxleroy2012-08-013-201/+234
| | | | | | | | | propagation, taking better advantage of inferred constants. Helps with the compilation of && and || operators. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1987 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to collect types of expressionsxleroy2012-07-282-2/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1984 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-2338-183/+331
| | | | | | | | | | injections compose (Values, Memdata, Memory) - Memory chunks: Mfloat64 now has alignment 8; introduced Mfloat64al32 that works like old Mfloat64 (i.e. has alignment 4); simplified handling of memcpy builtin accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1983 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove the PowerPC/MacOS X port, as MacOS no longer supports PowerPC.xleroy2012-07-144-937/+21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1980 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for indirect symbols under MacOS X (final).xleroy2012-07-1416-112/+53
| | | | | | | Remove stdio hack in runtime/ git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for MacOS X's indirect symbols. (first try)xleroy2012-07-1310-41/+102
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1978 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Late update for 1.11xleroy2012-07-131-4/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1977 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preparation for release 1.11v1.11xleroy2012-07-132-6/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1975 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: dead and debug code eliminationvarobert2012-07-122-3/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1974 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: simplificationsvarobert2012-07-122-67/+73
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1973 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: allow other number formats in configurationvarobert2012-07-121-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1972 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: minor fixesvarobert2012-07-122-7/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1971 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: configuration, indicate external symbolsvarobert2012-07-123-66/+84
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1970 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: added configurabilityvarobert2012-07-113-64/+180
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1969 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: more stringent compilationvarobert2012-07-112-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1968 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Strip quotes from section names during #pragma parsing.xleroy2012-07-114-9/+9
| | | | | | | | | Reinstall the quotes when printing asm. The idea is that .sdump files now contain unquoted section names, which is easier on cchecklink. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1967 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM port.xleroy2012-07-105-29/+20
| | | | | | | CSE.v: removed commented-out stuff. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1966 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Accept long double literals if -flongdouble is given.xleroy2012-07-101-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1965 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: fixed SDA inference, passes testvarobert2012-07-101-6/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1964 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.xleroy2012-07-093-16/+77
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1963 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert unintentional commit #1955xleroy2012-07-065-16/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1957 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: minor changesvarobert2012-07-051-8/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1956 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout trunk CompCertblazy2012-07-045-12/+16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1955 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: better diagnosisvarobert2012-07-041-112/+103
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1954 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: some more debug tracingvarobert2012-07-041-0/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1953 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: more defensive is_paddingvarobert2012-07-041-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1952 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: fixed bits/bytes mistakevarobert2012-07-041-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1951 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update CombineOp for arm and ia32.xleroy2012-07-034-7/+21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1950 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-02 21:33:49 +0000