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