Skip to content

Commit

Permalink
Fix too broad try block in BaseInvariant
Browse files Browse the repository at this point in the history
Caused Invalid_argument("Cilfacade.get_fkind: non-float type int ") before,
even though integer case is checked first,
but something else in it raises.
  • Loading branch information
sim642 committed Oct 9, 2023
1 parent 093eb5e commit 8468a5a
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/analyses/baseInvariant.ml
Original file line number Diff line number Diff line change
Expand Up @@ -805,15 +805,15 @@ struct
| BinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _, _) -> true
| _ -> false
in
try
let ik = Cilfacade.get_ikind_exp exp in
match Cilfacade.get_ikind_exp exp with
| ik ->
let itv = if not tv || is_cmp exp then (* false is 0, but true can be anything that is not 0, except for comparisons which yield 1 *)
ID.of_bool ik tv (* this will give 1 for true which is only ok for comparisons *)
else
ID.of_excl_list ik [BI.zero] (* Lvals, Casts, arithmetic operations etc. should work with true = non_zero *)
in
inv_exp (Int itv) exp st
with Invalid_argument _ ->
| exception Invalid_argument _ ->
let fk = Cilfacade.get_fkind_exp exp in
let ftv = if not tv then (* false is 0, but true can be anything that is not 0, except for comparisons which yield 1 *)
FD.of_const fk 0.
Expand Down

0 comments on commit 8468a5a

Please sign in to comment.