CBMC
Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Private Attributes | List of all members
variable_sensitivity_domaint Class Reference

#include <variable_sensitivity_domain.h>

+ Inheritance diagram for variable_sensitivity_domaint:
[フレーム]
[legend]
+ Collaboration diagram for variable_sensitivity_domaint:
[フレーム]
[legend]

Public Member Functions

  variable_sensitivity_domaint (variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
 
void  transform (const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) override
  Compute the abstract transformer for a single instruction.
 
void  make_bottom () override
  Sets the domain to bottom (no states / unreachable).
 
void  make_top () override
  Sets the domain to top (all states).
 
void  output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
  Basic text output of the abstract domain.
 
exprt  to_predicate () const override
  Gives a Boolean condition that is true for all values represented by the domain.
 
exprt  to_predicate (const exprt &expr, const namespacet &ns) const
 
exprt  to_predicate (const exprt::operandst &exprs, const namespacet &ns) const
 
virtual bool  merge (const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to)
  Computes the join between "this" and "b".
 
virtual void  merge_three_way_function_return (const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
  Merges just the things that have changes between "function_start" and "function_end" into "this".
 
bool  ai_simplify (exprt &condition, const namespacet &ns) const override
  Use the information in the domain to simplify the expression with respect to the current location.
 
bool  is_bottom () const override
  Find out if the domain is currently unreachable.
 
bool  is_top () const override
  Is the domain completely top at this state.
 
virtual abstract_object_pointert  eval (const exprt &expr, const namespacet &ns) const
 
- Public Member Functions inherited from ai_domain_baset
virtual  ~ai_domain_baset ()
 
virtual jsont  output_json (const ai_baset &ai, const namespacet &ns) const
 
virtual xmlt  output_xml (const ai_baset &ai, const namespacet &ns) const
 
virtual void  make_entry ()
  Make this domain a reasonable entry-point state For most domains top is sufficient.
 
virtual bool  ai_simplify_lhs (exprt &condition, const namespacet &ns) const
  Simplifies the expression but keeps it as an l-value.
 

Private Member Functions

void  transform_function_call (locationt from, locationt to, ai_baset &ai, const namespacet &ns)
  Used by variable_sensitivity_domaint::transform to handle FUNCTION_CALL transforms.
 
bool  ignore_function_call_transform (const irep_idt &function_id) const
  Used to specify which CPROVER internal functions should be skipped over when doing function call transforms.
 
void  assume (exprt expr, namespacet ns)
 

Private Attributes

abstract_environmentt  abstract_state
 
flow_sensitivityt  flow_sensitivity
 

Additional Inherited Members

- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett  locationt
 
typedef ai_history_baset::trace_ptrt  trace_ptrt
 
- Protected Member Functions inherited from ai_domain_baset
  ai_domain_baset ()
  The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface.
 
  ai_domain_baset (const ai_domain_baset &old)
  A copy constructor is part of the domain interface.
 

Detailed Description

Definition at line 115 of file variable_sensitivity_domain.h.

Constructor & Destructor Documentation

◆  variable_sensitivity_domaint()

variable_sensitivity_domaint::variable_sensitivity_domaint ( variable_sensitivity_object_factory_ptrt  _object_factory,
const vsd_configt &  _configuration 
)
inlineexplicit

Definition at line 118 of file variable_sensitivity_domain.h.

Member Function Documentation

◆  ai_simplify()

bool variable_sensitivity_domaint::ai_simplify ( exprt &  condition,
const namespacet &  ns 
) const
overridevirtual

Use the information in the domain to simplify the expression with respect to the current location.

This may be able to reduce some values to constants.

Parameters
condition the expression to simplify
ns the namespace
Returns
True if no simplification was made

Reimplemented from ai_domain_baset.

Definition at line 241 of file variable_sensitivity_domain.cpp.

◆  assume()

void variable_sensitivity_domaint::assume ( exprt  expr,
namespacet  ns 
)
private

Definition at line 452 of file variable_sensitivity_domain.cpp.

◆  eval()

virtual abstract_object_pointert variable_sensitivity_domaint::eval ( const exprt &  expr,
const namespacet &  ns 
) const
inlinevirtual

Definition at line 211 of file variable_sensitivity_domain.h.

◆  ignore_function_call_transform()

bool variable_sensitivity_domaint::ignore_function_call_transform ( const irep_idt &  function_id ) const
private

Used to specify which CPROVER internal functions should be skipped over when doing function call transforms.

Parameters
function_id the name of the function being called
Returns
Returns true if the function should be ignored

Definition at line 403 of file variable_sensitivity_domain.cpp.

◆  is_bottom()

bool variable_sensitivity_domaint::is_bottom ( ) const
overridevirtual

Find out if the domain is currently unreachable.

Returns
True if the domain is bottom (i.e. unreachable).

Implements ai_domain_baset.

Definition at line 268 of file variable_sensitivity_domain.cpp.

◆  is_top()

bool variable_sensitivity_domaint::is_top ( ) const
overridevirtual

Is the domain completely top at this state.

Returns
True if the domain is top

Implements ai_domain_baset.

Definition at line 273 of file variable_sensitivity_domain.cpp.

◆  make_bottom()

void variable_sensitivity_domaint::make_bottom ( )
overridevirtual

Sets the domain to bottom (no states / unreachable).

Implements ai_domain_baset.

Definition at line 210 of file variable_sensitivity_domain.cpp.

◆  make_top()

void variable_sensitivity_domaint::make_top ( )
overridevirtual

Sets the domain to top (all states).

Implements ai_domain_baset.

Definition at line 216 of file variable_sensitivity_domain.cpp.

◆  merge()

bool variable_sensitivity_domaint::merge ( const variable_sensitivity_domaint &  b,
trace_ptrt  from,
trace_ptrt  to 
)
virtual

Computes the join between "this" and "b".

Parameters
b the other domain
from it's preceding location
to it's current location
Returns
true if something has changed.

Reimplemented in variable_sensitivity_dependence_domaint.

Definition at line 221 of file variable_sensitivity_domain.cpp.

◆  merge_three_way_function_return()

void variable_sensitivity_domaint::merge_three_way_function_return ( const ai_domain_baset &  function_start,
const ai_domain_baset &  function_end,
const namespacet &  ns 
)
virtual

Merges just the things that have changes between "function_start" and "function_end" into "this".

To be used correctly "this" must be derived from the function call site. Anything that is not modified in the function (such as globals) will not be changed.

Parameters
function_start The base of the diff - changes that have been made between here and the end will be retained.
function_end The end of the merge - changes that have been made between the start and here will be retained.
ns The global namespace

Reimplemented in variable_sensitivity_dependence_domaint.

Definition at line 419 of file variable_sensitivity_domain.cpp.

◆  output()

void variable_sensitivity_domaint::output ( std::ostream &  out,
const ai_baset &  ai,
const namespacet &  ns 
) const
overridevirtual

Basic text output of the abstract domain.

Parameters
out the output stream
ai the abstract interpreter
ns the namespace

Reimplemented from ai_domain_baset.

Definition at line 171 of file variable_sensitivity_domain.cpp.

◆  to_predicate() [1/3]

exprt variable_sensitivity_domaint::to_predicate ( void  ) const
overridevirtual

Gives a Boolean condition that is true for all values represented by the domain.

This allows domains to be converted into program invariants.

Returns
exprt describing the domain

Reimplemented from ai_domain_baset.

Definition at line 179 of file variable_sensitivity_domain.cpp.

◆  to_predicate() [2/3]

exprt variable_sensitivity_domaint::to_predicate ( const exprt &  expr,
const namespacet &  ns 
) const

Definition at line 184 of file variable_sensitivity_domain.cpp.

◆  to_predicate() [3/3]

exprt variable_sensitivity_domaint::to_predicate ( const exprt::operandst &  exprs,
const namespacet &  ns 
) const

Definition at line 192 of file variable_sensitivity_domain.cpp.

◆  transform()

void variable_sensitivity_domaint::transform ( const irep_idt &  function_from,
trace_ptrt  trace_from,
const irep_idt &  function_to,
trace_ptrt  trace_to,
ai_baset &  ai,
const namespacet &  ns 
)
overridevirtual

Compute the abstract transformer for a single instruction.

Parameters
function_from the name of the function containing from
trace_from the instruction before the abstract domain
function_to the name of the function containing to
trace_to the instruction after the abstract domain
ai the abstract interpreter
ns the namespace

Implements ai_domain_baset.

Definition at line 24 of file variable_sensitivity_domain.cpp.

◆  transform_function_call()

void variable_sensitivity_domaint::transform_function_call ( locationt  from,
locationt  to,
ai_baset &  ai,
const namespacet &  ns 
)
private

Used by variable_sensitivity_domaint::transform to handle FUNCTION_CALL transforms.

This is copying the values of the arguments into new symbols corresponding to the declared parameter names.

If the function call is opaque we currently top the return value and the value of any things whose address is passed into the function.

Parameters
from the location to transform from which is a function call
to the destination of the transform (potentially inside the function call)
ai the abstract interpreter
ns the namespace of the current state

Definition at line 278 of file variable_sensitivity_domain.cpp.

Member Data Documentation

◆  abstract_state

abstract_environmentt variable_sensitivity_domaint::abstract_state
private

Definition at line 245 of file variable_sensitivity_domain.h.

◆  flow_sensitivity

flow_sensitivityt variable_sensitivity_domaint::flow_sensitivity
private

Definition at line 246 of file variable_sensitivity_domain.h.

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

AltStyle によって変換されたページ (->オリジナル) /