diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/valgrind_check_success | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/tools/valgrind_check_success b/tools/valgrind_check_success new file mode 100644 index 0000000..24830d5 --- /dev/null +++ b/tools/valgrind_check_success @@ -0,0 +1,30 @@ +#! /usr/bin/env tclsh + + +proc main {sourcetype source} { + switch $sourcetype { + file { + set chan [open $source] + try { + set data [read $chan] + } finally { + close $chan + } + } + string { + set data $source + } + default { + error [list {wrong # args}] + } + } + set found [regexp -inline -all {blocks are\ + (?:(?:(?:definitely|indirectly|possibly) lost)|still reachable)} $data] + if {[llength $found]} { + puts 0 + } else { + puts 1 + } + flush stdout +} +main {*}$argv |