CBMC
variable_sensitivity_configuration.h File Reference

Captures the user-supplied configuration for VSD, determining which domain abstractions are used, flow sensitivity, etc. More...

#include <map>
#include <string>
+ Include dependency graph for variable_sensitivity_configuration.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  vsd_configt
 

Enumerations

enum  ABSTRACT_OBJECT_TYPET {
  TWO_VALUE , CONSTANT , INTERVAL , ARRAY_SENSITIVE ,
  ARRAY_INSENSITIVE , VALUE_SET_OF_POINTERS , POINTER_SENSITIVE , POINTER_INSENSITIVE ,
  STRUCT_SENSITIVE , STRUCT_INSENSITIVE , UNION_INSENSITIVE , VALUE_SET ,
  HEAP_ALLOCATION
}
 
enum class  flow_sensitivityt { sensitive , insensitive }
 

Detailed Description

Captures the user-supplied configuration for VSD, determining which domain abstractions are used, flow sensitivity, etc.

Definition in file variable_sensitivity_configuration.h.

Enumeration Type Documentation

◆ ABSTRACT_OBJECT_TYPET

Enumerator
TWO_VALUE 
CONSTANT 
INTERVAL 
ARRAY_SENSITIVE 
ARRAY_INSENSITIVE 
VALUE_SET_OF_POINTERS 
POINTER_SENSITIVE 
POINTER_INSENSITIVE 
STRUCT_SENSITIVE 
STRUCT_INSENSITIVE 
UNION_INSENSITIVE 
VALUE_SET 
HEAP_ALLOCATION 

Definition at line 19 of file variable_sensitivity_configuration.h.

◆ flow_sensitivityt

enum flow_sensitivityt
strong
Enumerator
sensitive 
insensitive 

Definition at line 37 of file variable_sensitivity_configuration.h.