CBMC
java-testing-utils Directory Reference
+ Directory dependency graph for java-testing-utils:

Files

file  load_java_class.cpp [code]
 
file  load_java_class.h [code]
 Utility for loading and parsing a specified java class file, returning the symbol table generated by this.
 
file  require_goto_statements.cpp [code]
 
file  require_goto_statements.h [code]
 Utilties for inspecting goto functions.
 
file  require_parse_tree.cpp [code]
 
file  require_parse_tree.h [code]
 Utilties for inspecting java_parse_treet.
 
file  require_type.cpp [code]
 
file  require_type.h [code]
 Helper functions for requiring specific types If the type is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression.