CBMC
Public Types | Public Member Functions | Private Attributes | List of all members
nondet_instruction_infot Class Referencefinal

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 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: