aboutsummaryrefslogtreecommitdiffstats
path: root/checklink
Commit message (Collapse)AuthorAgeFilesLines
* Clean up support for common symbols. Uninitialized "const" symbols can be ↵Xavier Leroy2014-12-171-6/+5
| | | | common.
* Removed more unused variables.Bernhard Schommer2014-12-041-1/+0
|
* Removed unused variable and changed the search for the installation ↵Bernhard Schommer2014-12-041-5/+0
| | | | directory. Use Sys.executable_name instead of Sys.argv.(0).
* Changed the comparison of jumptables.Bernhard Schommer2014-12-011-14/+7
|
* Use Bitstring.is_zeroes_bitstring from bitstring 2.0.4.Xavier Leroy GALLIUM2014-11-251-0/+8
| | | | The original code is less efficient and not tail recursive.
* Analysis of jump tables was using the wrong size.Xavier Leroy2014-11-171-1/+1
|
* cchecklink: added option "-files-from" to read .sdump file namesXavier Leroy2014-11-151-3/+27
| | | | from a file or from standard input.
* Removed duplicated open.Bernhard Schommer2014-10-171-1/+0
|
* Follow-up to commit 2613xleroy2014-08-201-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2614 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add builtins for load with reservation and conditional store.xleroy2014-08-201-0/+20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2613 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink/Check.ml: missing SDA addressing for store instructions.xleroy2014-08-191-1/+46
| | | | | | | | powerpc/PrintAsm.ml: update Linux output (Csymbol_rel, SDA sections). test/regression/sections.c: test for SDA and relative addressings. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2571 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.xleroy2014-08-181-6/+22
| | | | | | | | | | | powerpc/Asmgen*: simplify the code generated for far-data relative accesses, so that the only occurrences of Csymbol_rel_{low,high} are in the pattern Paddis(r, GPR0, Csymbol_rel_high...); Paddi(r, r, Csymbol_rel_low...) checklink/Check.ml: check the pattern above. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2569 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-284-853/+385
| | | | | | | | | | pseudo-instructions so that it does not need to be re-done in cchecklink. cchecklink: updated accordingly. testsuite: compile with -sdump and run cchecklink if supported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for single-precision floats. Calls to vararg functions remainxleroy2014-07-245-32/+153
| | | | | | | to be updated. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add _a memory accesses.xleroy2014-07-231-6/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-2/+2
| | | | | | | - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-282-140/+33
| | | | | | | | | | | | | | - 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-262-10/+10
| | | | | | like we already do in ARM Asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 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
* powerpc/: new unary operation "addsymbol"xleroy2013-11-172-0/+8
| | | | | | | | 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
* Update cchecklink w/ new Asm instructions Pmulh*xleroy2013-07-292-0/+24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2301 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add bswap16xleroy2013-04-301-1/+23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2223 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated to Pbuiltin with list of resultsxleroy2013-04-302-26/+26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2222 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-203-0/+12
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a ↵xleroy2013-03-181-1/+7
| | | | | | limitation in the a3 analyzers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2154 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates to follow recent changes in PrintAsm.mlxleroy2013-03-011-14/+43
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-294-36/+22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated to new external functions and new representation of programsxleroy2013-01-081-4/+15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2095 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-2/+2
| | | | | | | | | | 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
* 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-111-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1968 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
* Revert unintentional commit #1955xleroy2012-07-061-0/+0
| | | | 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-041-0/+0
| | | | 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
* checklink: adaptation to the new floatsvarobert2012-07-033-7/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1949 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: Faster printingvarobert2012-06-292-64/+121
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1943 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: Indentationvarobert2012-06-291-17/+17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1942 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: removed garbage codevarobert2012-06-291-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1941 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: improved user-friendlinessvarobert2012-06-045-161/+184
| | | | | | | | 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
generated by cgit (git 2.34.1) at 2024-06-28 21:57:22 +0000