aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/ExtValues.v
Commit message (Expand)AuthorAgeFilesLines
* detailDavid Monniaux2019-05-151-1/+1
* more lemmas on divisionDavid Monniaux2019-05-151-0/+48
* more lemmas on divisionDavid Monniaux2019-05-151-1/+55
* some lemmas on division etc.David Monniaux2019-05-141-0/+258
* 32-bit modulo now uses sign extend then call to the 64-bit functionDavid Monniaux2019-05-131-0/+36
* we directly call 64-bit unsigned divisionDavid Monniaux2019-05-131-1/+1
* begin proving that we can use 64-bit division for doing 32David Monniaux2019-05-131-0/+64
* Srsd / SrswDavid Monniaux2019-04-291-0/+18
* detect insf case, beginDavid Monniaux2019-04-281-4/+11
* compute the highest bit in a numberDavid Monniaux2019-04-271-0/+10
* add bitfield insert opcode but not yet used nor translatedDavid Monniaux2019-04-271-4/+10
* more base operators on bitfieldDavid Monniaux2019-04-271-0/+19
* factor expressions into single fileDavid Monniaux2019-04-271-12/+14
* moved operators to specific file instead of common fileDavid Monniaux2019-04-271-0/+57