diff options
-rw-r--r-- | arm/PrintAsm.ml | 2 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 2 | ||||
-rw-r--r-- | cparser/Cutil.ml | 31 | ||||
-rw-r--r-- | cparser/Cutil.mli | 4 | ||||
-rw-r--r-- | cparser/Elab.ml | 14 | ||||
-rw-r--r-- | cparser/SimplExpr.ml | 2 |
6 files changed, 33 insertions, 22 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index db95e549..50b585e1 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -752,7 +752,7 @@ let print_var oc (Coq_pair(name, v)) = fprintf oc " .size %a, . - %a\n" print_symb name print_symb name let print_program oc p = - fprintf oc " .fpu vfp\n"; +(* fprintf oc " .fpu vfp\n"; *) List.iter (print_var oc) p.prog_vars; List.iter (print_fundef oc) p.prog_funct diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 9340cc50..c6080c30 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -363,7 +363,7 @@ let first_class_value env ty = let is_volatile_access env e = List.mem C.AVolatile (Cutil.attributes_of_type env e.etyp) - && Cutil.is_lvalue env e + && Cutil.is_lvalue e let volatile_kind ty = match ty with diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 103dda49..448f488e 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -632,17 +632,26 @@ let type_of_constant = function (* Check that a C expression is a lvalue *) -let rec is_lvalue env e = - (* Type must not be array or function *) - match unroll env e.etyp with - | TFun _ | TArray _ -> false - | _ -> - match e.edesc with - | EVar id -> true - | EUnop((Oderef | Oarrow _), _) -> true - | EUnop(Odot _, e') -> is_lvalue env e' - | EBinop(Oindex, _, _, _) -> true - | _ -> false +let rec is_lvalue e = + match e.edesc with + | EVar id -> true + | EUnop((Oderef | Oarrow _), _) -> true + | EUnop(Odot _, e') -> is_lvalue e' + | EBinop(Oindex, _, _, _) -> true + | _ -> false + +(* Check that a C expression is a modifiable l-value: an l-value + whose type is not const, neither an array type, nor a function type, + nor an incomplete type. *) + +let is_modifiable_lvalue env e = + is_lvalue e + && not (List.mem AConst (attributes_of_type env e.etyp)) + && not (incomplete_type env e.etyp) + && begin match unroll env e.etyp with + | TFun _ | TArray _ -> false + | _ -> true + end (* Check that a C expression is the literal "0", which can be used as a pointer. *) diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 7bd9119e..051fafb9 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -149,8 +149,10 @@ val type_of_member : Env.t -> field -> typ small unsigned bitfields. *) val is_literal_0 : exp -> bool (* Is the given expression the integer literal "0"? *) -val is_lvalue : Env.t -> exp -> bool +val is_lvalue : exp -> bool (* Is the given expression a l-value? *) +val is_modifiable_lvalue : Env.t -> exp -> bool + (* Is the given expression a modifiable l-value? *) val valid_assignment : Env.t -> exp -> typ -> bool (* Check that an assignment of the given expression to a l-value of the given type is allowed. *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 4db7b874..a4e934bf 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -893,7 +893,7 @@ let elab_expr loc env a = | UNARY(ADDROF, a1) -> let b1 = elab a1 in - if not (is_function_type env b1.etyp || is_lvalue env b1) then + if not (is_lvalue b1 || is_function_type env b1.etyp) then err "argument of '&' is not an l-value"; { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.etyp, []) } @@ -1044,10 +1044,10 @@ let elab_expr loc env a = | BINARY(ASSIGN, a1, a2) -> let b1 = elab a1 in let b2 = elab a2 in - if not (is_lvalue env b1) then - err "left-hand side of assignment is not an l-value"; if List.mem AConst (attributes_of_type env b1.etyp) then err "left-hand side of assignment has 'const' type"; + if not (is_modifiable_lvalue env b1) then + err "left-hand side of assignment is not a modifiable l-value"; if not (valid_assignment env b2 b1.etyp) then begin if valid_cast env b2.etyp b1.etyp then warning "assigning a value of type@ %a@ to a lvalue of type@ %a" @@ -1076,10 +1076,10 @@ let elab_expr loc env a = | _ -> assert false in begin match elab (BINARY(sop, a1, a2)) with | { edesc = EBinop(_, b1, b2, _); etyp = ty } as b -> - if not (is_lvalue env b1) then - err ("left-hand side of assignment is not an l-value"); if List.mem AConst (attributes_of_type env b1.etyp) then err "left-hand side of assignment has 'const' type"; + if not (is_modifiable_lvalue env b1) then + err ("left-hand side of assignment is not a modifiable l-value"); if not (valid_assignment env b b1.etyp) then begin if valid_cast env ty b1.etyp then warning "assigning a value of type@ %a@ to a lvalue of type@ %a" @@ -1133,8 +1133,8 @@ let elab_expr loc env a = (* Elaboration of pre- or post- increment/decrement *) and elab_pre_post_incr_decr op msg a1 = let b1 = elab a1 in - if not (is_lvalue env b1) then - err "the argument of %s is not an l-value" msg; + if not (is_modifiable_lvalue env b1) then + err "the argument of %s is not a modifiable l-value" msg; if not (is_scalar_type env b1.etyp) then err "the argument of %s must be an arithmetic or pointer type" msg; { edesc = EUnop(op, b1); etyp = b1.etyp } diff --git a/cparser/SimplExpr.ml b/cparser/SimplExpr.ml index 330b1841..4184d954 100644 --- a/cparser/SimplExpr.ml +++ b/cparser/SimplExpr.ml @@ -106,7 +106,7 @@ let simpl_expr loc env e act = let is_volatile_read e = !volatilize && List.mem AVolatile (attributes_of_type env e.etyp) - && is_lvalue env e in + && is_lvalue e in let lhs_to_rhs e = if is_volatile_read e |