Skip to content

Commit

Permalink
Correct & clarify --per_path_timeout documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
@pschanely
pschanely committed Feb 28, 2024
1 parent e4d1e75 commit 86b8d7c
Show file tree
Hide file tree
Showing 4 changed files with 32 additions and 20 deletions.
13 changes: 8 additions & 5 deletions crosshair/main.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -346,6 +346,7 @@ def command_line_parser() -> argparse.ArgumentParser:
"""\
Maximum number of consecutive iterations to run without making
significant progress in exploring the codebase.
(by default, 5 iterations)
This option can be more useful than --per_condition_timeout
because the amount of time invested will scale with the complexity
Expand All @@ -366,11 +367,13 @@ def command_line_parser() -> argparse.ArgumentParser:
help=textwrap.dedent(
"""\
Maximum seconds to spend checking one execution path.
If unspecified, CrossHair will timeout each path:
1. At the square root of `--per_condition_timeout`, if specified.
2. Otherwise, at a number of seconds equal to
`--max_uninteresting_iterations`, if specified.
3. Otherwise, there will be no per-path timeout.
If unspecified:
1. CrossHair will timeout each path at the square root of
`--per_condition_timeout`, if specified.
3. Otherwise, it will timeout each path at a number of seconds equal to
`--max_uninteresting_iterations`, unless it is explicitly set to zero.
(NOTE: `--max_uninteresting_iterations` is 5 by default)
2. Otherwise, it will not use any per-path timeout.
"""
),
)
Expand Down
13 changes: 8 additions & 5 deletions doc/source/contracts.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -176,6 +176,7 @@ It is more customizable than ``watch`` and produces machine-readable output.
--max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS
Maximum number of consecutive iterations to run without making
significant progress in exploring the codebase.
(by default, 5 iterations)
This option can be more useful than --per_condition_timeout
because the amount of time invested will scale with the complexity
Expand All @@ -186,11 +187,13 @@ It is more customizable than ``watch`` and produces machine-readable output.
run CrossHair for hours.
--per_path_timeout FLOAT
Maximum seconds to spend checking one execution path.
If unspecified, CrossHair will timeout each path:
1. At the square root of `--per_condition_timeout`, if specified.
2. Otherwise, at a number of seconds equal to
`--max_uninteresting_iterations`, if specified.
3. Otherwise, there will be no per-path timeout.
If unspecified:
1. CrossHair will timeout each path at the square root of
`--per_condition_timeout`, if specified.
3. Otherwise, it will timeout each path at a number of seconds equal to
`--max_uninteresting_iterations`, unless it is explicitly set to zero.
(NOTE: `--max_uninteresting_iterations` is 5 by default)
2. Otherwise, it will not use any per-path timeout.
--per_condition_timeout FLOAT
Maximum seconds to spend checking execution paths for one condition
--analysis_kind KIND Kind of contract to check.
Expand Down
13 changes: 8 additions & 5 deletions doc/source/cover.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,7 @@ How do I try it?
--max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS
Maximum number of consecutive iterations to run without making
significant progress in exploring the codebase.
(by default, 5 iterations)
This option can be more useful than --per_condition_timeout
because the amount of time invested will scale with the complexity
Expand All @@ -115,11 +116,13 @@ How do I try it?
run CrossHair for hours.
--per_path_timeout FLOAT
Maximum seconds to spend checking one execution path.
If unspecified, CrossHair will timeout each path:
1. At the square root of `--per_condition_timeout`, if specified.
2. Otherwise, at a number of seconds equal to
`--max_uninteresting_iterations`, if specified.
3. Otherwise, there will be no per-path timeout.
If unspecified:
1. CrossHair will timeout each path at the square root of
`--per_condition_timeout`, if specified.
3. Otherwise, it will timeout each path at a number of seconds equal to
`--max_uninteresting_iterations`, unless it is explicitly set to zero.
(NOTE: `--max_uninteresting_iterations` is 5 by default)
2. Otherwise, it will not use any per-path timeout.
--per_condition_timeout FLOAT
Maximum seconds to spend checking execution paths for one condition
Expand Down
13 changes: 8 additions & 5 deletions doc/source/diff_behavior.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,7 @@ How do I try it?
--max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS
Maximum number of consecutive iterations to run without making
significant progress in exploring the codebase.
(by default, 5 iterations)
This option can be more useful than --per_condition_timeout
because the amount of time invested will scale with the complexity
Expand All @@ -76,11 +77,13 @@ How do I try it?
run CrossHair for hours.
--per_path_timeout FLOAT
Maximum seconds to spend checking one execution path.
If unspecified, CrossHair will timeout each path:
1. At the square root of `--per_condition_timeout`, if specified.
2. Otherwise, at a number of seconds equal to
`--max_uninteresting_iterations`, if specified.
3. Otherwise, there will be no per-path timeout.
If unspecified:
1. CrossHair will timeout each path at the square root of
`--per_condition_timeout`, if specified.
3. Otherwise, it will timeout each path at a number of seconds equal to
`--max_uninteresting_iterations`, unless it is explicitly set to zero.
(NOTE: `--max_uninteresting_iterations` is 5 by default)
2. Otherwise, it will not use any per-path timeout.
--per_condition_timeout FLOAT
Maximum seconds to spend checking execution paths for one condition
Expand Down

0 comments on commit 86b8d7c

Please sign in to comment.