From 21718331168979d1d033b2c890c90fc3e0450f3e Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Mon, 10 Sep 2018 12:37:53 +0100 Subject: [PATCH 1/2] Assume relation between two symbols --- src/analyses/interval_domain.cpp | 8 +++---- src/util/interval_template.h | 41 ++++++++++++++++++++++++++++++++ 2 files changed, 45 insertions(+), 4 deletions(-) diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index b857a74dd8f..06222ec5afa 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -329,10 +329,10 @@ void interval_domaint::assume_rec( { integer_intervalt &lhs_i=int_map[lhs_identifier]; integer_intervalt &rhs_i=int_map[rhs_identifier]; - lhs_i.meet(rhs_i); - rhs_i=lhs_i; - if(rhs_i.is_bottom()) - make_bottom(); + if(id == ID_lt && !lhs_i.is_less_than(rhs_i)) + lhs_i.make_less_than(rhs_i); + if(id == ID_le && !lhs_i.is_less_than_eq(rhs_i)) + lhs_i.make_less_than_eq(rhs_i); } else if(is_float(lhs.type()) && is_float(rhs.type())) { diff --git a/src/util/interval_template.h b/src/util/interval_template.h index c6a3e64b0ef..ab2244edc69 100644 --- a/src/util/interval_template.h +++ b/src/util/interval_template.h @@ -143,6 +143,47 @@ template class interval_templatet } } + void make_bottom() + { + lower_set = upper_set = true; + upper = T(); + lower = upper + 1; + } + + void make_less_than_eq(interval_templatet &i) + { + if(upper_set && i.upper_set) + upper = std::min(upper, i.upper); + if(lower_set && i.lower_set) + i.lower = std::max(lower, i.lower); + } + + void make_less_than(interval_templatet &i) + { + make_less_than_eq(i); + if(singleton() && i.singleton() && lower == i.lower) + { + make_bottom(); + i.make_bottom(); + } + } + + bool is_less_than_eq(const interval_templatet &i) + { + if(i.lower_set && upper_set && upper <= i.lower) + return true; + else + return false; + } + + bool is_less_than(const interval_templatet &i) + { + if(i.lower_set && upper_set && upper < i.lower) + return true; + else + return false; + } + void approx_union_with(const interval_templatet &i) { if(i.lower_set && lower_set) From d05b9c66dbe2f0b68178e12e3a1b892ea77fd9e4 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 28 May 2020 11:54:38 +0100 Subject: [PATCH 2/2] Add test for checking symbolic comparisons --- .../goto-analyzer/intervals_simple-loops/main.c | 15 +++++++++++++++ .../intervals_simple-loops/test.desc | 11 +++++++++++ 2 files changed, 26 insertions(+) create mode 100644 regression/goto-analyzer/intervals_simple-loops/main.c create mode 100644 regression/goto-analyzer/intervals_simple-loops/test.desc diff --git a/regression/goto-analyzer/intervals_simple-loops/main.c b/regression/goto-analyzer/intervals_simple-loops/main.c new file mode 100644 index 00000000000..2f6eba4184b --- /dev/null +++ b/regression/goto-analyzer/intervals_simple-loops/main.c @@ -0,0 +1,15 @@ +#include +const int g_N = 2; + +void main(void) +{ + for(int i = 0; i < g_N; i++) + { + assert(0); + } + + for(int j = 4; j >= g_N; j--) + { + assert(0); + } +} diff --git a/regression/goto-analyzer/intervals_simple-loops/test.desc b/regression/goto-analyzer/intervals_simple-loops/test.desc new file mode 100644 index 00000000000..d3c31abbef1 --- /dev/null +++ b/regression/goto-analyzer/intervals_simple-loops/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--intervals +^EXIT=0$ +^SIGNAL=0$ +\[main\.assertion\.1\] line 8 assertion 0: UNKNOWN +\[main\.assertion\.2\] line 13 assertion 0: UNKNOWN +-- +-- +Test comparision between two symbols does not mark the +result as bottom