aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cminorgenproof.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-04-28 13:17:30 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-04-28 13:17:30 +0200
commit74c3e0e8615c2d943eae813b82b11cbfe74d4a82 (patch)
tree1901feb7ca3bc0e2f293b21c582e52b69a84c61f /cfrontend/Cminorgenproof.v
parent916bfc0c4f2a025e9aa642cf616cd8c6ace4ec70 (diff)
downloadcompcert-74c3e0e8615c2d943eae813b82b11cbfe74d4a82.tar.gz
compcert-74c3e0e8615c2d943eae813b82b11cbfe74d4a82.zip
Detect and reject "&" operator applied to "register" local variable or to a bit field.
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
0 files changed, 0 insertions, 0 deletions