diff options
author | Timotej Kapus <tk1713@ic.ac.uk> | 2018-06-07 17:21:54 +0100 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2019-04-04 20:37:41 +0100 |
commit | bed9f8d4b202a1b754e7b91fafdba14beb325272 (patch) | |
tree | 23d1e3b1af6cdd69b3317634ce425d537aea7117 /tools/klee-stats | |
parent | e6857002d7d69d6765b506f17fcb3e979854b995 (diff) | |
download | klee-bed9f8d4b202a1b754e7b91fafdba14beb325272.tar.gz |
Remove precision
Diffstat (limited to 'tools/klee-stats')
-rwxr-xr-x | tools/klee-stats/klee-stats | 21 |
1 files changed, 2 insertions, 19 deletions
diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats index 77b52aa7..5b8dacf4 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -256,18 +256,6 @@ def grafana(dirs): return 0 def main(): - # function for sanitizing arguments - def isPositiveInt(value): - try: - value = int(value) - except ValueError: - raise argparse.ArgumentTypeError( - 'integer expected: {0}'.format(value)) - if value <= 0: - raise argparse.ArgumentTypeError( - 'positive integer expected: {0}'.format(value)) - return value - parser = argparse.ArgumentParser( description='output statistics logged by klee', epilog='LEGEND\n' + tabulate(Legend), @@ -275,11 +263,6 @@ def main(): parser.add_argument('dir', nargs='+', help='klee output directory') - parser.add_argument('--precision', - dest='precision', type=isPositiveInt, - default=2, metavar='n', - help='Floating point numbers display precision ' - '(default: 2).') parser.add_argument('--table-format', choices=['plain', 'simple', 'grid', 'pipe', 'orgtbl', 'rst', 'mediawiki', 'latex', 'klee'], @@ -383,13 +366,13 @@ def main(): print(tabulate( table, headers='firstrow', tablefmt=args.tableFormat, - floatfmt='.{p}f'.format(p=args.precision), + floatfmt='.{p}f'.format(p=2), numalign='right', stralign='center')) else: stream = tabulate( table, headers='firstrow', tablefmt=KleeTable, - floatfmt='.{p}f'.format(p=args.precision), + floatfmt='.{p}f'.format(p=2), numalign='right', stralign='center') # add a line separator before the total line if len(data) > 1: |