summaryrefslogtreecommitdiff
path: root/checklink/Validator.ml
Commit message (Collapse)AuthorAge
* checklink: minor fixesGravatar varobert2012-07-12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1971 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: 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: 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
* 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
* Better fuzzing optionsGravatar varobert2012-04-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1868 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