summaryrefslogtreecommitdiff
path: root/checklink/Frameworks.ml
Commit message (Expand)AuthorAge
* PowerPC port: refactored the expansion of built-in functions andGravatar xleroy2014-07-28
* Update for single-precision floats. Calls to vararg functions remainGravatar xleroy2014-07-24
* Simpler, more robust emulation of calls to variadic functions:Gravatar xleroy2013-12-28
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
* checklink: dead and debug code eliminationGravatar varobert2012-07-12
* checklink: simplificationsGravatar varobert2012-07-12
* checklink: configuration, indicate external symbolsGravatar varobert2012-07-12
* checklink: added configurabilityGravatar varobert2012-07-11
* checklink: improved user-friendlinessGravatar varobert2012-06-04
* checklink: new disassembler, error severity, ...Gravatar varobert2012-06-01
* Better error reports for checklinkGravatar varobert2012-05-30
* cchecklink now reads segments instead of sectionsGravatar varobert2012-05-10
* Added small data area support to checklinkGravatar varobert2012-04-20
* New section mapping checks and symbol data lookupGravatar varobert2012-04-13
* Added safety to potentially overflowing arithmeticsGravatar varobert2012-04-04
* Better fuzzing optionsGravatar varobert2012-04-04
* Adjustments to cchecklink's options and verbosityGravatar varobert2012-04-04
* Cleaning up checklinkGravatar varobert2012-04-04
* checklink: first import of Valentin Robert's validator for asm and linkGravatar xleroy2012-03-28