diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 8497f38615..4911b0d033 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1765,25 +1765,26 @@ struct | _ -> res in (* bodge for abs(...); To be removed once we have a clean solution *) - let refineAbs absargexp valexp = - (* e.g. |arg| < 40 *) + let refineAbs op absargexp valexp = + let flip op = match op with | Le -> Ge | Lt -> Gt | _ -> failwith "impossible" in + (* e.g. |arg| <= 40 *) (* arg <= e (arg <= 40) *) - let le = BinOp (Le, absargexp, valexp, intType) in + let le = BinOp (op, absargexp, valexp, intType) in (* arg >= -e (arg >= -40) *) - let gt = BinOp(Ge, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in + let gt = BinOp(flip op, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv in match exp with - | BinOp (Lt, CastE(t, Lval (Var v, NoOffset)), e,_) when tv -> + | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv -> (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with | `Lifted (Abs arg) -> - refineAbs (CastE (t, arg)) e + refineAbs op (CastE (t, arg)) e | _ -> refine0) - | BinOp (Lt, Lval (Var v, NoOffset), e, _) when tv -> + | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv -> (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with | `Lifted (Abs arg) -> - refineAbs arg e + refineAbs op arg e | _ -> refine0) | _ -> refine0 in diff --git a/tests/regression/39-signed-overflows/06-abs.c b/tests/regression/39-signed-overflows/06-abs.c index e87e25d9fe..e56cc9ff7d 100644 --- a/tests/regression/39-signed-overflows/06-abs.c +++ b/tests/regression/39-signed-overflows/06-abs.c @@ -6,7 +6,16 @@ int main() { { if (abs(data) < 100) { - int result = data * data; + __goblint_check(data < 100); + __goblint_check(-100 < data); + int result = data * data; //NOWARN + } + + if(abs(data) <= 100) + { + __goblint_check(data <= 100); + __goblint_check(-100 <= data); + int result = data * data; //NOWARN } } return 8;