Some further obvious cases

Author: michael-schwarz

src/cdomain/value/domains/invariantCil.ml

@@ -59,10 +59,8 @@ let exclude_vars_regexp = ResettableLazy.from_fun (fun () ->
 (* let var_is_tmp {vdescrpure} = not vdescrpure (* doesn't exclude tmp___0 *) *)
 (* TODO: instead check if vdescr is nonempty? (doesn't cover all cases, e.g. ternary temporary) *)
 let varname_is_tmp vname = Str.string_match (ResettableLazy.force exclude_vars_regexp) vname 0
-let var_is_tmp vi =
-  match Cilfacade.find_original_name vi with
-  | None -> true
-  | Some vname -> varname_is_tmp vname
+let var_is_tmp vi = BatOption.map_default varname_is_tmp true (Cilfacade.find_original_name vi)
+
 class exp_contains_tmp_visitor (acc: bool ref) = object
   inherit nopCilVisitor as super
   method! vvrbl (vi: varinfo) =

src/cdomain/value/domains/valueDomainQueries.ml

@@ -61,9 +61,7 @@ let eval_int_binop (module Bool: Lattice.S with type t = bool) binop (eval_int:
   if ID.is_bot i || ID.is_bot_ikind i then
     Bool.top () (* base returns bot for non-int results, consider unknown *)
   else
-    match ID.to_bool i with
-    | Some b -> b
-    | None -> Bool.top ()
+    BatOption.default (Bool.top ()) (ID.to_bool i)
 
 (** Backwards-compatibility for former [MustBeEqual] query. *)
 let must_be_equal = eval_int_binop (module MustBool) Eq

src/common/framework/cfgTools.ml

@@ -432,9 +432,10 @@ let createCFG (file: file) =
                   List.iter (fun (fromNode, toNode) ->
                       addEdge_fromLoc fromNode (Test (one, false)) toNode;
                       added_connect := true;
-                      match NH.find_option node_scc toNode with
-                      | Some toNode_scc -> iter_scc toNode_scc (* continue to target scc as normally, to ensure they are also connected *)
-                      | None -> () (* pseudo return, wasn't in scc, but is fine *)
+                      Option.iter (fun toNode_scc ->
+                          iter_scc toNode_scc (* continue to target scc as normally, to ensure they are also connected *)
+                        ) (NH.find_option node_scc toNode)
+                      (* otherwise pseudo return, wasn't in scc, but is fine *)
                     ) targets
                 )
               )
@@ -556,12 +557,10 @@ struct
     Format.fprintf out ("\t%a [%s];\n") p_node n styles;
     match n with
     | Statement s when get_bool "dbg.cfg.loop-unrolling" ->
-      begin match LoopUnrolling0.find_copyof s with
-        | Some s' ->
+      Option.iter (fun s' ->
           let n' = Statement s' in
           Format.fprintf out "\t%a -> %a [style=dotted];\n" p_node n p_node n'
-        | None -> ()
-      end
+        ) (LoopUnrolling0.find_copyof s)
     | _ -> ()
 end
 

src/common/util/richVarinfo.ml

@@ -57,11 +57,7 @@ struct
 
   let marshal () = !xh
 
-  let unmarshal = function
-    | Some xh_loaded ->
-      xh := xh_loaded
-    | None -> ()
-
+  let unmarshal = Option.iter ((:=) xh)
   let bindings () = List.of_seq (XH.to_seq !xh)
 end
 

src/constraint/constrSys.ml

@@ -282,9 +282,7 @@ struct
     include S
 
     let system x =
-      match S.system x with
-      | None -> None
-      | Some f ->
+      Option.map (fun f ->
         let f' get set =
           let old_current_var = !current_var in
           current_var := Some x;
@@ -294,6 +292,7 @@ struct
               f get set
             )
         in
-        Some f'
+        f'
+        ) (S.system x)
   end
 end

src/incremental/compareCIL.ml

@@ -101,9 +101,7 @@ let addToFinalMatchesMapping oV nV final_matches =
 let empty_rename_assms m = VarinfoMap.for_all (fun vo vn -> vo.vname = vn.vname) m
 
 let already_matched oV nV final_matches =
-  match VarinfoMap.find_opt oV (fst final_matches) with
-  | None -> false
-  | Some v -> v.vid = oV.vid
+  GobOption.exists (fun v -> v.vid = nV.vid) (VarinfoMap.find_opt oV (fst final_matches))
 
 (* looks up the result of the already executed comparison and returns true if it is unchanged, false if it is changed.
    Throws an exception if not found. *)

src/incremental/makefileUtil.ml

@@ -9,12 +9,11 @@ let comb_suffix = "_comb.c"
 
 let exec_command ?path (command: string) =
   let current_dir = Sys.getcwd () in
-  (match path with
-   | Some path ->
+  GobOption.iter (fun path ->
      let path_str = Fpath.to_string path in
      if Sys.file_exists path_str && Sys.is_directory path_str then Sys.chdir path_str
      else failwith ("Directory " ^ path_str ^ " does not exist!")
-   | None -> ());
+    ) path;
   Logs.debug "%s" ("executing command `" ^ command ^ "` in " ^ Sys.getcwd ());
   let (std_out, std_in) = open_process command in
   let output = Buffer.create buff_size in