Move _Bool cast strip from assert to LibraryFunctions

src/analyses/assert.ml

@@ -23,13 +23,7 @@ struct
         | Some b -> `Lifted b
         | None -> `Top
     in
-    let expr =
-      match e with
-      | CastE (TInt (IBool, _), expr) -> expr
-      | Const (CInt (b, IBool, s)) -> Const (CInt (b, IInt, s))
-      | expr -> expr
-    in
-    let expr = CilType.Exp.show expr in
+    let expr = CilType.Exp.show e in
     let warn warn_fn ?annot msg = if check then
         if get_bool "dbg.regression" then ( (* This only prints unexpected results (with the difference) as indicated by the comment behind the assert (same as used by the regression test script). *)
           let loc = !M.current_loc in

src/analyses/baseInvariant.ml

@@ -855,12 +855,6 @@ struct
         inv_exp (Float ftv) exp st
 
   let invariant man st exp tv =
-    (* TODO: this cast should be supported generally somewhere above *)
-    let exp =
-      match exp with
-      | CastE (TInt (IBool, _), exp) -> exp
-      | exp -> exp
-    in
     (* The computations that happen here are not computations that happen in the programs *)
     (* Any overflow during the forward evaluation will already have been flagged here *)
     GobRef.wrap AnalysisState.executing_speculative_computations true

src/cdomain/value/util/wideningThresholds.ml

@@ -119,9 +119,6 @@ class extractInvariantsVisitor (exps) = object
       Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () ->
       let desc = LibraryFunctions.find f in
       begin match desc.special args with
-        | Assert { exp = CastE (TInt (IBool, _), exp); _ } -> (* TODO: this probably shouldn't be here *)
-          EH.replace exps exp ();
-          DoChildren
         | Assert { exp; _ } ->
           EH.replace exps exp ();
           DoChildren

src/cdomains/apron/sharedFunctions.apron.ml

@@ -511,12 +511,6 @@ struct
 
   (** Assert any expression. *)
   let assert_inv ask d e negate no_ov =
-    (* TODO: this cast should be supported generally somewhere above? *)
-    let e =
-      match e with
-      | CastE (TInt (IBool, _), e) -> e
-      | e -> e
-    in
     let e' =
       if exp_is_constraint e then
         e

src/util/library/libraryFunctions.ml

@@ -16,6 +16,11 @@ let intmax_t = lazy (
   !res
 )
 
+let stripOuterBoolCast = function
+  | CastE (TInt (IBool, _), e) -> e
+  | Const (CInt (b, IBool, s)) -> Const (CInt (b, IInt, s))
+  | e -> e
+
 (** C standard library functions.
     These are specified by the C standard. *)
 let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -830,9 +835,9 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
 (** Goblint functions. *)
 let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__goblint_unknown", unknown [drop' [w]]);
-    ("__goblint_check", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = false });
-    ("__goblint_assume", special [__ "exp" []] @@ fun exp -> Assert { exp; check = false; refine = true });
-    ("__goblint_assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" });
+    ("__goblint_check", special [__ "exp" []] @@ fun exp -> Assert { exp = stripOuterBoolCast exp; check = true; refine = false });
+    ("__goblint_assume", special [__ "exp" []] @@ fun exp -> Assert { exp = stripOuterBoolCast exp; check = false; refine = true });
+    ("__goblint_assert", special [__ "exp" []] @@ fun exp -> Assert { exp = stripOuterBoolCast exp; check = true; refine = get_bool "sem.assert.refine" });
     ("__goblint_globalize", special [__ "ptr" []] @@ fun ptr -> Globalize ptr);
     ("__goblint_split_begin", unknown [drop "exp" []]);
     ("__goblint_split_end", unknown [drop "exp" []]);