diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-01-31 14:08:17 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-01-31 14:08:17 +0100 |
commit | 1fe7f0c7ec5e1a4425eb09939d0e8f6143f1f913 (patch) | |
tree | 7b836be2205db162df62b602f097621f9d825f51 | |
parent | 06f987da5845d641106420e2de9e5bf6dba55f7b (diff) | |
download | compcert-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
-rw-r--r-- | cparser/Elab.ml | 11 |
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 *) |