Skip to content

Commit

Permalink
Some further obvious cases
Browse files Browse the repository at this point in the history
  • Loading branch information
michael-schwarz committed Feb 18, 2025
1 parent 8eeb996 commit 41730e0
Show file tree
Hide file tree
Showing 7 changed files with 16 additions and 29 deletions.
6 changes: 2 additions & 4 deletions src/cdomain/value/domains/invariantCil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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) =
Expand Down
4 changes: 1 addition & 3 deletions src/cdomain/value/domains/valueDomainQueries.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
13 changes: 6 additions & 7 deletions src/common/framework/cfgTools.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
)
)
Expand Down Expand Up @@ -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

Expand Down
6 changes: 1 addition & 5 deletions src/common/util/richVarinfo.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
7 changes: 3 additions & 4 deletions src/constraint/constrSys.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -294,6 +292,7 @@ struct
f get set
)
in
Some f'
f'
) (S.system x)
end
end
4 changes: 1 addition & 3 deletions src/incremental/compareCIL.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down
5 changes: 2 additions & 3 deletions src/incremental/makefileUtil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 41730e0

Please sign in to comment.