From 7afdb25c61ea202f7d592719fa770f0f04e2ae8d Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 7 Jul 2016 12:02:08 -0300 Subject: [PATCH 1/6] add a new test case to goto-analyzer Signed-off-by: Lucas Cordeiro --- .../goto-analyzer/aisimplifier01/aisimplifier01.c | 11 +++++++++++ regression/goto-analyzer/aisimplifier01/test.desc | 8 ++++++++ 2 files changed, 19 insertions(+) create mode 100644 regression/goto-analyzer/aisimplifier01/aisimplifier01.c create mode 100644 regression/goto-analyzer/aisimplifier01/test.desc diff --git a/regression/goto-analyzer/aisimplifier01/aisimplifier01.c b/regression/goto-analyzer/aisimplifier01/aisimplifier01.c new file mode 100644 index 00000000000..d1eaf25240e --- /dev/null +++ b/regression/goto-analyzer/aisimplifier01/aisimplifier01.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/aisimplifier01/test.desc b/regression/goto-analyzer/aisimplifier01/test.desc new file mode 100644 index 00000000000..78863831f91 --- /dev/null +++ b/regression/goto-analyzer/aisimplifier01/test.desc @@ -0,0 +1,8 @@ +CORE +asimplifier01.c +--intervals +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file aisimplifier01.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$ +-- +^warning: ignoring From 671c03e3bece976f6d16db8d4f84e7c2b7294188 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 7 Jul 2016 14:13:24 -0300 Subject: [PATCH 2/6] rename test case Signed-off-by: Lucas Cordeiro --- .../goto-analyzer/aisimplifier01/aisimplifier01.c | 11 ----------- regression/goto-analyzer/aisimplifier01/test.desc | 8 -------- 2 files changed, 19 deletions(-) delete mode 100644 regression/goto-analyzer/aisimplifier01/aisimplifier01.c delete mode 100644 regression/goto-analyzer/aisimplifier01/test.desc diff --git a/regression/goto-analyzer/aisimplifier01/aisimplifier01.c b/regression/goto-analyzer/aisimplifier01/aisimplifier01.c deleted file mode 100644 index d1eaf25240e..00000000000 --- a/regression/goto-analyzer/aisimplifier01/aisimplifier01.c +++ /dev/null @@ -1,11 +0,0 @@ -#include - -int main(){ - int x; - if (x > 0) { - if (x < 20) { - assert(x > -10 && x < 100); - } - } - return 0; -} diff --git a/regression/goto-analyzer/aisimplifier01/test.desc b/regression/goto-analyzer/aisimplifier01/test.desc deleted file mode 100644 index 78863831f91..00000000000 --- a/regression/goto-analyzer/aisimplifier01/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -asimplifier01.c ---intervals -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file aisimplifier01.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$ --- -^warning: ignoring From 0b95f89c334cfc4a6eccd410e81a1ac7f56f729e Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 7 Jul 2016 14:14:17 -0300 Subject: [PATCH 3/6] add 4 new test cases to the goto-analyzer Signed-off-by: Lucas Cordeiro --- regression/goto-analyzer/intervals2/intervals2.c | 11 +++++++++++ regression/goto-analyzer/intervals2/test.desc | 8 ++++++++ regression/goto-analyzer/intervals3/intervals3.c | 11 +++++++++++ regression/goto-analyzer/intervals3/test.desc | 8 ++++++++ regression/goto-analyzer/intervals4/intervals4.c | 12 ++++++++++++ regression/goto-analyzer/intervals4/test.desc | 8 ++++++++ regression/goto-analyzer/intervals5/intervals5.c | 12 ++++++++++++ regression/goto-analyzer/intervals5/test.desc | 8 ++++++++ 8 files changed, 78 insertions(+) create mode 100644 regression/goto-analyzer/intervals2/intervals2.c create mode 100644 regression/goto-analyzer/intervals2/test.desc create mode 100644 regression/goto-analyzer/intervals3/intervals3.c create mode 100644 regression/goto-analyzer/intervals3/test.desc create mode 100644 regression/goto-analyzer/intervals4/intervals4.c create mode 100644 regression/goto-analyzer/intervals4/test.desc create mode 100644 regression/goto-analyzer/intervals5/intervals5.c create mode 100644 regression/goto-analyzer/intervals5/test.desc 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 From 0f4133d7188ccfb5d83f0d7b5569409e6c144ba9 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 7 Jul 2016 14:21:46 -0300 Subject: [PATCH 4/6] fix OR operator for interval domain Signed-off-by: Lucas Cordeiro --- src/analyses/interval_domain.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 29bfc7a1a63..e36280a1541 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; @@ -429,9 +429,9 @@ void interval_domaint::assume_rec( } else if(cond.id()==ID_or) { - if(negation) + if(!negation) forall_operands(it, cond) - assume_rec(*it, true); + assume_rec(*it, false); } } From d65b9a91f322353c56e15e51b2e26d23454eab0e Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 7 Jul 2016 14:28:45 -0300 Subject: [PATCH 5/6] add new test cases to goto-analyzer Signed-off-by: Lucas Cordeiro --- regression/goto-analyzer/intervals6/intervals6.c | 11 +++++++++++ regression/goto-analyzer/intervals6/test.desc | 8 ++++++++ regression/goto-analyzer/intervals7/intervals7.c | 11 +++++++++++ regression/goto-analyzer/intervals7/test.desc | 8 ++++++++ 4 files changed, 38 insertions(+) create mode 100644 regression/goto-analyzer/intervals6/intervals6.c create mode 100644 regression/goto-analyzer/intervals6/test.desc create mode 100644 regression/goto-analyzer/intervals7/intervals7.c create mode 100644 regression/goto-analyzer/intervals7/test.desc 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 From e375c415ac6707482a687ef5fa3d677bd31d4879 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Fri, 8 Jul 2016 11:09:38 -0300 Subject: [PATCH 6/6] we need to consider lower and upper limits to support the OR operator Signed-off-by: Lucas Cordeiro --- src/analyses/interval_domain.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index e36280a1541..4f8aca54d4b 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -429,9 +429,9 @@ void interval_domaint::assume_rec( } else if(cond.id()==ID_or) { - if(!negation) + if(negation) forall_operands(it, cond) - assume_rec(*it, false); + assume_rec(*it, true); } }