aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-01-31 14:44:05 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-01-31 14:44:05 +0100
commited55884ea9749f93ffd67f0734da0907fe338102 (patch)
treeae47fd6501b1cd2b5b2de31ce5872e58d0c5170e /cparser/Elab.ml
parent3581ae495677aeca93f013d67a4d4f7c171d9cc0 (diff)
downloadcompcert-ed55884ea9749f93ffd67f0734da0907fe338102.tar.gz
compcert-ed55884ea9749f93ffd67f0734da0907fe338102.zip
Avoid overflows and report an error.
Instead of multiplying the array constant directly with the size of the offset the cautious_mul function is used to detect potential overflows. Bug 20765
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r--cparser/Elab.ml14
1 files changed, 7 insertions, 7 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 3dc1816b..61f51520 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1664,16 +1664,16 @@ let elab_expr vararg loc env a =
env,off_accu + off,ty
| ATINDEX_INIT e,TArray (sub_ty,_,_) ->
let e,env = elab env e in
- let e =
- begin match Ceval.integer_expr env e with
- | None ->
- error "array element designator for is not an integer constant expression"
- | Some n-> n
- end in
+ let e = match Ceval.integer_expr env e with
+ | None -> error "array element designator for is not an integer constant expression"
+ | Some n-> n in
let size = match sizeof env sub_ty with
| None -> assert false (* We expect only complete types *)
| Some s -> s in
- env,off_accu + size * (Int64.to_int e),sub_ty
+ let off_accu = match cautious_mul e size with
+ | None -> error "'offsetof' overflows"
+ | Some s -> off_accu + s in
+ env,off_accu,sub_ty
| ATINDEX_INIT _,_ -> error "subscripted value is not an array" in
let env,offset,_ = List.fold_left offset_of_member (env,0,ty) mem in
let size_t = size_t_ikind () in