Add TODOs for other uses of Queries.eval_bool

Author: sim642

src/analyses/abortUnless.ml

@@ -30,7 +30,7 @@ struct
     if man.local then
       match f.sformals with
       | [arg] when isIntegralType arg.vtype ->
-        (match man.ask (EvalInt (Lval (Var arg, NoOffset))) with
+        (match man.ask (EvalInt (Lval (Var arg, NoOffset))) with (* TODO: Queries.eval_bool? *)
          | v when Queries.ID.is_bot v -> false
          | v ->
            match Queries.ID.to_bool v with

src/analyses/memLeak.ml

@@ -228,7 +228,7 @@ struct
       warn_for_multi_threaded_due_to_abort man;
       state
     | Assert { exp; _ } ->
-      begin match man.ask (Queries.EvalInt exp) with
+      begin match man.ask (Queries.EvalInt exp) with (* TODO: Queries.eval_bool? *)
         | a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp
         | a ->
           begin match Queries.ID.to_bool a with

src/analyses/unassumeAnalysis.ml

@@ -261,7 +261,7 @@ struct
       let e = List.fold_left (fun a {exp = b; _} -> Cil.(BinOp (LAnd, a, b, intType))) x.exp xs in
       M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e;
       if not !AnalysisState.postsolving then (
-        if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (man.ask (EvalInt e)) = Some false) then (
+        if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (man.ask (EvalInt e)) = Some false) then ( (* TODO: Queries.eval_bool? *)
           let tokens = x.token :: List.map (fun {token; _} -> token) xs in
           man.emit (Unassume {exp = e; tokens});
           List.iter WideningTokenLifter.add tokens
@@ -280,7 +280,7 @@ struct
   let body man fd =
     let pres = FH.find_all fun_pres fd in
     let st = List.fold_left (fun acc pre ->
-        let v = man.ask (EvalInt pre) in
+        let v = man.ask (EvalInt pre) in (* TODO: Queries.eval_bool? *)
         (* M.debug ~category:Witness "%a precondition %a evaluated to %a" CilType.Fundec.pretty fd CilType.Exp.pretty pre Queries.ID.pretty v; *)
         if Queries.ID.to_bool v = Some true then
           D.add pre acc

src/transform/expressionEvaluation.ml

@@ -125,7 +125,7 @@ struct
                 value_after
 
       method private try_ask location expression =
-        match ~? (fun () -> (ask location).Queries.f (Queries.EvalInt expression)) with
+        match ~? (fun () -> (ask location).Queries.f (Queries.EvalInt expression)) with (* TODO: Queries.eval_bool? *)
         (* Inapplicable: Unreachable *)
         | Some x when Queries.ID.is_bot_ikind x -> None
         | Some x ->

src/witness/yamlWitness.ml

@@ -454,7 +454,7 @@ struct
                   | `Lifted c_inv ->
                     (* Collect all start states that may satisfy the invariant of current_c *)
                     List.iter (fun c ->
-                        let x = R.ask_local (c.node, c.context) ~local:c.state (Queries.EvalInt c_inv) in
+                        let x = R.ask_local (c.node, c.context) ~local:c.state (Queries.EvalInt c_inv) in (* TODO: Queries.eval_bool? *)
                         if Queries.ID.is_bot x || Queries.ID.is_bot_ikind x then (* dead code *)
                           failwith "Bottom not expected when querying context state" (* Maybe this is reachable, failwith for now so we see when this happens *)
                         else if Queries.ID.to_bool x = Some false then () (* Nothing to do, the c does definitely not satisfy the predicate of current_c *)
@@ -747,7 +747,7 @@ struct
 
               let result: VR.result = match InvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs with
                 | Ok inv_exp ->
-                  let x = ask_local lvar (Queries.EvalInt inv_exp) in
+                  let x = ask_local lvar (Queries.EvalInt inv_exp) in (* TODO: Queries.eval_bool? *)
                   if Queries.ID.is_bot x || Queries.ID.is_bot_ikind x then (* dead code *)
                     Option.get (VR.result_of_enum (VR.bot ()))
                   else (
@@ -859,7 +859,7 @@ struct
 
                 match InvariantParser.parse_cil inv_parser ~fundec ~loc pre_cabs with
                 | Ok pre_exp ->
-                  let x = ask_local pre_lvar (Queries.EvalInt pre_exp) in
+                  let x = ask_local pre_lvar (Queries.EvalInt pre_exp) in (* TODO: Queries.eval_bool? *)
                   if Queries.ID.is_bot x || Queries.ID.is_bot_ikind x then (* dead code *)
                     true
                   else (