main_function_resultt Struct Reference

#include <java_entry_point.h>

Collaboration diagram for main_function_resultt:

Public Types
enum	statust { Success, Error, NotFound }

Public Member Functions
	main_function_resultt (statust status)
	main_function_resultt (const symbolt &main_function)
bool	is_success () const
bool	is_error () const

Public Attributes
enum main_function_resultt::statust	status
symbolt	main_function

Detailed Description

Definition at line 32 of file java_entry_point.h.

Member Enumeration Documentation

statust

enum main_function_resultt::statust

Enumerator
Success
Error
NotFound

Definition at line 34 of file java_entry_point.h.

Constructor & Destructor Documentation

main_function_resultt() [1/2]

main_function_resultt::main_function_resultt ( statust  status )

inline

Definition at line 44 of file java_entry_point.h.

main_function_resultt() [2/2]

main_function_resultt::main_function_resultt ( const symbolt &  main_function )

inline

Definition at line 50 of file java_entry_point.h.

Member Function Documentation

is_error()

bool main_function_resultt::is_error ( ) const

inline

Definition at line 59 of file java_entry_point.h.

References Error, and status.

Referenced by java_bytecode_languaget::generate_support_functions().

is_success()

bool main_function_resultt::is_success ( ) const

inline

Definition at line 55 of file java_entry_point.h.

References status, and Success.

Referenced by ci_lazy_methodst::entry_point_methods(), java_bytecode_languaget::generate_support_functions(), and java_entry_point().

Member Data Documentation

main_function

symbolt main_function_resultt::main_function

Definition at line 40 of file java_entry_point.h.

Referenced by ci_lazy_methodst::entry_point_methods(), java_bytecode_languaget::generate_support_functions(), and java_entry_point().

status

enum main_function_resultt::statust main_function_resultt::status

Referenced by is_error(), and is_success().

---

The documentation for this struct was generated from the following file:

• /builddir/build/BUILD/cbmc-cbmc-5.10/jbmc/src/java_bytecode/java_entry_point.h