emit only non-negative refinementconstraints

Author: DrMichaelPetter

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 -> []

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 <goblint.h>
+
+int main()
+{
+  int x;
+  if(x<100) 
+  {
+    x=x;
+  }                           
+  __goblint_check(x<100); //UNKNOWN
+  __goblint_check(x>=-2147483647); //FAIL
+  return 0;
+}
+
+