[PPL-devel] PPL: Problem with Checked-Ints

[Didier Lime]

Dear PPL developer,

I am currently using the PPL to do some formal verification on Time  
Petri Nets. You might be interested in knowing that the next release  
of Romeo (http://romeo.rts-software.org/) should rely on it for all  
its "hybrid" computations.

Anyway, I have a strange "positive overflow" with the code below. The  
complete error message reads:
$ ./test_ppl
terminate called after throwing an instance of 'std::overflow_error'
   what():  Positive overflow.
Abort trap

Info that should be useful:
- I run this code on an Apple MacBook Pro with an Intel Core 2 Duo  
processor
- I compiled the PPL seamlessly with options --enabled- 
optimization=speed and --enable-coefficients=checked-int32
- g++ --version  reads: i686-apple-darwin8-g++-4.0.1 (GCC) 4.0.1  
(Apple Computer, Inc. build 5367)

My sample code :
#include <iostream>
using namespace std;

#include <ppl.hh>
using namespace PPL;
using namespace PPL::IO_Operators;

int main()
{
     NNC_Polyhedron P(2);
     Variable A(0);
     Variable B(1);

     P.add_constraint(B == 46342);
     P.add_constraint(A >= 0);
     P.add_constraint(A <= 1);

     Linear_Expression expr = B - A;
     P.affine_image(B, expr);

     cout << P << endl;

     return 0;
}

I compile it with g++ -o test_ppl test_ppl.cc -lppl -lgmp and get the  
above exception when executing it.

Now, if I compile the PPL with --enable-coefficients=native-int32, it  
just runs fine and gives the intended result:
A + B = 46342, -A >= -1

Also it runs fine with checked ints and B being below or equal to 46341.

I hope it is not just a misuse from me... Please ask if you need some  
more information.

Best wishes,

Didier


--
Dr. Didier Lime
Maître de Conférences
IRCCyN / École Centrale de Nantes
Nantes, France

http://www.irccyn.ec-nantes.fr/~lime