summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Integers: specialized function to compute x mod 2^N; used in "repr" toGravatar xleroy2012-12-21
| | | | | | | | 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 ↵Gravatar xleroy2012-12-20
| | | | | | 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 typeGravatar xleroy2012-12-18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2075 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inline assembly (asm statements).Gravatar xleroy2012-12-18
| | | | | | | 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_fctiGravatar xleroy2012-11-24
| | | | 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)Gravatar xleroy2012-11-24
| | | | 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 eachGravatar xleroy2012-11-12
| | | | | | | | | | | 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)Gravatar xleroy2012-11-03
| | | | 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)Gravatar xleroy2012-11-03
| | | | 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.Gravatar xleroy2012-10-14
| | | | | | | 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 optionGravatar xleroy2012-10-08
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2061 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make Clight independent of CompCert C.Gravatar xleroy2012-10-08
| | | | | | | 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.Gravatar xleroy2012-10-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed 2 errors in revised builtin_vstore. Gravatar xleroy2012-08-22
| | | | 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.Gravatar xleroy2012-08-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2030 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Define useful functions instr_defs and instr_usesGravatar xleroy2012-08-10
| | | | 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.Gravatar xleroy2012-08-06
| | | | | | | 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 documentationGravatar xleroy2012-08-02
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1989 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Removed old, commented-out definitions.Gravatar xleroy2012-08-01
| | | | | | | 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 constantGravatar xleroy2012-08-01
| | | | | | | | | 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 expressionsGravatar xleroy2012-07-28
| | | | 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 Gravatar xleroy2012-07-23
| | | | | | | | | | 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.Gravatar xleroy2012-07-14
| | | | 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).Gravatar xleroy2012-07-14
| | | | | | | 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)Gravatar xleroy2012-07-13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1978 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Late update for 1.11Gravatar xleroy2012-07-13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1977 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preparation for release 1.11Gravatar xleroy2012-07-13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1975 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: dead and debug code eliminationGravatar varobert2012-07-12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1974 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: simplificationsGravatar varobert2012-07-12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1973 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: allow other number formats in configurationGravatar varobert2012-07-12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1972 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: minor fixesGravatar varobert2012-07-12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1971 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: configuration, indicate external symbolsGravatar varobert2012-07-12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1970 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: added configurabilityGravatar varobert2012-07-11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1969 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: more stringent compilationGravatar varobert2012-07-11
| | | | 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.Gravatar xleroy2012-07-11
| | | | | | | | | 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.Gravatar xleroy2012-07-10
| | | | | | | 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.Gravatar xleroy2012-07-10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1965 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: fixed SDA inference, passes testGravatar varobert2012-07-10
| | | | 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.Gravatar xleroy2012-07-09
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1963 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert unintentional commit #1955Gravatar xleroy2012-07-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1957 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: minor changesGravatar varobert2012-07-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1956 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout trunk CompCertGravatar blazy2012-07-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1955 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: better diagnosisGravatar varobert2012-07-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1954 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: some more debug tracingGravatar varobert2012-07-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1953 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: more defensive is_paddingGravatar varobert2012-07-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1952 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: fixed bits/bytes mistakeGravatar varobert2012-07-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1951 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update CombineOp for arm and ia32.Gravatar xleroy2012-07-03
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1950 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: adaptation to the new floatsGravatar varobert2012-07-03
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1949 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Process successors in increasing order. Helps preserving the nice CFGGravatar xleroy2012-07-01
| | | | | | | | structure that we got from Cminorgen. Otherwise, the linearization heuristic can produce rather bad code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1948 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Factor out the evaluation of the float constant in intuoffloat.Gravatar xleroy2012-07-01
| | | | | | | Probably redundant with CSE, but better safe than sorry. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1947 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-16 12:31:14 +0000