@@ -2215,21 +2215,21 @@ struct
22152215 if CilType.Typ. equal s1_typ charPtrType && CilType.Typ. equal s2_typ charPtrType then
22162216 begin match lv, op_addr with
22172217 | Some lv_val , Some f ->
2218- (* when whished types coincide, compute result of operation op_addr, otherwise use top *)
2219- let lv_a = eval_lv (Analyses. ask_of_ctx ctx) gs st lv_val in
2220- let lv_typ = Cilfacade. typeOfLval lv_val in
2221- if all && typeSig s1_typ = typeSig s2_typ && typeSig s2_typ = typeSig lv_typ then (* all types need to coincide *)
2222- set ~ctx (Analyses. ask_of_ctx ctx) gs st lv_a lv_typ (f s1_a s2_a)
2223- else if not all && typeSig s1_typ = typeSig s2_typ then (* only the types of s1 and s2 need to coincide *)
2224- set ~ctx (Analyses. ask_of_ctx ctx) gs st lv_a lv_typ (f s1_a s2_a)
2225- else
2226- set ~ctx (Analyses. ask_of_ctx ctx) gs st lv_a lv_typ (VD. top_value (unrollType lv_typ))
2218+ (* when whished types coincide, compute result of operation op_addr, otherwise use top *)
2219+ let lv_a = eval_lv (Analyses. ask_of_ctx ctx) gs st lv_val in
2220+ let lv_typ = Cilfacade. typeOfLval lv_val in
2221+ if all && typeSig s1_typ = typeSig s2_typ && typeSig s2_typ = typeSig lv_typ then (* all types need to coincide *)
2222+ set ~ctx (Analyses. ask_of_ctx ctx) gs st lv_a lv_typ (f s1_a s2_a)
2223+ else if not all && typeSig s1_typ = typeSig s2_typ then (* only the types of s1 and s2 need to coincide *)
2224+ set ~ctx (Analyses. ask_of_ctx ctx) gs st lv_a lv_typ (f s1_a s2_a)
2225+ else
2226+ set ~ctx (Analyses. ask_of_ctx ctx) gs st lv_a lv_typ (VD. top_value (unrollType lv_typ))
22272227 | _ ->
22282228 (* check if s1 is potentially a string literal as writing to it would be undefined behavior; then return top *)
22292229 let _ = AD. string_writing_defined s1_a in
22302230 set ~ctx (Analyses. ask_of_ctx ctx) gs st s1_a s1_typ (VD. top_value (unrollType s1_typ))
22312231 end
2232- (* else compute value in array domain *)
2232+ (* else compute value in array domain *)
22332233 else
22342234 let lv_a, lv_typ = match lv with
22352235 | Some lv_val -> eval_lv (Analyses. ask_of_ctx ctx) gs st lv_val, Cilfacade. typeOfLval lv_val
@@ -2326,11 +2326,11 @@ struct
23262326 if needle is substring, assign the substring of haystack starting at the first occurrence of needle to dest,
23272327 if it surely isn't, assign a null_ptr *)
23282328 string_manipulation haystack needle lv true (Some (fun h_a n_a -> Address (AD. substring_extraction h_a n_a)))
2329- (fun h_ar n_ar -> match CArrays. substring_extraction h_ar n_ar with
2330- | CArrays. IsNotSubstr -> Address (AD. null_ptr)
2331- | CArrays. IsSubstrAtIndex0 -> Address (eval_lv (Analyses. ask_of_ctx ctx) gs st (mkMem ~addr: (Cil. stripCasts haystack) ~off: NoOffset ))
2332- | CArrays. IsMaybeSubstr -> Address (AD. join (eval_lv (Analyses. ask_of_ctx ctx) gs st
2333- (mkMem ~addr: (Cil. stripCasts haystack) ~off: (Index (Offset.Index.Exp. any, NoOffset )))) (AD. null_ptr)))
2329+ (fun h_ar n_ar -> match CArrays. substring_extraction h_ar n_ar with
2330+ | CArrays. IsNotSubstr -> Address (AD. null_ptr)
2331+ | CArrays. IsSubstrAtIndex0 -> Address (eval_lv (Analyses. ask_of_ctx ctx) gs st (mkMem ~addr: (Cil. stripCasts haystack) ~off: NoOffset ))
2332+ | CArrays. IsMaybeSubstr -> Address (AD. join (eval_lv (Analyses. ask_of_ctx ctx) gs st
2333+ (mkMem ~addr: (Cil. stripCasts haystack) ~off: (Index (Offset.Index.Exp. any, NoOffset )))) (AD. null_ptr)))
23342334 | None -> st
23352335 end
23362336 | Strcmp { s1; s2; n } , _ ->
0 commit comments