improve values of parameters in abs call

goblint · Nov 17, 2023 · 5663482 · 5663482
1 parent b9ede51
commit 5663482
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
@@ -726,6 +726,8 @@ struct
                             | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
                             | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
                             | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
+                            | `Lifted (Abs xInt) ->
+                              inv_exp (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st
                             | _ -> update_lval c x c' ID.pretty
                           end
                         | None -> update_lval c x c' ID.pretty