summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
* 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
* Recombine x = cmp(...); if (x == 1) ...Gravatar xleroy2012-07-01
| | | | | | | and x = cmp(...); if (x != 1) ... git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added option -falign-functionsGravatar xleroy2012-07-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More aggressive 'uncasting' before storing small integersGravatar xleroy2012-06-30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1944 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: Faster printingGravatar varobert2012-06-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1943 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: IndentationGravatar varobert2012-06-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1942 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: removed garbage codeGravatar varobert2012-06-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1941 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Changelog: updatedGravatar xleroy2012-06-28
| | | | | | | | | | driver/Interp.ml: clean up dead code lib/Integers.v: add shifted_or_is_add lib/Floats.v: add from_words_eq .depend: updated git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use Flocq for floatsGravatar xleroy2012-06-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make min_int / -1 and min_int % -1 semantically undefinedGravatar xleroy2012-06-09
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1919 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More properties on mul/div/modGravatar xleroy2012-06-09
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1918 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: improved user-friendlinessGravatar varobert2012-06-04
| | | | | | | | Command-line options have been renamed and reordered. Error messages verbosity is more fine-grained. Possibly spurious debug messages are more clearly separated from the actual conclusions of the process. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1913 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: improved error messagesGravatar varobert2012-06-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1909 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: new disassembler, error severity, ...Gravatar varobert2012-06-01
| | | | | | | | | | | | | | - Added the -disass command-line option to disassemble symbols found in the ELF ; - Field mismatch now stops the matching of two code fragments, while it used to only emit an error in the log ; - Fixed a long-lasting bug in the command-line option ; - Some error messages have been improved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1908 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: better error messagesGravatar varobert2012-05-31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1907 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: fixed FSQRTEx parsingGravatar varobert2012-05-31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1906 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better error reports for checklinkGravatar varobert2012-05-30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1905 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 18:35:58 +0000