diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 7710815e48..b6cebe962e 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -715,13 +715,19 @@ struct | None -> [] | Some d -> let constyp = Tcons1.get_typ tcons in - let match_compa = if constyp = SUP then Gt else Ge in + (* coff*var_index + cst match_compa 0 -> cil-exp*) let mkconstraint coff index cst = + let match_compa = match constyp with + | SUPEQ when coff=Z.minus_one -> Le + | SUP when coff=Z.minus_one -> Lt + | SUPEQ when coff=Z.one -> Ge + | SUP when coff=Z.one -> Gt + | _ -> raise (Invalid_argument "refine_value_domains: not implemented") in let varifo = Option.get @@ V.to_cil_varinfo (Environment.var_of_dim t.env index) in let ik = Cilfacade.get_ikind (varifo.vtype) in let lval = Lval (Var varifo, NoOffset) in - let monom = BinOp (Mult,Cil.kintegerCilint ik coff,lval,TInt (ik,[])) in - BinOp (match_compa, monom ,Cil.kintegerCilint ik cst,Cil.intType) + let monom = lval in + BinOp (match_compa, monom ,Cil.kintegerCilint ik Z.(coff*cst),Cil.intType) in match simplified_monomials_from_texp t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with | None -> [] diff --git a/tests/regression/77-lin2vareq/36-refinement-oppositebounds.c b/tests/regression/77-lin2vareq/36-refinement-oppositebounds.c new file mode 100644 index 0000000000..54fc4eb3f0 --- /dev/null +++ b/tests/regression/77-lin2vareq/36-refinement-oppositebounds.c @@ -0,0 +1,19 @@ +//SKIP PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none +// motivated from SVCOMP's terminator_02-1.c +// checks, whether the lin2var interval refinement meddles with the wrong bounds + +#include + +int main() +{ + int x; + if(x<100) + { + x=x; + } + __goblint_check(x<100); //UNKNOWN + __goblint_check(x>=-2147483647); //FAIL + return 0; +} + +