change query result from ID.t to FlatBool.t

src/analyses/apron/relationAnalysis.apron.ml

@@ -877,7 +877,10 @@ struct
       if M.tracing then M.trace "relationalArray" "v=%a -> %a %a d=%i\n" CilType.Varinfo.pretty v CilType.Varinfo.pretty newVar d_exp  exp d;
       let i = eval_int comp (no_overflow ask comp ) in 
       if M.tracing then M.trace "relationalArray" "comp: %a\n result=%a\n" d_exp comp ID.pretty i;
-      i 
+      begin match ValueDomainQueries.ID.to_bool i with 
+        | Some b -> `Lifted b 
+        | _ -> `Top
+      end
     | AllocMayBeOutOfBounds {exp=e;e1_offset= i;struct_offset= o; _} -> 
       let inBoundsForAllAddresses indexExp = begin match ctx.ask (Queries.MayPointTo e) with 
         | a when not (Queries.AD.is_top a) -> 

src/cdomain/value/cdomains/arrayDomain.ml

@@ -843,8 +843,11 @@ let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l)
       | None -> 
         (match arrExpDim, e with 
          | Some (Some(Var arr_lval, _),counter ), Some exp ->
-           if M.tracing then M.trace "relationalArray" "c=%a e=%a" CilType.Varinfo.pretty arr_lval d_exp exp;
-           ValueDomainQueries.ID.to_bool (ask.may_be_out_of_bounds (arr_lval, counter ) exp)
+           if M.tracing then M.trace "relationalArray" "c=%a e=%a\n" CilType.Varinfo.pretty arr_lval d_exp exp;
+           begin match (ask.may_be_out_of_bounds (arr_lval, counter ) exp) with 
+             | `Lifted b -> Some  b 
+             | _ -> None 
+           end
          | _, _ -> None) 
       | b -> b in
 

src/cdomain/value/domains/valueDomainQueries.ml

@@ -52,7 +52,7 @@ end
 type eval_int = exp -> ID.t
 type may_point_to = exp -> AD.t
 type is_multiple = varinfo -> bool
-type may_be_out_of_bounds = (varinfo * int) -> exp -> ID.t
+type may_be_out_of_bounds = (varinfo * int) -> exp -> FlatBool.t
 
 (** Subset of queries used by the valuedomain, using a simpler representation. *)
 type t = {

src/domains/queries.ml

@@ -33,6 +33,7 @@ module AD = ValueDomain.AD
 
 module MayBool = BoolDomain.MayBool
 module MustBool = BoolDomain.MustBool
+module FlatBool = BoolDomain.FlatBool
 
 module Unit = Lattice.Unit
 
@@ -127,7 +128,7 @@ type _ t =
   | MustTermAllLoops: MustBool.t t
   | IsEverMultiThreaded: MayBool.t t
   | TmpSpecial:  Mval.Exp.t -> ML.t t
-  | MayBeOutOfBounds: maybeoutofbounds -> ID.t t
+  | MayBeOutOfBounds: maybeoutofbounds -> FlatBool.t t
   | NoOverflow : exp -> MayBool.t t
   | AllocMayBeOutOfBounds : allocmaybeoutofbounds -> VDQ.ProdID.t t
   | AllocAssignedToGlobal : varinfo -> MustBool.t t
@@ -200,7 +201,7 @@ struct
     | MustTermAllLoops -> (module MustBool)
     | IsEverMultiThreaded -> (module MayBool)
     | TmpSpecial _ -> (module ML)
-    | MayBeOutOfBounds _ -> (module ID)
+    | MayBeOutOfBounds _ -> (module FlatBool)
     | NoOverflow _ -> (module MayBool)
     | AllocMayBeOutOfBounds _ -> (module VDQ.ProdID)
     | AllocAssignedToGlobal _ -> (module MustBool)
@@ -273,7 +274,7 @@ struct
     | IsEverMultiThreaded -> MayBool.top ()
     | TmpSpecial _ -> ML.top ()
     | MayBeOutOfBounds _ -> ID.top ()
-    | NoOverflow _ -> MayBool.top ()
+    | NoOverflow _ -> FlatBool.top ()
     | AllocMayBeOutOfBounds _ -> VDQ.ProdID.top ()
     | AllocAssignedToGlobal _ -> MustBool.top ()
 end