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
 
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
 Make this domain 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 void transform (const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns)
 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...
 
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' A default constructor is not part of the domain interface. More...
 
 ai_domain_baset (const ai_domain_baset &old)
 A copy constructor is part of the domain interface. 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
 
typedef ai_history_baset::trace_ptrt trace_ptrt
 

Detailed Description

Definition at line 23 of file interval_domain.h.

Member Typedef Documentation

◆ float_mapt

Definition at line 118 of file interval_domain.h.

◆ int_mapt

Definition at line 117 of file interval_domain.h.

Constructor & Destructor Documentation

◆ interval_domaint()

interval_domaint::interval_domaint ( )
inline

Definition at line 30 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 482 of file interval_domain.cpp.

◆ assign()

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

Definition at line 209 of file interval_domain.cpp.

◆ assume()

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

Definition at line 349 of file interval_domain.cpp.

◆ assume_rec() [1/2]

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

Definition at line 356 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 237 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 215 of file interval_domain.cpp.

◆ is_bottom()

bool interval_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 80 of file interval_domain.h.

◆ is_float()

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

Definition at line 105 of file interval_domain.h.

◆ is_int()

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

Definition at line 100 of file interval_domain.h.

◆ is_top()

bool interval_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 91 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 151 of file interval_domain.cpp.

◆ make_bottom()

void interval_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 60 of file interval_domain.h.

◆ make_entry()

void interval_domaint::make_entry ( )
inlinefinaloverridevirtual

Make this domain a reasonable entry-point state.

Implements ai_domain_baset.

Definition at line 75 of file interval_domain.h.

◆ make_expression()

exprt interval_domaint::make_expression ( const symbol_exprt src) const

Definition at line 402 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 68 of file interval_domain.h.

◆ merge()

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

Definition at line 51 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
Deprecated:
SINCE(2019, 08, 01, "use the history signature instead")

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 115 of file interval_domain.h.

◆ float_map

float_mapt interval_domaint::float_map
protected

Definition at line 121 of file interval_domain.h.

◆ int_map

int_mapt interval_domaint::int_map
protected

Definition at line 120 of file interval_domain.h.


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