CBMC
interval_constraint.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interval constraint
4 
5 Author: Jeannie Moulton
6 
7 \*******************************************************************/
8 
9 #include "interval_constraint.h"
10 #include "arith_tools.h"
11 
12 exprt interval_constraint(const exprt &expr, const integer_intervalt &interval)
13 {
14  // expr >= lower_bound && expr <= upper_bound
15  return and_exprt(
16  binary_relation_exprt(
17  expr, ID_ge, from_integer(interval.lower, expr.type())),
18  binary_relation_exprt(
19  expr, ID_le, from_integer(interval.upper, expr.type())));
20 }
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
arith_tools.h
and_exprt
Boolean AND.
Definition: std_expr.h:2125
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
exprt
Base class for all expressions.
Definition: expr.h:56
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
interval_templatet
Definition: interval_template.h:20
interval_constraint
exprt interval_constraint(const exprt &expr, const integer_intervalt &interval)
Given an exprt and an integer interval return an exprt that represents restricting the expression to ...
Definition: interval_constraint.cpp:12
interval_constraint.h