summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-10-16 06:59:55 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-10-16 06:59:55 +0000
commit32b9fdc4332a6af5d108a0468399661867f4d2b4 (patch)
treeba455fb82bea4c5a4b9a9465a485898fbb8c09c9
parent1d40928b2df6dd395c5c32a21f0ae41a56f74bea (diff)
Warn for volatile accesses to composites
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2344 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--cfrontend/C2C.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index dd9cfbf..a121678 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -431,6 +431,10 @@ let rec convertExpr env e =
| C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _)
| C.EBinop(C.Oindex, _, _, _) ->
let l = convertLvalue env e in
+ if Cutil.is_composite_type env e.etyp
+ && List.mem AVolatile (Cutil.attributes_of_type env e.etyp) then
+ warning "access to a l-value of volatile composite type. \
+ The 'volatile' qualifier is ignored.";
Evalof(l, ty)
| C.EConst(C.CInt(i, (ILongLong|IULongLong), _)) ->
@@ -498,6 +502,10 @@ let rec convertExpr env e =
| C.EBinop(C.Oassign, e1, e2, _) ->
let e1' = convertLvalue env e1 in
let e2' = convertExpr env e2 in
+ if Cutil.is_composite_type env e1.etyp
+ && List.mem AVolatile (Cutil.attributes_of_type env e1.etyp) then
+ warning "assignment to a l-value of volatile composite type. \
+ The 'volatile' qualifier is ignored.";
Eassign(e1', e2', ty)
| C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign|
C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign|