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 /cparser/Elab.ml | |
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
Diffstat (limited to 'cparser/Elab.ml')
-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 *) |