diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/klee-stats/klee-stats | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats index 6fc803b2..1a32432d 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -165,7 +165,7 @@ def getRow(record, stats, pr): return row -def grafana(dirs): +def grafana(dirs, host_address, port): dr = getLogFile(dirs[0]) from flask import Flask, jsonify, request import datetime @@ -238,7 +238,7 @@ def grafana(dirs): ret = jsonify(result) return ret - app.run() + app.run(host=host_address, port=port) return 0 def main(): @@ -259,6 +259,12 @@ def main(): parser.add_argument('--grafana', action='store_true', dest='grafana', help='Start a grafana web server') + parser.add_argument('--grafana-host', dest='grafana_host', + help='IP address grafana web server should listen to', + default="127.0.0.1") + parser.add_argument('--grafana-port', dest='grafana_port', type=int, + help='Port grafana web server should listen to', + default=5000) # argument group for controlling output verboseness pControl = parser.add_mutually_exclusive_group(required=False) @@ -295,7 +301,7 @@ def main(): dirs = getKleeOutDirs(args.dir) if args.grafana: - return grafana(dirs) + return grafana(dirs, args.grafana_host, args.grafana_port) if len(dirs) == 0: print('no klee output dir found', file=sys.stderr) exit(1) |