File tree Expand file tree Collapse file tree 5 files changed +19
-12
lines changed
Expand file tree Collapse file tree 5 files changed +19
-12
lines changed Original file line number Diff line number Diff line change @@ -2030,10 +2030,11 @@ struct
20302030 match exp with
20312031 | None -> nst
20322032 | Some exp ->
2033- let t_override = match Cilfacade. fundec_return_type fundec with (* TODO: unrolltype? *)
2034- | TVoid _ -> M. warn ~category: M.Category. Program " Returning a value from a void function" ; assert false
2035- | ret -> ret
2036- in
2033+ let t_override = Cilfacade. fundec_return_type fundec in
2034+ if Cil. isVoidType t_override then (
2035+ M. warn ~category: M.Category. Program " Returning a value from a void function" ;
2036+ assert false
2037+ );
20372038 let rv = eval_rv ~man man.local exp in
20382039 let st' = set ~man ~t_override nst (return_var () ) t_override rv in
20392040 match ThreadId. get_current ask with
Original file line number Diff line number Diff line change @@ -337,11 +337,7 @@ struct
337337 | ts when Queries.TS. is_top ts ->
338338 ()
339339 | ts ->
340- let f = function (* TODO: unrolltype? *)
341- | TComp (_ , _ ) -> true
342- | _ -> false
343- in
344- if Queries.TS. exists f ts then
340+ if Queries.TS. exists Cilfacade. isStructOrUnionType ts then
345341 old_access None
346342 end ;
347343 on_ad ad
Original file line number Diff line number Diff line change @@ -503,8 +503,8 @@ struct
503503 let chosen_domain () = get_string " ana.base.structs.domain"
504504
505505 let pick_combined setting (comp : compinfo ) =
506- let all_bool () = List. for_all (fun f -> match f.ftype with TInt ( IBool , _ ) -> true | _ -> false ) comp.cfields in (* TODO: unrolltype? *)
507- let has_ptr () = List. exists (fun f -> match f.ftype with TPtr ( _ , _ ) -> true | _ -> false ) comp.cfields in (* TODO: unrolltype? *)
506+ let all_bool () = List. for_all (fun f -> Cilfacade. isBoolType f.ftype) comp.cfields in
507+ let has_ptr () = List. exists (fun f -> Cil. isPointerType f.ftype) comp.cfields in
508508 match setting with
509509 | "combined-sk" -> if has_ptr () then " keyed" else " simple"
510510 | "combined-all" ->
Original file line number Diff line number Diff line change @@ -508,7 +508,7 @@ struct
508508 | Int x when ID. to_int x = Some Z. zero -> AD. null_ptr
509509 | Int x -> AD. top_ptr
510510 (* we ignore casts to void*! TODO report UB! *)
511- | Address x -> (match t with TVoid _ -> x | _ -> cast_addr t x) (* TODO: unrolltype? *)
511+ | Address x -> (match t with TVoid _ -> x | _ -> cast_addr t x) (* TODO: unrolltype? TVoid unreachable? always goes to previous case? *)
512512 (* | Address x -> x*)
513513 | _ -> log_top __POS__; AD. top_ptr
514514 )
Original file line number Diff line number Diff line change @@ -27,6 +27,11 @@ let isCharType t =
2727 | TInt ((IChar | ISChar | IUChar ), _ ) -> true
2828 | _ -> false
2929
30+ let isBoolType t =
31+ match Cil. unrollType t with
32+ | TInt (IBool, _ ) -> true
33+ | _ -> false
34+
3035let isFloatType t =
3136 match Cil. unrollType t with
3237 | TFloat _ -> true
@@ -39,6 +44,11 @@ let rec isVLAType t = (* TODO: use in base? *)
3944 variable_len || isVLAType et
4045 | _ -> false
4146
47+ let isStructOrUnionType t =
48+ match Cil. unrollType t with
49+ | TComp _ -> true
50+ | _ -> false
51+
4252let is_first_field x = match x.fcomp.cfields with
4353 | [] -> false
4454 | f :: _ -> CilType.Fieldinfo. equal f x
You can’t perform that action at this time.
0 commit comments