summaryrefslogtreecommitdiff
path: root/checklink/Library.ml
Commit message (Collapse)AuthorAge
* Update for single-precision floats. Calls to vararg functions remainGravatar xleroy2014-07-24
| | | | | | | to be updated. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:Gravatar xleroy2013-04-20
| | | | | | | | | 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
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 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: more stringent compilationGravatar varobert2012-07-11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1968 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
* checklink: Faster printingGravatar varobert2012-06-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1943 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
* cchecklink continues when sections overlapGravatar varobert2012-05-24
| | | | | | | cchecklink now reports overlapping sections but keeps analyzing. Error messages have also been made clearer. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1901 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cchecklink now reads segments instead of sectionsGravatar varobert2012-05-10
| | | | | | | | | | | | | cchecklink is now using program header information to figure out the initial address space of the program, rather than the information in the parent section of each symbol. This decouples the resolution of symbols from inaccurate section information, reflecting more the actual program loading. Additionally, a -relaxed option has been added to deal with some strange ELFs, for instance when symbols data is dynamically bootstrapped from another place by boot code different than the program loader. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1893 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added small data area support to checklinkGravatar varobert2012-04-20
| | | | | | | | Accesses to small data areas are dynamically resolved by constructing a mapping from registers to virtual addresses they are supposed to point to. This mapping is reported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1880 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Faster ndxes_of_sym_nameGravatar varobert2012-04-12
| | | | | | | | | ndxes_of_sym_name used to have an O(s^2) complexity where s was the number of symbols in the ELF file. It has now been reduced to an O(s*ln(s)) by pre-computing the sets of symbols corresponding to each normalized symbol name. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1875 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added safety to potentially overflowing arithmeticsGravatar varobert2012-04-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1872 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Adjustments to cchecklink's options and verbosityGravatar varobert2012-04-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1866 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: first import of Valentin Robert's validator for asm and linkGravatar xleroy2012-03-28
cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e