CBMC: /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Enumerations

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

enum 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 class flow_sensitivityt

strong

Enumerator
sensitive
insensitive

Definition at line 37 of file variable_sensitivity_configuration.h.