interval_domain.cpp File Reference

Interval Domain. More...

#include <goto-programs/abstract-interpretation/interval_domain.h>
#include <goto-programs/abstract-interpretation/bitwise_bounds.h>
#include <util/arith/arith_tools.h>
#include <util/lang/c_typecast.h>
#include <util/irep/std_expr.h>
#include <util/base/prefix.h>
#include <optional>
#include <string_view>
#include <unordered_set>

Include dependency graph for interval_domain.cpp:

Functions
template<>
interval_domaint::integer_intervalt	interval_domaint::generate_modular_interval< interval_domaint::integer_intervalt > (const type2tc &t) const
template<>
interval_domaint::real_intervalt	interval_domaint::generate_modular_interval< interval_domaint::real_intervalt > (const type2tc &) const
template<>
bool	interval_domaint::is_mapped< interval_domaint::integer_intervalt > (const symbol2t &sym) const
template<>
bool	interval_domaint::is_mapped< interval_domaint::real_intervalt > (const symbol2t &sym) const
template<>
expr2tc	interval_domaint::make_expression_value< interval_domaint::integer_intervalt > (const interval_domaint::integer_intervalt &interval, const type2tc &type, bool is_upper) const
template<>
expr2tc	interval_domaint::make_expression_value< interval_domaint::real_intervalt > (const interval_domaint::real_intervalt &interval, const type2tc &type, bool upper) const
template<class Interval>
void	print_interval (const interval_templatet< Interval > &i, const std::string &name, std::ostream &out)
bool	contains_float (const expr2tc &e)
bool	do_is_subset (const interval_domaint::interval &a, const interval_domaint::interval &b)
static std::optional< size_t >	first_written_argument (const irep_idt &callee)
static expr2tc	pointed_object (expr2tc address)
	The object address points into, or nil when that is not statically known.

Detailed Description

Interval Domain.

Function Documentation

contains_float()

bool contains_float

(

const expr2tc &

e

)

do_is_subset()

bool do_is_subset	(	const interval_domaint::interval &	a,
		const interval_domaint::interval &	b )

first_written_argument()

std::optional< size_t > first_written_argument ( const irep_idt & callee )

static

interval_domaint::generate_modular_interval< interval_domaint::integer_intervalt >()

template<>

interval_domaint::integer_intervalt interval_domaint::generate_modular_interval< interval_domaint::integer_intervalt >

(

const type2tc &

t

)

const

interval_domaint::generate_modular_interval< interval_domaint::real_intervalt >()

template<>

interval_domaint::real_intervalt interval_domaint::generate_modular_interval< interval_domaint::real_intervalt >

(

const type2tc &

)

const

interval_domaint::is_mapped< interval_domaint::integer_intervalt >()

template<>

bool interval_domaint::is_mapped< interval_domaint::integer_intervalt >

(

const symbol2t &

sym

)

const

interval_domaint::is_mapped< interval_domaint::real_intervalt >()

template<>

bool interval_domaint::is_mapped< interval_domaint::real_intervalt >

(

const symbol2t &

sym

)

const

interval_domaint::make_expression_value< interval_domaint::integer_intervalt >()

template<>

expr2tc interval_domaint::make_expression_value< interval_domaint::integer_intervalt >	(	const interval_domaint::integer_intervalt &	interval,
		const type2tc &	type,
		bool	is_upper ) const

interval_domaint::make_expression_value< interval_domaint::real_intervalt >()

template<>

expr2tc interval_domaint::make_expression_value< interval_domaint::real_intervalt >	(	const interval_domaint::real_intervalt &	interval,
		const type2tc &	type,
		bool	upper ) const

pointed_object()

expr2tc pointed_object ( expr2tc address )

static

The object address points into, or nil when that is not statically known.

print_interval()

template<class Interval>

void print_interval	(	const interval_templatet< Interval > &	i,
		const std::string &	name,
		std::ostream &	out )