Skip to content

Commit 830c302

Browse files
author
Thomas Kiley
authored
Merge pull request #5362 from thk123/assume-relation
Assume relation between two symbols
2 parents df9ef23 + d05b9c6 commit 830c302

File tree

4 files changed

+71
-4
lines changed

4 files changed

+71
-4
lines changed
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <assert.h>
2+
const int g_N = 2;
3+
4+
void main(void)
5+
{
6+
for(int i = 0; i < g_N; i++)
7+
{
8+
assert(0);
9+
}
10+
11+
for(int j = 4; j >= g_N; j--)
12+
{
13+
assert(0);
14+
}
15+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--intervals
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main\.assertion\.1\] line 8 assertion 0: UNKNOWN
7+
\[main\.assertion\.2\] line 13 assertion 0: UNKNOWN
8+
--
9+
--
10+
Test comparision between two symbols does not mark the
11+
result as bottom

src/analyses/interval_domain.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -329,10 +329,10 @@ void interval_domaint::assume_rec(
329329
{
330330
integer_intervalt &lhs_i=int_map[lhs_identifier];
331331
integer_intervalt &rhs_i=int_map[rhs_identifier];
332-
lhs_i.meet(rhs_i);
333-
rhs_i=lhs_i;
334-
if(rhs_i.is_bottom())
335-
make_bottom();
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);
336336
}
337337
else if(is_float(lhs.type()) && is_float(rhs.type()))
338338
{

src/util/interval_template.h

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,47 @@ template<class T> class interval_templatet
143143
}
144144
}
145145

146+
void make_bottom()
147+
{
148+
lower_set = upper_set = true;
149+
upper = T();
150+
lower = upper + 1;
151+
}
152+
153+
void make_less_than_eq(interval_templatet &i)
154+
{
155+
if(upper_set && i.upper_set)
156+
upper = std::min(upper, i.upper);
157+
if(lower_set && i.lower_set)
158+
i.lower = std::max(lower, i.lower);
159+
}
160+
161+
void make_less_than(interval_templatet &i)
162+
{
163+
make_less_than_eq(i);
164+
if(singleton() && i.singleton() && lower == i.lower)
165+
{
166+
make_bottom();
167+
i.make_bottom();
168+
}
169+
}
170+
171+
bool is_less_than_eq(const interval_templatet &i)
172+
{
173+
if(i.lower_set && upper_set && upper <= i.lower)
174+
return true;
175+
else
176+
return false;
177+
}
178+
179+
bool is_less_than(const interval_templatet &i)
180+
{
181+
if(i.lower_set && upper_set && upper < i.lower)
182+
return true;
183+
else
184+
return false;
185+
}
186+
146187
void approx_union_with(const interval_templatet &i)
147188
{
148189
if(i.lower_set && lower_set)

0 commit comments

Comments
 (0)