nondet_instruction_infot Class Reference

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

Public Types
enum	is_nondett : bool { is_nondett::FALSE, is_nondett::TRUE }
enum	is_nullablet : bool { is_nullablet::FALSE, is_nullablet::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 23 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 26 of file replace_java_nondet.cpp.

is_nullablet

enum nondet_instruction_infot::is_nullablet : bool

strong

Enumerator
FALSE
TRUE

Definition at line 31 of file replace_java_nondet.cpp.

Constructor & Destructor Documentation

nondet_instruction_infot() [1/2]

nondet_instruction_infot::nondet_instruction_infot ( )

inline

Definition at line 37 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 42 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 47 of file replace_java_nondet.cpp.

get_nullable_type()

is_nullablet nondet_instruction_infot::get_nullable_type ( ) const

inline

Definition at line 51 of file replace_java_nondet.cpp.

Member Data Documentation

is_nondet

is_nondett nondet_instruction_infot::is_nondet

private

Definition at line 57 of file replace_java_nondet.cpp.

is_nullable

is_nullablet nondet_instruction_infot::is_nullable

private

Definition at line 58 of file replace_java_nondet.cpp.

---

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

• /builddir/build/BUILD/cbmc-cbmc-5.11/jbmc/src/java_bytecode/replace_java_nondet.cpp