cprover
interval_domaint Class Reference

#include <interval_domain.h>

+ Inheritance diagram for interval_domaint:
+ Collaboration diagram for interval_domaint:

Public Member Functions

 interval_domaint ()
 
void transform (const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
 how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More...
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
 
bool merge (const interval_domaint &b, locationt, locationt)
 
void make_bottom () final override
 no states More...
 
void make_top () final override
 all states – the analysis doesn't use this, and domains may refuse to implement it. More...
 
void make_entry () final override
 a reasonable entry-point state More...
 
bool is_bottom () const override final
 
bool is_top () const override final
 
exprt make_expression (const symbol_exprt &) const
 
void assume (const exprt &, const namespacet &)
 
virtual bool ai_simplify (exprt &condition, const namespacet &ns) const override
 Uses the abstract state to simplify a given expression using context- specific information. More...
 
- 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 bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const
 Simplifies the expression but keeps it as an l-value. More...
 
virtual exprt to_predicate (void) const
 Gives a Boolean condition that is true for all values represented by the domain. More...
 

Static Public Member Functions

static bool is_int (const typet &src)
 
static bool is_float (const typet &src)
 

Protected Types

typedef std::map< irep_idt, integer_intervaltint_mapt
 
typedef std::map< irep_idt, ieee_float_intervaltfloat_mapt
 

Protected Member Functions

bool join (const interval_domaint &b)
 Sets *this to the mathematical join between the two domains. More...
 
void havoc_rec (const exprt &)
 
void assume_rec (const exprt &, bool negation=false)
 
void assume_rec (const exprt &lhs, irep_idt id, const exprt &rhs)
 
void assign (const class code_assignt &assignment)
 
integer_intervalt get_int_rec (const exprt &)
 
ieee_float_intervalt get_float_rec (const exprt &)
 
- Protected Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 The constructor is expected to produce 'false' or 'bottom'. More...
 

Protected Attributes

bool bottom
 
int_mapt int_map
 
float_mapt float_map
 

Additional Inherited Members

- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 

Detailed Description

Definition at line 24 of file interval_domain.h.

Member Typedef Documentation

◆ float_mapt

Definition at line 119 of file interval_domain.h.

◆ int_mapt

Definition at line 118 of file interval_domain.h.

Constructor & Destructor Documentation

◆ interval_domaint()

interval_domaint::interval_domaint ( )
inline

Definition at line 31 of file interval_domain.h.

Member Function Documentation

◆ ai_simplify()

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

Uses the abstract state to simplify a given expression using context- specific information.

parameters: The expression to simplify.
Returns
A simplified version of the expression.

Reimplemented from ai_domain_baset.

Definition at line 460 of file interval_domain.cpp.

◆ assign()

void interval_domaint::assign ( const class code_assignt assignment)
protected

Definition at line 187 of file interval_domain.cpp.

◆ assume()

void interval_domaint::assume ( const exprt cond,
const namespacet ns 
)

Definition at line 327 of file interval_domain.cpp.

◆ assume_rec() [1/2]

void interval_domaint::assume_rec ( const exprt cond,
bool  negation = false 
)
protected

Definition at line 334 of file interval_domain.cpp.

◆ assume_rec() [2/2]

void interval_domaint::assume_rec ( const exprt lhs,
irep_idt  id,
const exprt rhs 
)
protected

Definition at line 215 of file interval_domain.cpp.

◆ get_float_rec()

ieee_float_intervalt interval_domaint::get_float_rec ( const exprt )
protected

◆ get_int_rec()

integer_intervalt interval_domaint::get_int_rec ( const exprt )
protected

◆ havoc_rec()

void interval_domaint::havoc_rec ( const exprt lhs)
protected

Definition at line 193 of file interval_domain.cpp.

◆ is_bottom()

bool interval_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 81 of file interval_domain.h.

◆ is_float()

static bool interval_domaint::is_float ( const typet src)
inlinestatic

Definition at line 106 of file interval_domain.h.

◆ is_int()

static bool interval_domaint::is_int ( const typet src)
inlinestatic

Definition at line 101 of file interval_domain.h.

◆ is_top()

bool interval_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 92 of file interval_domain.h.

◆ join()

bool interval_domaint::join ( const interval_domaint b)
protected

Sets *this to the mathematical join between the two domains.

This can be thought of as an abstract version of union; *this is increased so that it contains all of the values that are represented by b as well as its original intervals. The result is an overapproximation, for example: "[0,1]".join("[3,4]") –> "[0,4]" includes 2 which isn't in [0,1] or [3,4].

     Join is used in several places, the most significant being
     merge, which uses it to bring together two different paths
     of analysis.
parameters: The interval domain, b, to join to this domain.
Returns
True if the join increases the set represented by *this, False if there is no change.

Definition at line 129 of file interval_domain.cpp.

◆ make_bottom()

void interval_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 61 of file interval_domain.h.

◆ make_entry()

void interval_domaint::make_entry ( )
inlinefinaloverridevirtual

a reasonable entry-point state

Implements ai_domain_baset.

Definition at line 76 of file interval_domain.h.

◆ make_expression()

exprt interval_domaint::make_expression ( const symbol_exprt src) const

Definition at line 380 of file interval_domain.cpp.

◆ make_top()

void interval_domaint::make_top ( )
inlinefinaloverridevirtual

all states – the analysis doesn't use this, and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 69 of file interval_domain.h.

◆ merge()

bool interval_domaint::merge ( const interval_domaint b,
locationt  ,
locationt   
)
inline

Definition at line 52 of file interval_domain.h.

◆ output()

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

Reimplemented from ai_domain_baset.

Definition at line 23 of file interval_domain.cpp.

◆ transform()

void interval_domaint::transform ( const irep_idt function_from,
locationt  from,
const irep_idt function_to,
locationt  to,
ai_baset ai,
const namespacet ns 
)
finaloverridevirtual

how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)

"this" is the domain before the instruction "from" "from" is the instruction to be interpretted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())

Implements ai_domain_baset.

Definition at line 59 of file interval_domain.cpp.

Member Data Documentation

◆ bottom

bool interval_domaint::bottom
protected

Definition at line 116 of file interval_domain.h.

◆ float_map

float_mapt interval_domaint::float_map
protected

Definition at line 122 of file interval_domain.h.

◆ int_map

int_mapt interval_domaint::int_map
protected

Definition at line 121 of file interval_domain.h.


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