summaryrefslogtreecommitdiff
path: root/checklink
Commit message (Expand)AuthorAge
* Follow-up to commit 2613Gravatar xleroy2014-08-20
* Add builtins for load with reservation and conditional store.Gravatar xleroy2014-08-20
* checklink/Check.ml: missing SDA addressing for store instructions.Gravatar xleroy2014-08-19
* powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.Gravatar xleroy2014-08-18
* 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
* Add _a memory accesses.Gravatar xleroy2014-07-23
* - 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: more stringent compilationGravatar varobert2012-07-11
* checklink: fixed SDA inference, passes testGravatar varobert2012-07-10
* Revert unintentional commit #1955Gravatar xleroy2012-07-06
* checklink: minor changesGravatar varobert2012-07-05
* Ajout trunk CompCertGravatar blazy2012-07-04
* 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: Faster printingGravatar varobert2012-06-29
* 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
* checklink: fixed FSQRTEx parsingGravatar 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-18 13:30:24 +0000