aboutsummaryrefslogtreecommitdiffstats
path: root/checklink/Frameworks.ml
Commit message (Expand)AuthorAgeFilesLines
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-281-4/+4
* Update for single-precision floats. Calls to vararg functions remainxleroy2014-07-241-0/+2
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-8/+0
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-2/+2
* checklink: dead and debug code eliminationvarobert2012-07-121-2/+0
* checklink: simplificationsvarobert2012-07-121-13/+8
* checklink: configuration, indicate external symbolsvarobert2012-07-121-0/+2
* checklink: added configurabilityvarobert2012-07-111-2/+20
* checklink: improved user-friendlinessvarobert2012-06-041-1/+3
* checklink: new disassembler, error severity, ...varobert2012-06-011-1/+1
* Better error reports for checklinkvarobert2012-05-301-13/+20
* cchecklink now reads segments instead of sectionsvarobert2012-05-101-3/+1
* Added small data area support to checklinkvarobert2012-04-201-0/+11
* New section mapping checks and symbol data lookupvarobert2012-04-131-0/+6
* Added safety to potentially overflowing arithmeticsvarobert2012-04-041-4/+4
* Better fuzzing optionsvarobert2012-04-041-7/+0
* Adjustments to cchecklink's options and verbosityvarobert2012-04-041-5/+5
* Cleaning up checklinkvarobert2012-04-041-4/+0
* checklink: first import of Valentin Robert's validator for asm and linkxleroy2012-03-281-0/+194