From 6bd7861bc6fb052867a0df07c75a3284c1d3c214 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Tue, 17 Dec 2024 10:56:09 +0100 Subject: [PATCH] emit only non-negative refinementconstraints --- .../apron/linearTwoVarEqualityDomain.apron.ml | 12 +++++++++--- .../36-refinement-oppositebounds.c | 19 +++++++++++++++++++ 2 files changed, 28 insertions(+), 3 deletions(-) create mode 100644 tests/regression/77-lin2vareq/36-refinement-oppositebounds.c 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; +} + +