aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-01-31 14:08:17 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-01-31 14:08:17 +0100
commit1fe7f0c7ec5e1a4425eb09939d0e8f6143f1f913 (patch)
tree7b836be2205db162df62b602f097621f9d825f51 /cparser
parent06f987da5845d641106420e2de9e5bf6dba55f7b (diff)
downloadcompcert-1fe7f0c7ec5e1a4425eb09939d0e8f6143f1f913.tar.gz
compcert-1fe7f0c7ec5e1a4425eb09939d0e8f6143f1f913.zip
Remove superfluous check.
Gcc and clang do not raise an error for this, also it should work for the last array element which can be without size. Bug 20765
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Elab.ml11
1 files changed, 4 insertions, 7 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 68dd1b76..f4f1586c 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1662,16 +1662,13 @@ let elab_expr vararg loc env a =
let flds = List.rev flds in
let off,ty = offset_of_list 0 env ty flds in
env,off_accu + off,ty
- | ATINDEX_INIT e,TArray (sub_ty,b,_) ->
+ | ATINDEX_INIT e,TArray (sub_ty,_,_) ->
let e,env = elab env e in
let e =
- begin match Ceval.integer_expr env e,b with
- | None,_ ->
+ begin match Ceval.integer_expr env e with
+ | None ->
error "array element designator for is not an integer constant expression"
- | Some n,Some b -> if n >= b then
- error "array index %Ld exceeds array bounds" n;
- n
- | Some n,None -> assert false
+ | Some n-> n
end in
let size = match sizeof env sub_ty with
| None -> assert false (* We expect only complete types *)