diff options
Diffstat (limited to 'tools/klee-stats/klee-stats')
| -rwxr-xr-x | tools/klee-stats/klee-stats | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats index ab28ba0f..544a06d3 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -366,12 +366,13 @@ def main(): pr = 'more' dirs = getKleeOutDirs(args.dir) - if args.grafana: - return grafana(dirs, args.grafana_host, args.grafana_port) if len(dirs) == 0: print('no klee output dir found', file=sys.stderr) exit(1) + if args.grafana: + return grafana(dirs, args.grafana_host, args.grafana_port) + # Filter non-existing files, useful for star operations valid_log_files = [getLogFile(f) for f in dirs if os.path.isfile(getLogFile(f))] |