aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Inject.v
Commit message (Expand)AuthorAgeFilesLines
* Adding copyrightsCyril SIX2020-05-041-0/+12
* adapt for Icond with predicted directionDavid Monniaux2020-04-161-2/+2
* begin adapting for LICM phaseDavid Monniaux2020-04-011-2/+2
* now able to inject on CallDavid Monniaux2020-04-011-1/+1
* except for builtins, finished the proofDavid Monniaux2020-03-311-1/+1
* INJnopDavid Monniaux2020-03-311-0/+3
* lemma on stepping through non trapping instructionsDavid Monniaux2020-03-301-10/+18
* additional checksDavid Monniaux2020-03-301-1/+11
* injector wrapper functionDavid Monniaux2020-03-301-0/+22
* use inject_lDavid Monniaux2020-03-301-0/+7
* more on injectionDavid Monniaux2020-03-301-0/+10
* more on injectionDavid Monniaux2020-03-301-2/+4
* begin coding dead code injectorDavid Monniaux2020-03-291-0/+60