Skip to content

Commit

Permalink
emit only non-negative refinementconstraints
Browse files Browse the repository at this point in the history
  • Loading branch information
DrMichaelPetter committed Dec 17, 2024
1 parent 54595bd commit 6bd7861
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 3 deletions.
12 changes: 9 additions & 3 deletions src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 -> []
Expand Down
19 changes: 19 additions & 0 deletions tests/regression/77-lin2vareq/36-refinement-oppositebounds.c
Original file line number Diff line number Diff line change
@@ -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 <goblint.h>

int main()
{
int x;
if(x<100)
{
x=x;
}
__goblint_check(x<100); //UNKNOWN
__goblint_check(x>=-2147483647); //FAIL
return 0;
}


0 comments on commit 6bd7861

Please sign in to comment.