CBMC
Public Member Functions | Private Member Functions | Static Private Member Functions | Private Attributes | List of all members
instrument_spec_assignst::location_intervalt Class Reference

Represents an interval of source locations covered by the static local variable search. More...

#include <instrument_spec_assigns.h>

Public Member Functions

 location_intervalt ()
 Initializes to the empty interval. More...
 
void anywhere ()
 Grows the interval cover the maximum range [(size_t::min, size_t::min), (size_t::min, size_t::max)]. More...
 
void update (const source_locationt &source_location)
 Grows the interval to include the given (line, col) location. More...
 
bool contains (const source_locationt &source_location)
 True iff the interval contains the given location. More...
 

Private Member Functions

std::size_t col_to_size_t (const source_locationt &source_location, std::size_t default_value)
 If line or col is missing use default. More...
 
std::size_t line_to_size_t (const source_locationt &source_location, std::size_t default_value)
 If line is missing use default. More...
 
void update_min (size_t line, size_t col)
 Updates the min_line and min_col in place using the given values iff they are smaller. More...
 
void update_max (size_t line, size_t col)
 Updates the max_line and max_col in place using the given values iff they are larger. More...
 

Static Private Member Functions

static bool is_lte (size_t line0, size_t col0, size_t line1, size_t col1)
 True iff (line0, col0) <= (line1, col1) in lexicographic ordering. More...
 

Private Attributes

std::size_t min_line
 
std::size_t min_col
 
std::size_t max_line
 
std::size_t max_col
 

Detailed Description

Represents an interval of source locations covered by the static local variable search.

Interval bounds are represented with (line, col) positive integers. Lexicographic ordering is used for comparisons. Updates to the bounds and inclusion checks use pessimistic defaults when source locations are undefined or only partially defined.

Definition at line 261 of file instrument_spec_assigns.h.

Constructor & Destructor Documentation

◆ location_intervalt()

instrument_spec_assignst::location_intervalt::location_intervalt ( )
inline

Initializes to the empty interval.

Definition at line 265 of file instrument_spec_assigns.h.

Member Function Documentation

◆ anywhere()

void instrument_spec_assignst::location_intervalt::anywhere ( )
inline

Grows the interval cover the maximum range [(size_t::min, size_t::min), (size_t::min, size_t::max)].

Definition at line 275 of file instrument_spec_assigns.h.

◆ col_to_size_t()

std::size_t instrument_spec_assignst::location_intervalt::col_to_size_t ( const source_locationt &  source_location,
std::size_t  default_value 
)
inlineprivate

If line or col is missing use default.

Definition at line 333 of file instrument_spec_assigns.h.

◆ contains()

bool instrument_spec_assignst::location_intervalt::contains ( const source_locationt &  source_location)
inline

True iff the interval contains the given location.

Definition at line 303 of file instrument_spec_assigns.h.

◆ is_lte()

static bool instrument_spec_assignst::location_intervalt::is_lte ( size_t  line0,
size_t  col0,
size_t  line1,
size_t  col1 
)
inlinestaticprivate

True iff (line0, col0) <= (line1, col1) in lexicographic ordering.

Definition at line 371 of file instrument_spec_assigns.h.

◆ line_to_size_t()

std::size_t instrument_spec_assignst::location_intervalt::line_to_size_t ( const source_locationt &  source_location,
std::size_t  default_value 
)
inlineprivate

If line is missing use default.

Definition at line 353 of file instrument_spec_assigns.h.

◆ update()

void instrument_spec_assignst::location_intervalt::update ( const source_locationt &  source_location)
inline

Grows the interval to include the given (line, col) location.

Definition at line 284 of file instrument_spec_assigns.h.

◆ update_max()

void instrument_spec_assignst::location_intervalt::update_max ( size_t  line,
size_t  col 
)
inlineprivate

Updates the max_line and max_col in place using the given values iff they are larger.

Definition at line 389 of file instrument_spec_assigns.h.

◆ update_min()

void instrument_spec_assignst::location_intervalt::update_min ( size_t  line,
size_t  col 
)
inlineprivate

Updates the min_line and min_col in place using the given values iff they are smaller.

Definition at line 378 of file instrument_spec_assigns.h.

Member Data Documentation

◆ max_col

std::size_t instrument_spec_assignst::location_intervalt::max_col
private

Definition at line 401 of file instrument_spec_assigns.h.

◆ max_line

std::size_t instrument_spec_assignst::location_intervalt::max_line
private

Definition at line 400 of file instrument_spec_assigns.h.

◆ min_col

std::size_t instrument_spec_assignst::location_intervalt::min_col
private

Definition at line 399 of file instrument_spec_assigns.h.

◆ min_line

std::size_t instrument_spec_assignst::location_intervalt::min_line
private

Definition at line 398 of file instrument_spec_assigns.h.

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