CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
widened_range.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: helper for extending intervals during widening merges
4
5 Author: Jez Higgins
6
7\*******************************************************************/
8
9#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H
10#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H
11
12#include <util/arith_tools.h>
13#include <util/interval.h>
14#include <util/namespace.h>
15#include <util/symbol_table.h>
16
18{
19public:
21 const constant_interval_exprt &lhs,
22 const constant_interval_exprt &rhs)
24 constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower())),
26 constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper())),
28 constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower())),
30 constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper())),
34 from_integer(1, lhs.type()))),
37 {
38 }
39
40 const bool is_lower_widened;
41 const bool is_upper_widened;
44
45private:
48
49public:
52
53private:
56};
57
58#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Represents an interval of values.
Definition interval.h:52
Base class for all expressions.
Definition expr.h:56
Binary minus.
Definition std_expr.h:1061
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The symbol table.
widened_ranget(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
const exprt upper_bound
exprt widen_lower_bound() const
const bool is_upper_widened
namespacet ns_
const exprt widened_upper_bound
const exprt lower_bound
exprt widen_upper_bound() const
const exprt widened_lower_bound
const bool is_lower_widened
binary_relation_exprt less_than(exprt lhs, exprt rhs)
Definition string_expr.h:49
Author: Diffblue Ltd.