| method | MediaInfoOutput getOutput(String, String) |
| presumption | java.lang.Runtime:exec(...)@77 != null |
| presumption | java.lang.Runtime:getRuntime(...)@77 != null |
| post | java.lang.StringBuffer:toString(...)._tainted == 0 |
| post | return_value in Addr_Set{&new MediaInfoOutput(g etOutput#6),&new MediaInfoOutput(getOutput#7)} |
| post | new MediaInfoOutput(getOutput#6) num objects <= 1 |
| post | init'ed(new MediaInfoOutput(getOutput#6).exitCode) |
| post | new MediaInfoOutput(getOutput#6).output == &java.lang.StringBuffer:toString(...) |
| post | new MediaInfoOutput(getOutput#7) num objects <= 1 |
| post | new MediaInfoOutput(getOutput#7).exitCode == -1 |
| post | new MediaInfoOutput(getOutput#7).output == &"Error executing GetMediaInfo.exe" |
| method | void extractFiles(ResourceManager, File, String) |
| pre | res != null |
| presumption | init'ed(com.dmdirc.logger.ErrorLevel.LOW) |
| presumption | com.dmdirc.util.resourcemanager.ResourceManager:get ResourceManager(...)@111 != null |
| presumption | com.dmdirc.util.resourcemanager.ResourceManager:get ResourcesEndingWithAsBytes(...)@101 != null |
| presumption | java.util.Iterator:next(...)@102 != null |
| presumption | java.util.Map:entrySet(...)@102 != null |
| presumption | java.util.Map_Entry:getKey(...)@104 != null |
| test_vector | java.io.File:exists(...)@110: {0}, {1} |
| test_vector | java.io.File:isDirectory(...)@109: {1}, {0} |
| test_vector | java.util.Iterator:hasNext(...)@102: {0}, {1} |
| method | void onLoad() |
| presumption | init'ed(com.dmdirc.logger.ErrorLevel.LOW) |
| presumption | com.dmdirc.plugins.PluginInfo:getResourceManager(.. .)@130 != null |
| presumption | com.dmdirc.plugins.PluginManager:getPluginManager(. ..)@123 != null |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on com.dmdirc.util.resourcemanager. ResourceManager:getResourcesEndingWithAsBytes |
| unanalyzed | call on java.util.Map:entrySet |
| unanalyzed | call on java.util.Set:iterator |
| unanalyzed | call on java.util.Map$Entry:getKey |
| unanalyzed | call on java.lang.String:lastIndexOf |
| unanalyzed | call on java.lang.String:length |
| unanalyzed | call on java.lang.String:substring |
| unanalyzed | call on java.io.File |
| unanalyzed | call on java.io.File:isDirectory |
| unanalyzed | call on java.io.File:exists |
| unanalyzed | call on java.io.File:delete |
| unanalyzed | call on com.dmdirc.util.resourcemanager. ResourceManager:getResourceManager |
| unanalyzed | call on java.util.Map$Entry:getValue |
| unanalyzed | call on com.dmdirc.util.resourcemanager. ResourceManager:resourceToFile |
| unanalyzed | call on java.io.IOException:getMessage |
| unanalyzed | call on com.dmdirc.logger.Logger:userError |
| test_vector | com.dmdirc.plugins.PluginManager:getPluginInfoByNam e(...)@123: Inverse{null}, Addr_Set{null} |
| test_vector | java.io.File:exists(...)@134: {1}, {0} |