CBMC: /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/widened_range.cpp Source File

12 static bool has_underflowed(const exprt &value)

13{

14 return constant_interval_exprt::greater_than(

15 value, from_integer(0, value.type()));

16}

17 static bool has_overflowed(const exprt &value, const exprt &initial_value)

18{

19 return constant_interval_exprt::less_than(value, initial_value);

20}

22 exprt widened_ranget::widen_lower_bound() const

23{

24 if(!is_lower_widened)

25 return lower_bound;

26

27 auto new_lower_bound = simplify_expr(minus_exprt(lower_bound, range_), ns_);

28

29 if(

30 constant_interval_exprt::contains_extreme(new_lower_bound) ||

31 has_underflowed(new_lower_bound))

32 return min_value_exprt(lower_bound.type());

33

34 return new_lower_bound;

35}

37 exprt widened_ranget::widen_upper_bound() const

38{

39 if(!is_upper_widened)

40 return upper_bound;

41

42 auto new_upper_bound = simplify_expr(plus_exprt(upper_bound, range_), ns_);

43

44 if(

45 constant_interval_exprt::contains_extreme(new_upper_bound) ||

46 has_overflowed(new_upper_bound, upper_bound))

47 return max_value_exprt(upper_bound.type());

48

49 return new_upper_bound;

50}

from_integer

constant_exprt from_integer(const mp_integer &int_value, const typet &type)

Definition arith_tools.cpp:100

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

constant_interval_exprt::greater_than

tvt greater_than(const constant_interval_exprt &o) const

Definition interval.cpp:397

constant_interval_exprt::contains_extreme

static bool contains_extreme(const exprt expr)

Definition interval.cpp:1830

constant_interval_exprt::less_than

tvt less_than(const constant_interval_exprt &o) const

Definition interval.cpp:376

exprt

Base class for all expressions.

Definition expr.h:57

exprt::type

typet & type()

Return the type of the expression.

Definition expr.h:85

max_value_exprt

+∞ upper bound for intervals

Definition interval.h:18

min_value_exprt

-∞ upper bound for intervals

Definition interval.h:33

minus_exprt

Binary minus.

Definition std_expr.h:1065

plus_exprt

The plus expression Associativity is not specified.

Definition std_expr.h:1006

widened_ranget::upper_bound

const exprt upper_bound

Definition widened_range.h:43

widened_ranget::widen_lower_bound

exprt widen_lower_bound() const

Definition widened_range.cpp:22

widened_ranget::is_upper_widened

const bool is_upper_widened

Definition widened_range.h:41

widened_ranget::ns_

namespacet ns_

Definition widened_range.h:46

widened_ranget::lower_bound

const exprt lower_bound

Definition widened_range.h:42

widened_ranget::widen_upper_bound

exprt widen_upper_bound() const

Definition widened_range.cpp:37

widened_ranget::range_

exprt range_

Definition widened_range.h:47

widened_ranget::is_lower_widened

const bool is_lower_widened

Definition widened_range.h:40

simplify_expr

exprt simplify_expr(exprt src, const namespacet &ns)

Definition simplify_expr.cpp:3412

simplify_expr.h

has_overflowed

static bool has_overflowed(const exprt &value, const exprt &initial_value)

Definition widened_range.cpp:17

has_underflowed

static bool has_underflowed(const exprt &value)

Definition widened_range.cpp:12

widened_range.h