cprover
interval_domain.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interval Domain
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "interval_domain.h"
13 
14 #ifdef DEBUG
15 #include <iostream>
16 #include <langapi/language_util.h>
17 #endif
18 
19 #include <util/simplify_expr.h>
20 #include <util/std_expr.h>
21 #include <util/arith_tools.h>
22 
24  std::ostream &out,
25  const ai_baset &,
26  const namespacet &) const
27 {
28  if(bottom)
29  {
30  out << "BOTTOM\n";
31  return;
32  }
33 
34  for(const auto &interval : int_map)
35  {
36  if(interval.second.is_top())
37  continue;
38  if(interval.second.lower_set)
39  out << interval.second.lower << " <= ";
40  out << interval.first;
41  if(interval.second.upper_set)
42  out << " <= " << interval.second.upper;
43  out << "\n";
44  }
45 
46  for(const auto &interval : float_map)
47  {
48  if(interval.second.is_top())
49  continue;
50  if(interval.second.lower_set)
51  out << interval.second.lower << " <= ";
52  out << interval.first;
53  if(interval.second.upper_set)
54  out << " <= " << interval.second.upper;
55  out << "\n";
56  }
57 }
58 
60  const irep_idt &function_from,
61  trace_ptrt trace_from,
62  const irep_idt &function_to,
63  trace_ptrt trace_to,
64  ai_baset &ai,
65  const namespacet &ns)
66 {
67  locationt from{trace_from->current_location()};
68  locationt to{trace_to->current_location()};
69 
70  const goto_programt::instructiont &instruction=*from;
71  switch(instruction.type)
72  {
73  case DECL:
74  havoc_rec(instruction.decl_symbol());
75  break;
76 
77  case DEAD:
78  havoc_rec(instruction.dead_symbol());
79  break;
80 
81  case ASSIGN:
82  assign(to_code_assign(instruction.code));
83  break;
84 
85  case GOTO:
86  {
87  // Comparing iterators is safe as the target must be within the same list
88  // of instructions because this is a GOTO.
89  locationt next = from;
90  next++;
91  if(from->get_target() != next) // If equal then a skip
92  {
93  if(next == to)
94  assume(not_exprt(instruction.get_condition()), ns);
95  else
96  assume(instruction.get_condition(), ns);
97  }
98  break;
99  }
100 
101  case ASSUME:
102  assume(instruction.get_condition(), ns);
103  break;
104 
105  case FUNCTION_CALL:
106  {
107  const code_function_callt &code_function_call =
108  to_code_function_call(instruction.code);
109  if(code_function_call.lhs().is_not_nil())
110  havoc_rec(code_function_call.lhs());
111  break;
112  }
113 
114  case CATCH:
115  case THROW:
116  DATA_INVARIANT(false, "Exceptions must be removed before analysis");
117  break;
118  case RETURN:
119  DATA_INVARIANT(false, "Returns must be removed before analysis");
120  break;
121  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
122  case ATOMIC_END: // Ignoring is a valid over-approximation
123  case END_FUNCTION: // No action required
124  case START_THREAD: // Require a concurrent analysis at higher level
125  case END_THREAD: // Require a concurrent analysis at higher level
126  case ASSERT: // No action required
127  case LOCATION: // No action required
128  case SKIP: // No action required
129  break;
130  case OTHER:
131 #if 0
132  DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
133 #endif
134  break;
135  case INCOMPLETE_GOTO:
136  case NO_INSTRUCTION_TYPE:
137  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
138  break;
139  }
140 }
141 
155  const interval_domaint &b)
156 {
157  if(b.bottom)
158  return false;
159  if(bottom)
160  {
161  *this=b;
162  return true;
163  }
164 
165  bool result=false;
166 
167  for(int_mapt::iterator it=int_map.begin();
168  it!=int_map.end(); ) // no it++
169  {
170  // search for the variable that needs to be merged
171  // containers have different size and variable order
172  const int_mapt::const_iterator b_it=b.int_map.find(it->first);
173  if(b_it==b.int_map.end())
174  {
175  it=int_map.erase(it);
176  result=true;
177  }
178  else
179  {
180  integer_intervalt previous=it->second;
181  it->second.join(b_it->second);
182  if(it->second!=previous)
183  result=true;
184 
185  it++;
186  }
187  }
188 
189  for(float_mapt::iterator it=float_map.begin();
190  it!=float_map.end(); ) // no it++
191  {
192  const float_mapt::const_iterator b_it=b.float_map.begin();
193  if(b_it==b.float_map.end())
194  {
195  it=float_map.erase(it);
196  result=true;
197  }
198  else
199  {
200  ieee_float_intervalt previous=it->second;
201  it->second.join(b_it->second);
202  if(it->second!=previous)
203  result=true;
204 
205  it++;
206  }
207  }
208 
209  return result;
210 }
211 
212 void interval_domaint::assign(const code_assignt &code_assign)
213 {
214  havoc_rec(code_assign.lhs());
215  assume_rec(code_assign.lhs(), ID_equal, code_assign.rhs());
216 }
217 
219 {
220  if(lhs.id()==ID_if)
221  {
222  havoc_rec(to_if_expr(lhs).true_case());
223  havoc_rec(to_if_expr(lhs).false_case());
224  }
225  else if(lhs.id()==ID_symbol)
226  {
227  irep_idt identifier=to_symbol_expr(lhs).get_identifier();
228 
229  if(is_int(lhs.type()))
230  int_map.erase(identifier);
231  else if(is_float(lhs.type()))
232  float_map.erase(identifier);
233  }
234  else if(lhs.id()==ID_typecast)
235  {
236  havoc_rec(to_typecast_expr(lhs).op());
237  }
238 }
239 
241  const exprt &lhs, irep_idt id, const exprt &rhs)
242 {
243  if(lhs.id()==ID_typecast)
244  return assume_rec(to_typecast_expr(lhs).op(), id, rhs);
245 
246  if(rhs.id()==ID_typecast)
247  return assume_rec(lhs, id, to_typecast_expr(rhs).op());
248 
249  if(id==ID_equal)
250  {
251  assume_rec(lhs, ID_ge, rhs);
252  assume_rec(lhs, ID_le, rhs);
253  return;
254  }
255 
256  if(id==ID_notequal)
257  return; // won't do split
258 
259  if(id==ID_ge)
260  return assume_rec(rhs, ID_le, lhs);
261 
262  if(id==ID_gt)
263  return assume_rec(rhs, ID_lt, lhs);
264 
265  // we now have lhs < rhs or
266  // lhs <= rhs
267 
268  assert(id==ID_lt || id==ID_le);
269 
270  #ifdef DEBUG
271  std::cout << "assume_rec: "
272  << from_expr(lhs) << " " << id << " "
273  << from_expr(rhs) << "\n";
274  #endif
275 
276  if(lhs.id()==ID_symbol && rhs.id()==ID_constant)
277  {
278  irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
279 
280  if(is_int(lhs.type()) && is_int(rhs.type()))
281  {
282  mp_integer tmp = numeric_cast_v<mp_integer>(to_constant_expr(rhs));
283  if(id==ID_lt)
284  --tmp;
285  integer_intervalt &ii=int_map[lhs_identifier];
286  ii.make_le_than(tmp);
287  if(ii.is_bottom())
288  make_bottom();
289  }
290  else if(is_float(lhs.type()) && is_float(rhs.type()))
291  {
292  ieee_floatt tmp(to_constant_expr(rhs));
293  if(id==ID_lt)
294  tmp.decrement();
295  ieee_float_intervalt &fi=float_map[lhs_identifier];
296  fi.make_le_than(tmp);
297  if(fi.is_bottom())
298  make_bottom();
299  }
300  }
301  else if(lhs.id()==ID_constant && rhs.id()==ID_symbol)
302  {
303  irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
304 
305  if(is_int(lhs.type()) && is_int(rhs.type()))
306  {
307  mp_integer tmp = numeric_cast_v<mp_integer>(to_constant_expr(lhs));
308  if(id==ID_lt)
309  ++tmp;
310  integer_intervalt &ii=int_map[rhs_identifier];
311  ii.make_ge_than(tmp);
312  if(ii.is_bottom())
313  make_bottom();
314  }
315  else if(is_float(lhs.type()) && is_float(rhs.type()))
316  {
317  ieee_floatt tmp(to_constant_expr(lhs));
318  if(id==ID_lt)
319  tmp.increment();
320  ieee_float_intervalt &fi=float_map[rhs_identifier];
321  fi.make_ge_than(tmp);
322  if(fi.is_bottom())
323  make_bottom();
324  }
325  }
326  else if(lhs.id()==ID_symbol && rhs.id()==ID_symbol)
327  {
328  irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
329  irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
330 
331  if(is_int(lhs.type()) && is_int(rhs.type()))
332  {
333  integer_intervalt &lhs_i=int_map[lhs_identifier];
334  integer_intervalt &rhs_i=int_map[rhs_identifier];
335  if(id == ID_lt && !lhs_i.is_less_than(rhs_i))
336  lhs_i.make_less_than(rhs_i);
337  if(id == ID_le && !lhs_i.is_less_than_eq(rhs_i))
338  lhs_i.make_less_than_eq(rhs_i);
339  }
340  else if(is_float(lhs.type()) && is_float(rhs.type()))
341  {
342  ieee_float_intervalt &lhs_i=float_map[lhs_identifier];
343  ieee_float_intervalt &rhs_i=float_map[rhs_identifier];
344  lhs_i.meet(rhs_i);
345  rhs_i=lhs_i;
346  if(rhs_i.is_bottom())
347  make_bottom();
348  }
349  }
350 }
351 
353  const exprt &cond,
354  const namespacet &ns)
355 {
356  assume_rec(simplify_expr(cond, ns), false);
357 }
358 
360  const exprt &cond,
361  bool negation)
362 {
363  if(cond.id()==ID_lt || cond.id()==ID_le ||
364  cond.id()==ID_gt || cond.id()==ID_ge ||
365  cond.id()==ID_equal || cond.id()==ID_notequal)
366  {
367  const auto &rel = to_binary_relation_expr(cond);
368 
369  if(negation) // !x<y ---> x>=y
370  {
371  if(rel.id() == ID_lt)
372  assume_rec(rel.op0(), ID_ge, rel.op1());
373  else if(rel.id() == ID_le)
374  assume_rec(rel.op0(), ID_gt, rel.op1());
375  else if(rel.id() == ID_gt)
376  assume_rec(rel.op0(), ID_le, rel.op1());
377  else if(rel.id() == ID_ge)
378  assume_rec(rel.op0(), ID_lt, rel.op1());
379  else if(rel.id() == ID_equal)
380  assume_rec(rel.op0(), ID_notequal, rel.op1());
381  else if(rel.id() == ID_notequal)
382  assume_rec(rel.op0(), ID_equal, rel.op1());
383  }
384  else
385  assume_rec(rel.op0(), rel.id(), rel.op1());
386  }
387  else if(cond.id()==ID_not)
388  {
389  assume_rec(to_not_expr(cond).op(), !negation);
390  }
391  else if(cond.id()==ID_and)
392  {
393  if(!negation)
394  forall_operands(it, cond)
395  assume_rec(*it, false);
396  }
397  else if(cond.id()==ID_or)
398  {
399  if(negation)
400  forall_operands(it, cond)
401  assume_rec(*it, true);
402  }
403 }
404 
406 {
407  if(is_int(src.type()))
408  {
409  int_mapt::const_iterator i_it=int_map.find(src.get_identifier());
410  if(i_it==int_map.end())
411  return true_exprt();
412 
413  const integer_intervalt &interval=i_it->second;
414  if(interval.is_top())
415  return true_exprt();
416  if(interval.is_bottom())
417  return false_exprt();
418 
419  exprt::operandst conjuncts;
420 
421  if(interval.upper_set)
422  {
423  exprt tmp=from_integer(interval.upper, src.type());
424  conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
425  }
426 
427  if(interval.lower_set)
428  {
429  exprt tmp=from_integer(interval.lower, src.type());
430  conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
431  }
432 
433  return conjunction(conjuncts);
434  }
435  else if(is_float(src.type()))
436  {
437  float_mapt::const_iterator i_it=float_map.find(src.get_identifier());
438  if(i_it==float_map.end())
439  return true_exprt();
440 
441  const ieee_float_intervalt &interval=i_it->second;
442  if(interval.is_top())
443  return true_exprt();
444  if(interval.is_bottom())
445  return false_exprt();
446 
447  exprt::operandst conjuncts;
448 
449  if(interval.upper_set)
450  {
451  exprt tmp=interval.upper.to_expr();
452  conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
453  }
454 
455  if(interval.lower_set)
456  {
457  exprt tmp=interval.lower.to_expr();
458  conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
459  }
460 
461  return conjunction(conjuncts);
462  }
463  else
464  return true_exprt();
465 }
466 
471 /*
472  * This implementation is aimed at reducing assertions to true, particularly
473  * range checks for arrays and other bounds checks.
474  *
475  * Rather than work with the various kinds of exprt directly, we use assume,
476  * join and is_bottom. It is sufficient for the use case and avoids duplicating
477  * functionality that is in assume anyway.
478  *
479  * As some expressions (1<=a && a<=2) can be represented exactly as intervals
480  * and some can't (a<1 || a>2), the way these operations are used varies
481  * depending on the structure of the expression to try to give the best results.
482  * For example negating a disjunction makes it easier for assume to handle.
483  */
484 
486  exprt &condition,
487  const namespacet &ns) const
488 {
489  bool unchanged=true;
490  interval_domaint d(*this);
491 
492  // merge intervals to properly handle conjunction
493  if(condition.id()==ID_and) // May be directly representable
494  {
496  a.make_top(); // a is everything
497  a.assume(condition, ns); // Restrict a to an over-approximation
498  // of when condition is true
499  if(!a.join(d)) // If d (this) is included in a...
500  { // Then the condition is always true
501  unchanged=condition.is_true();
502  condition = true_exprt();
503  }
504  }
505  else if(condition.id()==ID_symbol)
506  {
507  // TODO: we have to handle symbol expression
508  }
509  else // Less likely to be representable
510  {
511  d.assume(not_exprt(condition), ns); // Restrict to when condition is false
512  if(d.is_bottom()) // If there there are none...
513  { // Then the condition is always true
514  unchanged=condition.is_true();
515  condition = true_exprt();
516  }
517  }
518 
519  return unchanged;
520 }
interval_domaint::bottom
bool bottom
Definition: interval_domain.h:115
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
interval_templatet::make_ge_than
void make_ge_than(const T &v)
Definition: interval_template.h:91
ieee_floatt
Definition: ieee_float.h:120
conjunction
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:41
interval_domaint::transform
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_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...
Definition: interval_domain.cpp:59
arith_tools.h
interval_domaint::assume
void assume(const exprt &, const namespacet &)
Definition: interval_domain.cpp:352
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
ieee_floatt::decrement
void decrement(bool distinguish_zero=false)
Definition: ieee_float.h:224
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:337
interval_domaint::is_float
static bool is_float(const typet &src)
Definition: interval_domain.h:105
interval_templatet::make_less_than_eq
void make_less_than_eq(interval_templatet &i)
Definition: interval_template.h:153
interval_templatet::is_less_than
bool is_less_than(const interval_templatet &i)
Definition: interval_template.h:179
exprt
Base class for all expressions.
Definition: expr.h:54
interval_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Definition: interval_domain.cpp:23
interval_domaint::assign
void assign(const class code_assignt &assignment)
Definition: interval_domain.cpp:212
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
goto_programt::instructiont::decl_symbol
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:212
interval_templatet::meet
void meet(const interval_templatet< T > &i)
Definition: interval_template.h:112
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
interval_templatet
Definition: interval_template.h:20
interval_domaint::make_top
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
Definition: interval_domain.h:68
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
THROW
@ THROW
Definition: goto_program.h:51
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
GOTO
@ GOTO
Definition: goto_program.h:35
interval_templatet::is_top
bool is_top() const
Definition: interval_template.h:66
interval_templatet::upper
T upper
Definition: interval_template.h:44
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
goto_programt::instructiont::dead_symbol
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:254
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
language_util.h
interval_domaint::assume_rec
void assume_rec(const exprt &, bool negation=false)
Definition: interval_domain.cpp:359
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
interval_templatet::join
void join(const interval_templatet< T > &i)
Definition: interval_template.h:106
ieee_floatt::increment
void increment(bool distinguish_zero=false)
Definition: ieee_float.h:215
interval_domaint::ai_simplify
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Uses the abstract state to simplify a given expression using context- specific information.
Definition: interval_domain.cpp:485
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2529
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:34
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
interval_templatet::is_less_than_eq
bool is_less_than_eq(const interval_templatet &i)
Definition: interval_template.h:171
OTHER
@ OTHER
Definition: goto_program.h:38
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
false_exprt
The Boolean constant false.
Definition: std_expr.h:2726
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:43
SKIP
@ SKIP
Definition: goto_program.h:39
interval_templatet::is_bottom
bool is_bottom() const
Definition: interval_template.h:61
simplify_expr.h
RETURN
@ RETURN
Definition: goto_program.h:46
ASSIGN
@ ASSIGN
Definition: goto_program.h:47
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:77
interval_domain.h
Interval Domain.
interval_templatet::make_less_than
void make_less_than(interval_templatet &i)
Definition: interval_template.h:161
interval_domaint::is_bottom
bool is_bottom() const override final
Definition: interval_domain.h:80
CATCH
@ CATCH
Definition: goto_program.h:52
DECL
@ DECL
Definition: goto_program.h:48
interval_domaint
Definition: interval_domain.h:24
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2067
interval_domaint::float_map
float_mapt float_map
Definition: interval_domain.h:121
interval_domaint::make_expression
exprt make_expression(const symbol_exprt &) const
Definition: interval_domain.cpp:405
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
ASSUME
@ ASSUME
Definition: goto_program.h:36
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
interval_domaint::join
bool join(const interval_domaint &b)
Sets *this to the mathematical join between the two domains.
Definition: interval_domain.cpp:154
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
START_THREAD
@ START_THREAD
Definition: goto_program.h:40
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:50
interval_domaint::make_bottom
void make_bottom() final override
no states
Definition: interval_domain.h:60
interval_templatet::make_le_than
void make_le_than(const T &v)
Definition: interval_template.h:77
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:45
DEAD
@ DEAD
Definition: goto_program.h:49
interval_templatet::upper_set
bool upper_set
Definition: interval_template.h:43
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:44
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:350
LOCATION
@ LOCATION
Definition: goto_program.h:42
interval_domaint::is_int
static bool is_int(const typet &src)
Definition: interval_domain.h:100
ASSERT
@ ASSERT
Definition: goto_program.h:37
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
std_expr.h
API to expression classes.
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:724
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
END_THREAD
@ END_THREAD
Definition: goto_program.h:41
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:53
interval_templatet::lower_set
bool lower_set
Definition: interval_template.h:43
interval_domaint::havoc_rec
void havoc_rec(const exprt &)
Definition: interval_domain.cpp:218
not_exprt
Boolean negation.
Definition: std_expr.h:2042
interval_templatet::lower
T lower
Definition: interval_template.h:44
interval_domaint::int_map
int_mapt int_map
Definition: interval_domain.h:120
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701