arm/PrintAsm: don't generate "vfd" directive, useless?

cparser: distinguish more carefully between lvalues and modifiable lvalues.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1722 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 31 insertions, 20 deletions

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 103dda4..448f488 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 7bd9119..051fafb 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 4db7b87..a4e934b 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 330b184..4184d95 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