Skip to content

Commit

Permalink
ad_invariants: Do not generate invariants for pointers when the point…
Browse files Browse the repository at this point in the history
…ed-to type is void.

If some block has void-type in our abstract domain, we cannot produce meaningful invariants, because we cannot insert the necessary casts easily.
To generate invariants even for these casees, one may try to determine the type to cast to by looking at the abstract value more closely.
  • Loading branch information
jerhard committed Oct 13, 2022
1 parent 04aa143 commit e52b3c0
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/cdomains/valueDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1248,6 +1248,7 @@ struct
in
let i_deref =
match Cilfacade.typeOfLval (Var vi, offset) with
| TVoid _ -> Invariant.none (* TODO: Try to determine type of abstract value and introduce appropriate casts *)
| typ ->
(* Address set for a void* variable contains pointers to values of non-void type,
so insert pointer cast to make invariant expression valid (no field/index on void). *)
Expand Down

0 comments on commit e52b3c0

Please sign in to comment.