nondet_instruction_infot Class Reference

Holds information about any discovered nondet methods, with extreme type- safety. More...

Public Types
enum class	is_nondett : bool { FALSE , TRUE }
enum class	is_nullablet : bool { FALSE , TRUE }

Public Member Functions
	nondet_instruction_infot ()
	nondet_instruction_infot (is_nullablet is_nullable)
is_nondett	get_instruction_type () const
is_nullablet	get_nullable_type () const

Private Attributes
is_nondett	is_nondet
is_nullablet	is_nullable

Detailed Description

Holds information about any discovered nondet methods, with extreme type- safety.

Definition at line 24 of file replace_java_nondet.cpp.

Member Enumeration Documentation

is_nondett

enum nondet_instruction_infot::is_nondett : bool

strong

Enumerator
FALSE
TRUE

Definition at line 27 of file replace_java_nondet.cpp.

is_nullablet

enum nondet_instruction_infot::is_nullablet : bool

strong

Enumerator
FALSE
TRUE

Definition at line 32 of file replace_java_nondet.cpp.

Constructor & Destructor Documentation

nondet_instruction_infot() [1/2]

nondet_instruction_infot::nondet_instruction_infot ( )

inline

Definition at line 38 of file replace_java_nondet.cpp.

nondet_instruction_infot() [2/2]

nondet_instruction_infot::nondet_instruction_infot ( is_nullablet  is_nullable )

inlineexplicit

Definition at line 43 of file replace_java_nondet.cpp.

Member Function Documentation

get_instruction_type()

is_nondett nondet_instruction_infot::get_instruction_type ( ) const

inline

Definition at line 48 of file replace_java_nondet.cpp.

get_nullable_type()

is_nullablet nondet_instruction_infot::get_nullable_type ( ) const

inline

Definition at line 52 of file replace_java_nondet.cpp.

Member Data Documentation

is_nondet

is_nondett nondet_instruction_infot::is_nondet

private

Definition at line 58 of file replace_java_nondet.cpp.

is_nullable

is_nullablet nondet_instruction_infot::is_nullable

private

Definition at line 59 of file replace_java_nondet.cpp.

---

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

• /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/replace_java_nondet.cpp