diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml index db17a42a4..727e3ac71 100644 --- a/sledge/cli/sledge_cli.ml +++ b/sledge/cli/sledge_cli.ml @@ -97,7 +97,9 @@ let analyze = let%map_open bound = flag "bound" (optional_with_default 1 int) - ~doc:" stop execution exploration at depth " + ~doc: + " stop execution exploration at depth , a negative bound \ + is never hit and leads to unbounded exploration" and function_summaries = flag "function-summaries" no_arg ~doc:"use function summaries (in development)" diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 572265648..9823090bb 100644 --- a/sledge/sledge-help.txt +++ b/sledge/sledge-help.txt @@ -107,7 +107,8 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo === flags === [-append-report] append to report file - [-bound ] stop execution exploration at depth + [-bound ] stop execution exploration at depth , a negative + bound is never hit and leads to unbounded exploration [-colors] enable printing in colors [-domain ] select abstract domain; must be one of "sh" (default, symbolic heap domain), "globals" (used-globals domain), @@ -186,7 +187,8 @@ The file must be binary LLAIR, such as produced by `sledge translate`. === flags === [-append-report] append to report file - [-bound ] stop execution exploration at depth + [-bound ] stop execution exploration at depth , a negative + bound is never hit and leads to unbounded exploration [-colors] enable printing in colors [-domain ] select abstract domain; must be one of "sh" (default, symbolic heap domain), "globals" (used-globals domain), diff --git a/sledge/src/control.ml b/sledge/src/control.ml index c13933b85..0963f8872 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -288,8 +288,9 @@ module Make (Config : Config) (D : Domain) (Queue : Queue) = struct let edge = {Edge.dst= curr; src= prev; stk} in let depth = Option.value (Depths.find edge depths) ~default:0 in let depth = if retreating then depth + 1 else depth in - if depth <= Config.bound then enqueue depth edge state depths queue - else prune depth edge queue + if 0 <= Config.bound && Config.bound < depth then + prune depth edge queue + else enqueue depth edge state depths queue let init state curr = add ~retreating:false Stack.empty state curr Depths.empty