aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Asmgenproof.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-08-21 15:35:13 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-08-21 15:35:13 +0200
commit84c3580d0514c24a7c29eeec635e16183c3c5c65 (patch)
treef4202f012faf10d41b9c0285b5fd1d2cebe21c1c /powerpc/Asmgenproof.v
parent78808873d889608ee39fb6a9d9c0dac0335ccf47 (diff)
downloadcompcert-kvx-84c3580d0514c24a7c29eeec635e16183c3c5c65.tar.gz
compcert-kvx-84c3580d0514c24a7c29eeec635e16183c3c5c65.zip
Simplify the handling of extended inline asm, taking advantage of the new, structured builtin arguments and results.
Diffstat (limited to 'powerpc/Asmgenproof.v')
0 files changed, 0 insertions, 0 deletions