Skip to content

Commit

Permalink
RelationalAnalysis: Assert type-bounds also for signed types when no-…
Browse files Browse the repository at this point in the history
…overflow is assumed.
  • Loading branch information
jerhard committed Nov 15, 2023
1 parent b57b9e4 commit 70ef2d2
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions src/analyses/apron/relationAnalysis.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -196,15 +196,14 @@ struct
let assert_type_bounds ask rel x =
assert (RD.Tracked.varinfo_tracked x);
match Cilfacade.get_ikind x.vtype with
| ik when not (IntDomain.should_ignore_overflow ik) -> (* don't add type bounds for signed when assume_none *)
| ik -> (* don't add type bounds for signed when assume_none *)
let (type_min, type_max) = IntDomain.Size.range ik in
(* TODO: don't go through CIL exp? *)
let e1 = BinOp (Le, Lval (Cil.var x), (Cil.kintegerCilint ik type_max), intType) in
let e2 = BinOp (Ge, Lval (Cil.var x), (Cil.kintegerCilint ik type_min), intType) in
let rel = RD.assert_inv rel e1 false (no_overflow ask e1) in (* TODO: how can be overflow when asserting type bounds? *)
let rel = RD.assert_inv rel e2 false (no_overflow ask e2) in
rel
| _
| exception Invalid_argument _ ->
rel

Expand Down

0 comments on commit 70ef2d2

Please sign in to comment.