August 2011 - PPL-devel - BUGSENG Mailman

[doko@debian.org: Bug#625417: ppl: ftbfs with gcc-4.6 -Werror]
by Michael Tautschnig 08 Nov '11

08 Nov '11

Hi all, As you might have heard already, GCC 4.6 introduced a number of new warnings. As we build the package for Debian with -Werror turned on, these would cause build failures. If you agree that these warnings should be addressed, it would be nice if you could fix them upstream. Otherwise I will introduce Debian-specific patches to work around them. The best way to find all of them is take a look at the build log at http://people.debian.org/~doko/tmp/werror/ppl_0.11.2-3_lsid64.buildlog and search for -Wunused. Many of the warnings relate to ppl.hh, hence are easily fixed by changing the code it is generated from. Only a few others concern the tests. Thanks a lot, Michael PS.: If someone could afterwards tell me about the git commit ids that would makes things even easier :-) ----- Forwarded message from Matthias Klose <doko(a)debian.org> ----- Date: Tue, 03 May 2011 10:34:10 +0000 From: Matthias Klose <doko(a)debian.org> To: maintonly(a)bugs.debian.org Subject: Bug#625417: ppl: ftbfs with gcc-4.6 -Werror Reply-To: Matthias Klose <doko(a)debian.org>, 625417-maintonly(a)bugs.debian.org Package: ppl Version: 0.11.2-3 Severity: important Tags: wheezy sid User: debian-gcc(a)lists.debian.org Usertags: ftbfs-gcc-4.6 ftbfs-werror This package builds with -Werror, and GCC 4.6 triggers new warnings which will make the package fail to build. Currently a Debian patch just passes -Wno-error=unused-but-set-variable and -Wno-error=unused-but-set-parameter to avoid build failures, but this patch will be reverted with the GCC 4.6.1 release, and the severity of the report will be raised. The full build log can be found at: http://people.debian.org/~doko/tmp/werror/ppl_0.11.2-3_lsid64.buildlog The last lines of the build log are at the end of this report. ----- End forwarded message -----

2 1

PPL installation problems
by Adrien Champion 08 Nov '11

08 Nov '11

Hello, A few months ago, I managed to install and use PPL on my main computer, but now that I am trying to install it on my notebook I encounter problems. I should probably start by saying that the part I am interested in is the Java interface. The configure, make and make install work but when I try to run make for the java interface I get the following error: /bin/bash: no: command not found make[1]: *** [java_classes.stamp] Error 127 When looking closer however, the configure does not really work since it does not find all the java related commands: checking for javac... no checking for java... no checking for jar... no checking for javah... no configure: WARNING: unable to include <jni.h> Do you happen to have any solution for this problem ? Thank you in advance. Best, -- Adrien Champion PhD student Onera / Rockwell Collins France adrien.champion(a)onera.fr Onera: +33 (0)5 62 25 26 54 RCF: +33 (0)5 61 71 77 00

3 2

Re: [PPL-devel] Can't find GMP, but it's installed
by Roberto Bagnara 07 Nov '11

07 Nov '11

On 05/11/11 14:18, rafael ff1 wrote: > 2011/5/11 Roberto Bagnara<bagnara(a)cs.unipr.it>: >> >> What is the contents of the `config.log' file generated by the >> `configure' script? >> Cheers, >> >> Roberto >> >> -- >> Prof. Roberto Bagnara >> Applied Formal Methods Laboratory >> Department of Mathematics, University of Parma, Italy >> http://www.cs.unipr.it/~bagnara/ >> mailto:bagnara@cs.unipr.it >> _______________________________________________ >> PPL-devel mailing list >> PPL-devel(a)cs.unipr.it >> http://www.cs.unipr.it/mailman/listinfo/ppl-devel >> > > I'm sending as attachment a config.log for the aforementioned > configure script and another one with ld library path forced. Please > let me know if you don't receive it - some mail lists block > attachments... > > Rafael Hi Rafael, the config.log you sent does not seem to match the file fail-build.log you sent earlier. The latter says: checking how to link with libgmp... /usr/lib32/libgmp.so -Wl,-rpath -Wl,/usr/lib32 checking how to link with libgmpxx... /usr/lib32/libgmpxx.so /usr/lib32/libgmp.so -Wl,-rpath -Wl,/usr/lib32 -Wl,-rpath -Wl,/usr/lib32 which looks correct to me. The former says: configure:10129: checking how to link with libgmp configure:10602: result: /usr/lib/libgmp.so configure:10644: checking how to link with libgmpxx configure:11117: result: /usr/lib/libgmpxx.so /usr/lib/libgmp.so which is very different and very wrong, since it is because of that that later we have: configure:11252: g++ -m32 -o conftest -g -O2 -frounding-math -march=x86-64 -mtune=generic -O2 -pipe -Wl,--hash-style=gnu -Wl,--as-needed conftest.cpp /usr/lib/libgmpxx.so /usr/lib/libgmp.so >&5 /usr/lib/libgmpxx.so: could not read symbols: File in wrong format collect2: ld returned 1 exit status This is caused by the fact that g++ is given the x86_64 version of GMP. Please direct all messages to ppl-devel(a)cs.unipr.it. Cheers, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

3 4

[GIT] ppl/ppl(bounded_arithmetic): Minor changes to the code.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 20d6899edb2b8be27a6f04e7ddacd37d6b4df964 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=20d6899edb2b… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 18:12:17 2011 +0200 Minor changes to the code. --- tests/Concrete_Expression/linearize_int.cc | 83 ++++++++++++++-------------- 1 files changed, 42 insertions(+), 41 deletions(-) diff --git a/tests/Concrete_Expression/linearize_int.cc b/tests/Concrete_Expression/linearize_int.cc index 6bf18cc..2b0c1ad 100644 --- a/tests/Concrete_Expression/linearize_int.cc +++ b/tests/Concrete_Expression/linearize_int.cc @@ -135,13 +135,6 @@ test01(){ known_result_lshift = known_result_or; known_result_rshift = known_result_or; - linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), result_or); - nout << "*** " << known_result_or << " | " << lf << " ***" << endl - << "*** result_or *** " << endl - << result_or << endl; - known_result_or |= lf; - nout << endl; - linearize_int(band, oracle, Integer_Linear_Form_Abstract_Store(), result_and); nout << "*** " << known_result_and << " & " << lf << " ***" << endl << "*** result_and *** " << endl @@ -149,6 +142,13 @@ test01(){ known_result_and &= lf; nout << endl; + linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), result_or); + nout << "*** " << known_result_or << " | " << lf << " ***" << endl + << "*** result_or *** " << endl + << result_or << endl; + known_result_or |= lf; + nout << endl; + linearize_int(bxor, oracle, Integer_Linear_Form_Abstract_Store(), result_xor); nout << "*** " << known_result_xor << " ^ " << lf << " ***" << endl << "*** result_xor *** " << endl @@ -175,10 +175,10 @@ test01(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -312,9 +312,9 @@ test02(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) + && + (result_or == known_result_or) && (result_xor == known_result_xor) && @@ -457,10 +457,10 @@ test03(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -593,10 +593,10 @@ test04(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -740,10 +740,10 @@ test05(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -832,10 +832,10 @@ test06(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -896,20 +896,23 @@ test07(){ bool failed_or = false; bool failed_xor = false; - if (!linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), - result_or)) { + nout << "*** " << known_result_and << " << " << lf << " ***" << endl; + if (!linearize_int(band, oracle, Integer_Linear_Form_Abstract_Store(), + result_and)) { nout << "*** Linearization failed, the two linear forms have " << "different size *** " << endl << endl; - failed_or = true; + failed_and = true; } - if (!linearize_int(band, oracle, Integer_Linear_Form_Abstract_Store(), - result_and)) { + nout << "*** " << known_result_or << " << " << lf << " ***" << endl; + if (!linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), + result_or)) { nout << "*** Linearization failed, the two linear forms have " << "different size *** " << endl << endl; - failed_and = true; + failed_or = true; } + nout << "*** " << known_result_xor << " << " << lf << " ***" << endl; if (!linearize_int(bxor, oracle, Integer_Linear_Form_Abstract_Store(), result_xor)) { nout << "*** Linearization failed, the two linear forms have " @@ -934,10 +937,10 @@ test07(){ nout << endl; bool ok = - (failed_or) - && (failed_and) && + (failed_or) + && (failed_xor) && (result_lshift == known_result_lshift) @@ -1017,13 +1020,6 @@ test08(){ known_result_lshift = known_result_or; known_result_rshift = known_result_or; - linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), result_or); - nout << "*** " << known_result_or << " | " << lf << " ***" << endl - << "*** result_or *** " << endl - << result_or << endl; - known_result_or |= lf; - nout << endl; - linearize_int(band, oracle, Integer_Linear_Form_Abstract_Store(), result_and); nout << "*** " << known_result_and << " & " << lf << " ***" << endl << "*** result_and *** " << endl @@ -1031,6 +1027,13 @@ test08(){ known_result_and &= lf; nout << endl; + linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), result_or); + nout << "*** " << known_result_or << " | " << lf << " ***" << endl + << "*** result_or *** " << endl + << result_or << endl; + known_result_or |= lf; + nout << endl; + linearize_int(bxor, oracle, Integer_Linear_Form_Abstract_Store(), result_xor); nout << "*** " << known_result_xor << " ^ " << lf << " ***" << endl << "*** result_xor *** " << endl @@ -1058,10 +1061,10 @@ test08(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -1168,6 +1171,7 @@ test09(){ known_result_xor = known_result_and; known_result_lshift = known_result_and; known_result_rshift = known_result_and; + linearize_int(band, oracle, Integer_Linear_Form_Abstract_Store(), result_and); nout << "*** " << known_result_and << " & " << lf << " ***" << endl << "*** result_and *** " << endl @@ -1189,9 +1193,6 @@ test09(){ known_result_xor ^= lf; nout << endl; - // b1 *= tmp1; - //inh_term1 += b1; - bool failed_lshift = false; bool failed_rshift = false; @@ -1212,10 +1213,10 @@ test09(){ } bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && failed_lshift

1 0

[GIT] ppl/ppl(bounded_arithmetic): Added to the bitwise functions, a check for the existence of the infinite.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 91d973104574475fec53561a5d8dfc0e901050b8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=91d973104574… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 18:09:12 2011 +0200 Added to the bitwise functions, a check for the existence of the infinite. --- src/Interval.inlines.hh | 38 ++++++++++++++++++++++++++++++++++++++ 1 files changed, 38 insertions(+), 0 deletions(-) diff --git a/src/Interval.inlines.hh b/src/Interval.inlines.hh index 54d7231..fa70325 100644 --- a/src/Interval.inlines.hh +++ b/src/Interval.inlines.hh @@ -1089,6 +1089,16 @@ Interval<To_Boundary, To_Info>::and_assign(const From1& x, const From2& y) { if (check_empty_arg(x) || check_empty_arg(y)) return assign(EMPTY); + int inf = Parma_Polyhedra_Library::is_infinity(x); + if (inf) { + if (Parma_Polyhedra_Library::is_infinity(y) == -inf) + return assign(NOT_A_NUMBER); + } + else + inf = Parma_Polyhedra_Library::is_infinity(y); + if (inf) + return assign(NOT_A_NUMBER); + Interval<To_Boundary, To_Info> x1; Interval<To_Boundary, To_Info> x2; Interval<To_Boundary, To_Info> zero(0); @@ -1184,6 +1194,16 @@ Interval<To_Boundary, To_Info>::or_assign(const From1& x, const From2& y) { if (check_empty_arg(x) || check_empty_arg(y)) return assign(EMPTY); + int inf = Parma_Polyhedra_Library::is_infinity(x); + if (inf) { + if (Parma_Polyhedra_Library::is_infinity(y) == -inf) + return assign(NOT_A_NUMBER); + } + else + inf = Parma_Polyhedra_Library::is_infinity(y); + if (inf) + return assign(NOT_A_NUMBER); + Interval<To_Boundary, To_Info> x1; Interval<To_Boundary, To_Info> x2; Interval<To_Boundary, To_Info> neg_one(-1); @@ -1280,6 +1300,16 @@ Interval<To_Boundary, To_Info>::xor_assign(const From1& x, const From2& y) { if (check_empty_arg(x) || check_empty_arg(y)) return assign(EMPTY); + int inf = Parma_Polyhedra_Library::is_infinity(x); + if (inf) { + if (Parma_Polyhedra_Library::is_infinity(y) == -inf) + return assign(NOT_A_NUMBER); + } + else + inf = Parma_Polyhedra_Library::is_infinity(y); + if (inf) + return assign(NOT_A_NUMBER); + Interval<To_Boundary, To_Info> x1; Interval<To_Boundary, To_Info> zero(0); Interval<To_Boundary, To_Info> neg_one(-1); @@ -1378,6 +1408,10 @@ Interval<To_Boundary, To_Info>::lshift_assign(const From1& x, const From2& y) { if (check_empty_arg(x) || check_empty_arg(y)) return assign(EMPTY); + int inf = Parma_Polyhedra_Library::is_infinity(x); + if (inf) + return assign(NOT_A_NUMBER); + Interval<To_Boundary, To_Info> x1; Interval<To_Boundary, To_Info> z; Interval<To_Boundary, To_Info> @@ -1459,6 +1493,10 @@ Interval<To_Boundary, To_Info>::rshift_assign(const From1& x, const From2& y) { if (check_empty_arg(x) || check_empty_arg(y)) return assign(EMPTY); + int inf = Parma_Polyhedra_Library::is_infinity(x); + if (inf) + return assign(NOT_A_NUMBER); + Interval<To_Boundary, To_Info> x1; Interval<To_Boundary, To_Info> z; Interval<To_Boundary, To_Info>

1 0

[GIT] ppl/ppl(bounded_arithmetic): Minor changes to the code.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 25b80bc7ca0e0e921fcbb502a23bfbc0a70a3e91 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=25b80bc7ca0e… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 17:34:01 2011 +0200 Minor changes to the code. --- tests/Concrete_Expression/linearize_int.cc | 272 ++++++++++++++++------------ 1 files changed, 157 insertions(+), 115 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=25b80bc7…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Changed the documentation of the functions bitwise.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: aaca7bfedc40309394045897d3d7513a6db5e6c9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=aaca7bfedc40… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 17:32:06 2011 +0200 Changed the documentation of the functions bitwise. --- src/linearize_integer.hh | 331 ++++++++-------------------------------------- 1 files changed, 56 insertions(+), 275 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=aaca7bfe…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Small changes in the definition of functions and two additional functions: bool check_totaly which returns true only if
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 1aeb2d0117f75efed305c80a6598e49e1e869df7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1aeb2d0117f7… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 17:27:56 2011 +0200 Small changes in the definition of functions and two additional functions: bool check_totaly which returns true only if the linear forms are totally greater than or equal to zero or less than zero, and function bool incomplete which returns true if the two linear form have coefficients associated with the same variables, different from zero. --- src/Linear_Form.defs.hh | 22 ++- src/Linear_Form.templates.hh | 450 ++++++++---------------------------------- 2 files changed, 101 insertions(+), 371 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=1aeb2d01…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Modified declaration and implementation of bitwise operator on intervals.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 5f6685859cdee87fa71b14c1cc8d8a27b03fce25 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5f6685859cde… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 17:16:05 2011 +0200 Modified declaration and implementation of bitwise operator on intervals. --- src/Interval.defs.hh | 89 ++- src/Interval.inlines.hh | 1437 +++++++++++++++++------------------------------ 2 files changed, 584 insertions(+), 942 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=5f668585…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Adjusted documentation about bitwise operator.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 0663324f51238dc36d88909734de6e7063ba4b73 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0663324f5123… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 17:12:43 2011 +0200 Adjusted documentation about bitwise operator. --- doc/definitions.dox | 92 ++++++++++++++++++++++++-------------------------- 1 files changed, 44 insertions(+), 48 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index ba80d9f..e48e010 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2821,9 +2821,10 @@ The interval bitwise operators are defined as follow: \begin{cases} \bigl[0, \min(b, b')\bigr], & \text{if $a \geq 0$ and $a' \geq 0$}; \\ - \bigl[0, \max(b, b')\bigr], - & \text{if $a \geq 0$ and $b' < 0$, - or $b < 0$ and $a' \geq 0$}; \\ + \bigl[0, b\bigr], + & \text{if $a \geq 0$ and $b' < 0$}; \\ + \bigl[0, b'\bigr], + & \text{if $b < 0$ and $a' \geq 0$}; \\ \bigl[a + a', \min(b,b')\bigr], & \text{if $b < 0$ and $b' < 0$}. \\ \end{cases} @@ -2834,9 +2835,10 @@ The interval bitwise operators are defined as follow: \begin{cases} \bigl[\max(a,a'), b + b'\bigr], & \text{if $a \geq 0$ and $a' \geq 0$}; \\ - \bigl[\min(a,a'),-1\bigr], - & \text{if $a \geq 0$ and $b' < 0$, - or $b < 0$ and $a' \geq 0$}; \\ + \bigl[a',-1\bigr], + & \text{if $a \geq 0$ and $b' < 0$}; \\ + \bigl[a,-1\bigr], + & \text{if $b < 0$ and $a' \geq 0$}; \\ \bigl[\max(a,a'),-1\bigr], & \text{if $b < 0$ and $b' < 0$}. \\ \end{cases} @@ -2845,25 +2847,31 @@ The interval bitwise operators are defined as follow: \f[ [a,b] \bxorii [a',b'] \approx \begin{cases} - \bigl[0,|b + b'|\bigr], - & \text{if $a \geq 0$ and $a' \geq 0$, - or $b < 0$ and $b' < 0$}; \\ - \bigl[-(|a| + |a'|),-1\bigr], - & \text{if $a \geq 0$ and $b' < 0$, - or $b < 0$ and $a' \geq 0$}. \\ + \bigl[0,b + b'\bigr], + & \text{if $a \geq 0$ and $a' \geq 0$}; \\ + \bigl[(-a + a'),-1\bigr], + & \text{if $a \geq 0$ and $b' < 0$}; \\ + \bigl[(a - a'),-1\bigr], + & \text{if $b < 0$ and $a' \geq 0$}; \\ + \bigl[0, |b + b'|\bigr], + & \text{if $b < 0$ and $b' < 0$}. \\ \end{cases} \f] \f[ [a,b] \olessthan ^{\#} [a',b'] \approx \begin{cases} - \bigl[0, \bigl(b \times 2^{b'}\bigr)\bigr], + \bigl[\bigl(a \times 2^{a'}\bigr), + \bigl(b \times 2^{b'}\bigr)\bigr], & \text{if $a \geq 0$ and $a' \geq 0$}; \\ - \bigl[0, \bigl(b / 2^{\left|b'\right|}\bigr)\bigr], + \bigl[\bigl(a / 2^{\left|a'\right|}\bigr, + \bigl(b / 2^{\left|b'\right|}\bigr)\bigr], & \text{if $a \geq 0$ and $b' < 0$}; \\ - \bigl[\bigl(a \times 2^{a'}\bigr), 0\bigr], + \bigl[\bigl(a \times 2^{a'}\bigr), + \bigl(b \times 2^{b'}\bigr)\bigr], & \text{if $b < 0$ and $a' \geq 0$}; \\ - \bigl[\bigl(a / 2^{\left|a'\right|}\bigr), 0\bigr], + \bigl[\bigl(a / 2^{\left|a'\right|}\bigr), + \bigl(b / 2^{\left|b'\right|}\bigr)\bigr], & \text{if $b < 0$ and $b' < 0$}. \\ \end{cases} \f] @@ -2871,13 +2879,17 @@ The interval bitwise operators are defined as follow: \f[ [a,b] \ogreaterthan ^{\#} [a',b'] \approx \begin{cases} - \bigl[0, \bigl(b / 2^{b'}\bigr)\bigr], + \bigl[\bigl(a / 2^{a'}\bigr), + \bigl(b / 2^{b'}\bigr)\bigr], & \text{if $a \geq 0$ and $a' \geq 0$}; \\ - \bigl[0, \bigl(b \times 2^{\left|b'\right|}\bigr)\bigr], + \bigl[\bigl(a \times 2^{\left|a'\right|}\bigr), + \bigl(b \times 2^{\left|b'\right|}\bigr)\bigr], & \text{if $a \geq 0$ and $b' < 0$}; \\ - \bigl[\bigl(a / 2^{a'}\bigr), 0\bigr], + \bigl[\bigl(a / 2^{a'}\bigr), + \bigl(b / 2^{b'}\bigr)\bigr], & \text{if $b < 0$ and $a' \geq 0$}; \\ - \bigl[\bigl(a \times 2^{\left|a'\right|}\bigr), 0\bigr], + \bigl[\bigl(a \times 2^{\left|a'\right|}\bigr), + \bigl(b \times 2^{\left|b'\right|}\bigr)\bigr], & \text{if $b < 0$ and $b' < 0$}. \\ \end{cases} @@ -3060,10 +3072,8 @@ both greater than or equal zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ - 0 - \leq \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \amlf 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} @@ -3074,10 +3084,8 @@ have discordand signs, with the first greater than or equal zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ - 0 - \leq \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \adivlf 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} @@ -3088,26 +3096,22 @@ have discordand signs, with the first less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ + \left(k + \sum_{v \in \cV}k_{v}v \right) + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \amlf 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} - \leq - \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq - 0 \f] Finally, if \f$i + \sum_{v \in V}i_{v}v\f$ and \f$i' + \sum_{v \in V}i'_{v}v\f$ are both less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ + \left(k + \sum_{v \in \cV}k_{v}v \right) + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \adivlf 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} - \leq - \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq - 0 \f] \subsubsection bitwise_right_shift Bitwise RIGHT SHIFT @@ -3125,10 +3129,8 @@ both greater than or equal zero then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ - 0 - \leq \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \adivlf 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} @@ -3139,10 +3141,8 @@ have discordand signs, with the first greater than or equal zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ - 0 - \leq \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \amlf 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} @@ -3153,26 +3153,22 @@ have discordand signs, with the first less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ + \left(k + \sum_{v \in \cV}k_{v}v \right) + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \adivlf 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} - \leq - \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq - 0 \f] Finally, if \f$i + \sum_{v \in V}i_{v}v\f$ and \f$i' + \sum_{v \in V}i'_{v}v\f$ are both less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ + \left(k + \sum_{v \in \cV}k_{v}v \right) + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \amlf 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} - \leq - \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq - 0 \f] Where \f$\asifp, \adifp, \amifp,\f$ and \f$\adivifp\f$ are the corresponding

1 0