aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cexec.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-03-27 15:28:20 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2015-03-27 15:28:20 +0100
commite11b3b885a6d359925b86743b89698cc6757157a (patch)
tree4729067203418873c940aa27d45085ca9881905d /cfrontend/Cexec.v
parent33b742bb41725e47bd88dc12f2a4f40173023f83 (diff)
downloadcompcert-kvx-e11b3b885a6d359925b86743b89698cc6757157a.tar.gz
compcert-kvx-e11b3b885a6d359925b86743b89698cc6757157a.zip
Updating the PowerPC and ARM ports.
PowerPC: always use full register names to print annotations.
Diffstat (limited to 'cfrontend/Cexec.v')
0 files changed, 0 insertions, 0 deletions