diff --git a/regression/goto-analyzer/intervals2/intervals2.c b/regression/goto-analyzer/intervals2/intervals2.c new file mode 100644 index 00000000000..d1eaf25240e --- /dev/null +++ b/regression/goto-analyzer/intervals2/intervals2.c @@ -0,0 +1,11 @@ +#include + +int main(){ + int x; + if (x > 0) { + if (x < 20) { + assert(x > -10 && x < 100); + } + } + return 0; +} diff --git a/regression/goto-analyzer/intervals2/test.desc b/regression/goto-analyzer/intervals2/test.desc new file mode 100644 index 00000000000..0c017f6b333 --- /dev/null +++ b/regression/goto-analyzer/intervals2/test.desc @@ -0,0 +1,8 @@ +CORE +intervals2.c +--intervals +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals2.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals3/intervals3.c b/regression/goto-analyzer/intervals3/intervals3.c new file mode 100644 index 00000000000..bbaa3ce4e1e --- /dev/null +++ b/regression/goto-analyzer/intervals3/intervals3.c @@ -0,0 +1,11 @@ +#include + +int main(){ + int x; + if (x > 0) { + if (x < 20) { + assert(x > -10 || x < 100); + } + } + return 0; +} diff --git a/regression/goto-analyzer/intervals3/test.desc b/regression/goto-analyzer/intervals3/test.desc new file mode 100644 index 00000000000..5db07df08a4 --- /dev/null +++ b/regression/goto-analyzer/intervals3/test.desc @@ -0,0 +1,8 @@ +CORE +intervals3.c +--intervals +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals3.c line 7 function main, assertion x > -10 || x < 100: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals4/intervals4.c b/regression/goto-analyzer/intervals4/intervals4.c new file mode 100644 index 00000000000..e9bc51f30b5 --- /dev/null +++ b/regression/goto-analyzer/intervals4/intervals4.c @@ -0,0 +1,12 @@ +//#include + +int main() +{ + int i; + + if(i>0) + if(i<3) + assert(i>=1 && i<=2); + + return 0; +} diff --git a/regression/goto-analyzer/intervals4/test.desc b/regression/goto-analyzer/intervals4/test.desc new file mode 100644 index 00000000000..9f56ff02403 --- /dev/null +++ b/regression/goto-analyzer/intervals4/test.desc @@ -0,0 +1,8 @@ +CORE +intervals4.c +--intervals +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals4.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals5/intervals5.c b/regression/goto-analyzer/intervals5/intervals5.c new file mode 100644 index 00000000000..960e7473cc6 --- /dev/null +++ b/regression/goto-analyzer/intervals5/intervals5.c @@ -0,0 +1,12 @@ +//#include + +int main() +{ + int i; + + if(i>0) + if(i<3) + assert(i>=1 || i<=2); + + return 0; +} diff --git a/regression/goto-analyzer/intervals5/test.desc b/regression/goto-analyzer/intervals5/test.desc new file mode 100644 index 00000000000..42554724e2d --- /dev/null +++ b/regression/goto-analyzer/intervals5/test.desc @@ -0,0 +1,8 @@ +CORE +intervals5.c +--intervals +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals5.c line 9 function main, assertion i >= 1 || i <= 2: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals6/intervals6.c b/regression/goto-analyzer/intervals6/intervals6.c new file mode 100644 index 00000000000..e93240e7573 --- /dev/null +++ b/regression/goto-analyzer/intervals6/intervals6.c @@ -0,0 +1,11 @@ +#include + +int main(){ + int x; + if (x > 0) { + if (x < 20) { + assert(x < -10 || x > 100); + } + } + return 0; +} diff --git a/regression/goto-analyzer/intervals6/test.desc b/regression/goto-analyzer/intervals6/test.desc new file mode 100644 index 00000000000..14fd64f33dd --- /dev/null +++ b/regression/goto-analyzer/intervals6/test.desc @@ -0,0 +1,8 @@ +CORE +intervals6.c +--intervals +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: UNKNOWN$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals7/intervals7.c b/regression/goto-analyzer/intervals7/intervals7.c new file mode 100644 index 00000000000..c893c413ad5 --- /dev/null +++ b/regression/goto-analyzer/intervals7/intervals7.c @@ -0,0 +1,11 @@ +#include + +int main(){ + int x; + if (x > 0) { + if (x < 20) { + assert(x < -10 && x > 100); + } + } + return 0; +} diff --git a/regression/goto-analyzer/intervals7/test.desc b/regression/goto-analyzer/intervals7/test.desc new file mode 100644 index 00000000000..aeeb24bd0a9 --- /dev/null +++ b/regression/goto-analyzer/intervals7/test.desc @@ -0,0 +1,8 @@ +CORE +intervals7.c +--intervals +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: UNKNOWN$ +-- +^warning: ignoring diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 29bfc7a1a63..4f8aca54d4b 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -148,7 +148,7 @@ bool interval_domaint::merge( if(bottom) { *this=b; return true; } bool result=false; - + for(int_mapt::iterator it=int_map.begin(); it!=int_map.end(); ) // no it++ { @@ -293,7 +293,7 @@ void interval_domaint::assume_rec( if(lhs.id()==ID_symbol && rhs.id()==ID_constant) { irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier(); - + if(is_int(lhs.type()) && is_int(rhs.type())) { mp_integer tmp;