@@ -907,26 +907,26 @@ struct
907907
908908 (* Funny, this does not compile without the final type annotation! *)
909909 let rec eval_offset (ask : VDQ.t ) f (x : t ) (offs :offs ) (exp :exp option ) (v :lval option ) (t :typ ): t =
910- let rec do_eval_offset (ask :VDQ.t ) f ( x :t ) (offs :offs ) (exp :exp option ) ( l :lval option ) (o :offset option ) ( v :lval option ) ( t :typ ): t =
910+ let rec do_eval_offset (x :t ) (offs :offs ) (l :lval option ) (o :offset option ): t =
911911 if M. tracing then M. traceli " eval_offset" " do_eval_offset %a %a (%a)" pretty x Offs. pretty offs (Pretty. docOpt (CilType.Exp. pretty () )) exp;
912912 let r =
913913 match x, offs with
914914 | Blob ((va , _ , zeroinit ) as c ), `Index (_ , ox ) ->
915915 begin
916916 let l', o' = shift_one_over l o in
917- let ev = do_eval_offset ask f (Blobs. value c) ox exp l' o' v t in
917+ let ev = do_eval_offset (Blobs. value c) ox l' o' in
918918 zero_init_calloced_memory zeroinit ev t
919919 end
920920 | Blob ((va , _ , zeroinit ) as c ), `Field _ ->
921921 begin
922922 let l', o' = shift_one_over l o in
923- let ev = do_eval_offset ask f (Blobs. value c) offs exp l' o' v t in
923+ let ev = do_eval_offset (Blobs. value c) offs l' o' in
924924 zero_init_calloced_memory zeroinit ev t
925925 end
926926 | Blob ((va , _ , zeroinit ) as c ), `NoOffset ->
927927 begin
928928 let l', o' = shift_one_over l o in
929- let ev = do_eval_offset ask f (Blobs. value c) offs exp l' o' v t in
929+ let ev = do_eval_offset (Blobs. value c) offs l' o' in
930930 zero_init_calloced_memory zeroinit ev t
931931 end
932932 | Bot , _ -> Bot
@@ -938,7 +938,7 @@ struct
938938 | Struct str ->
939939 let x = Structs. get str fld in
940940 let l', o' = shift_one_over l o in
941- do_eval_offset ask f x offs exp l' o' v t
941+ do_eval_offset x offs l' o'
942942 | Top -> M. info ~category: Imprecise " Trying to read a field, but the struct is unknown" ; top ()
943943 | _ -> M. warn ~category: Imprecise ~tags: [Category Program ] " Trying to read a field, but was not given a struct" ; top ()
944944 end
@@ -953,7 +953,7 @@ struct
953953 | _ ->
954954 let x = cast ~kind: Internal fld.ftype value in (* TODO: proper castkind *)
955955 let l', o' = shift_one_over l o in
956- do_eval_offset ask f x offs exp l' o' v t )
956+ do_eval_offset x offs l' o')
957957 | Union _ -> top ()
958958 | Top -> M. info ~category: Imprecise " Trying to read a field, but the union is unknown" ; top ()
959959 | _ -> M. warn ~category: Imprecise ~tags: [Category Program ] " Trying to read a field, but was not given a union" ; top ()
@@ -963,12 +963,12 @@ struct
963963 match x with
964964 | Array x ->
965965 let e = determine_offset ask l o exp v in
966- do_eval_offset ask f (CArrays. get ask x (e, idx)) offs exp l' o' v t
966+ do_eval_offset (CArrays. get ask x (e, idx)) offs l' o'
967967 | Address _ ->
968968 begin
969- do_eval_offset ask f x offs exp l' o' v t (* this used to be `blob `address -> we ignore the index *)
969+ do_eval_offset x offs l' o' (* this used to be `blob `address -> we ignore the index *)
970970 end
971- | x when GobOption. exists (Z. equal Z. zero) (IndexDomain. to_int idx) -> eval_offset ask f x offs exp v t
971+ | x when GobOption. exists (Z. equal Z. zero) (IndexDomain. to_int idx) -> eval_offset ask f x offs exp v t (* TODO: why recursive call to outer function? *)
972972 | Top -> M. info ~category: Imprecise " Trying to read an index, but the array is unknown" ; top ()
973973 | _ -> M. warn ~category: Imprecise ~tags: [Category Program ] " Trying to read an index, but was not given an array (%a)" pretty x; top ()
974974 end
@@ -980,7 +980,7 @@ struct
980980 | Some (Lval (x ,o )) -> Some ((x, NoOffset )), Some (o)
981981 | _ -> None , None
982982 in
983- do_eval_offset ask f x offs exp l o v t
983+ do_eval_offset x offs l o
984984
985985 let update_offset ?(blob_destructive =false ) (ask : VDQ.t ) (x :t ) (offs :offs ) (value :t ) (exp :exp option ) (v :lval ) (t :typ ): t =
986986 let rec do_update_offset ?(bitfield :int option=None ) (ask :VDQ.t ) (x :t ) (offs :offs ) (value :t ) (exp :exp option ) (l :lval option ) (o :offset option ) (v :lval ) (t :typ ):t =
0 commit comments