summaryrefslogtreecommitdiff
path: root/checklink/Check.ml
Commit message (Expand)AuthorAge
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.Gravatar xleroy2014-01-12
* Simpler, more robust emulation of calls to variadic functions:Gravatar xleroy2013-12-28
* Future-proofing: keep signature information in IA32 and PowerPC Asm, just lik...Gravatar xleroy2013-12-26
* More tweaking re: builtin_memcpyGravatar xleroy2013-11-27
* Attempted update to cchecklink re: memcpy.Gravatar xleroy2013-11-27
* powerpc/: new unary operation "addsymbol"Gravatar xleroy2013-11-17
* Update cchecklink w/ new Asm instructions Pmulh*Gravatar xleroy2013-07-29
* Add bswap16Gravatar xleroy2013-04-30
* Updated to Pbuiltin with list of resultsGravatar xleroy2013-04-30
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:Gravatar xleroy2013-04-20
* For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a ...Gravatar xleroy2013-03-18
* Updates to follow recent changes in PrintAsm.mlGravatar xleroy2013-03-01
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
* Updated to new external functions and new representation of programsGravatar xleroy2013-01-08
* - Revised non-overflow constraints on memory injections so that Gravatar xleroy2012-07-23
* checklink: dead and debug code eliminationGravatar varobert2012-07-12
* checklink: simplificationsGravatar varobert2012-07-12
* checklink: allow other number formats in configurationGravatar varobert2012-07-12
* checklink: minor fixesGravatar varobert2012-07-12
* checklink: configuration, indicate external symbolsGravatar varobert2012-07-12
* checklink: added configurabilityGravatar varobert2012-07-11
* checklink: fixed SDA inference, passes testGravatar varobert2012-07-10
* checklink: minor changesGravatar varobert2012-07-05
* checklink: better diagnosisGravatar varobert2012-07-04
* checklink: some more debug tracingGravatar varobert2012-07-04
* checklink: more defensive is_paddingGravatar varobert2012-07-04
* checklink: fixed bits/bytes mistakeGravatar varobert2012-07-04
* checklink: adaptation to the new floatsGravatar varobert2012-07-03
* checklink: IndentationGravatar varobert2012-06-29
* checklink: removed garbage codeGravatar varobert2012-06-29
* checklink: improved user-friendlinessGravatar varobert2012-06-04
* checklink: improved error messagesGravatar varobert2012-06-01
* checklink: new disassembler, error severity, ...Gravatar varobert2012-06-01
* checklink: better error messagesGravatar varobert2012-05-31
* Better error reports for checklinkGravatar varobert2012-05-30
* cchecklink continues when sections overlapGravatar varobert2012-05-24
* cchecklink now reads segments instead of sectionsGravatar varobert2012-05-10
* Fixed float comparison in checklinkGravatar varobert2012-05-02
* Added small data area support to checklinkGravatar varobert2012-04-20
* New section mapping checks and symbol data lookupGravatar varobert2012-04-13
* Added long versions of Pbf and PbtGravatar varobert2012-04-12
* Added Pallocframe second formGravatar varobert2012-04-12
* Faster ndxes_of_sym_nameGravatar varobert2012-04-12
* Tracing each data chunk in debug modeGravatar varobert2012-04-04
* Added safety to potentially overflowing arithmeticsGravatar varobert2012-04-04
* Better error messages for data symbolsGravatar 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