aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | | | | | | returnDavid Monniaux2020-03-311-1/+29
| * | | | | | | jumptableDavid Monniaux2020-03-311-1/+22
| * | | | | | | condDavid Monniaux2020-03-311-2/+54
| * | | | | | | builtin (incomplete)David Monniaux2020-03-311-0/+33
| * | | | | | | tailcallDavid Monniaux2020-03-311-1/+58
| * | | | | | | call (could not handle it)David Monniaux2020-03-311-1/+62
| * | | | | | | storeDavid Monniaux2020-03-311-1/+42
| * | | | | | | loadsDavid Monniaux2020-03-311-3/+126
| * | | | | | | lots of admits to be filledDavid Monniaux2020-03-311-13/+134
| * | | | | | | transf_function_redirectsDavid Monniaux2020-03-311-0/+109
| * | | | | | | INJnopDavid Monniaux2020-03-312-1/+8
| * | | | | | | transf_function_inj_plusstepDavid Monniaux2020-03-311-0/+25
| * | | | | | | transf_function_inj_endDavid Monniaux2020-03-311-0/+57
| * | | | | | | injector "ghost steps"David Monniaux2020-03-311-4/+35
| * | | | | | | one more admitDavid Monniaux2020-03-311-7/+85
| * | | | | | | lemma on stepping through non trapping instructionsDavid Monniaux2020-03-303-19/+126
| * | | | | | | additional checksDavid Monniaux2020-03-301-1/+11
| * | | | | | | more proofs on injectorDavid Monniaux2020-03-301-1/+173
| * | | | | | | injector wrapper functionDavid Monniaux2020-03-301-0/+22
| * | | | | | | use inject_lDavid Monniaux2020-03-303-19/+11
| * | | | | | | inject_l_redirectsDavid Monniaux2020-03-301-0/+82
| * | | | | | | inject_l injected_endDavid Monniaux2020-03-301-0/+90
| * | | | | | | inject_l injectedDavid Monniaux2020-03-301-4/+43
| * | | | | | | injection positions..David Monniaux2020-03-301-4/+49
| * | | | | | | injection positions are okDavid Monniaux2020-03-301-0/+24
| * | | | | | | inject_at injects the endDavid Monniaux2020-03-301-5/+26
| * | | | | | | injector injects the endDavid Monniaux2020-03-301-4/+19
| * | | | | | | injector injects..David Monniaux2020-03-301-0/+69
| * | | | | | | preservation lemmasDavid Monniaux2020-03-301-0/+155
| * | | | | | | more on injectionDavid Monniaux2020-03-301-0/+10
| * | | | | | | more on injectionDavid Monniaux2020-03-302-2/+5
| * | | | | | | begin coding dead code injectorDavid Monniaux2020-03-291-0/+60
| * | | | | | | nop insertion at entrypointDavid Monniaux2020-03-292-16/+24
* | | | | | | | bump Coq versionDavid Monniaux2020-04-131-11/+11
* | | | | | | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-1243-45/+1741
|\ \ \ \ \ \ \ \
| * | | | | | | | profiling instructionsDavid Monniaux2020-04-121-1/+5
| * | | | | | | | instructionsDavid Monniaux2020-04-121-0/+30
| * | | | | | | | now use COMPCERT_PROFILING_DATA and don't print stuffDavid Monniaux2020-04-121-2/+10
| * | | | | | | | fix IA32 profiling bugDavid Monniaux2020-04-121-2/+4
| * | | | | | | | x86-64 profilingDavid Monniaux2020-04-123-8/+65
| * | | | | | | | otherwise timings disabled on arm (ccomp should call preprocessor with approp...David Monniaux2020-04-121-1/+1
| * | | | | | | | fix reverse printing problem for hashesDavid Monniaux2020-04-114-46/+65
| * | | | | | | | fix for k1cDavid Monniaux2020-04-112-3/+3
| * | | | | | | | fix for aarch64David Monniaux2020-04-112-1/+5
| * | | | | | | | seems like the ARM profiling perhaps worksDavid Monniaux2020-04-116-8/+58
| * | | | | | | | for running benchmarks on marteDavid Monniaux2020-04-101-0/+16
| * | | | | | | | fix for running the profile code on hostDavid Monniaux2020-04-101-6/+8
| * | | | | | | | fixing MakefileDavid Monniaux2020-04-102-5/+23
| * | | | | | | | fix writing profiling info for Aarch64David Monniaux2020-04-103-11/+38
| * | | | | | | | use proper local labelsDavid Monniaux2020-04-104-5/+6
generated by cgit (git 2.34.1) at 2024-07-12 01:04:47 +0000