[PPL-devel] Re: Source Code

[Roberto Bagnara]

Sriram Sankaranarayanan wrote:
> The new tarball is attached. I could have generated a patch, 
>  but this is easier
> 
> 
>  Just to make sure.. Here are the versions of things I am using
> 
> srirams at Dali:~% g++ --version
> 
> g++ (GCC) 3.2.2 20030222 (Red Hat Linux 3.2.2-5)
> Copyright (C) 2002 Free Software Foundation, Inc.
> 
> 
> srirams at Dali:~% flex --version
> flex version 2.5.4
> 
> srirams at Dali:~% ~/bin/bison --version
> bison (GNU Bison) 1.875c
> Written by Robert Corbett and Richard Stallman.

I am using GCC 3.4.2, Bison 1.875d, and Flex 2.5.4.
There is only one problem in the sources you sent:

MatrixStore.cc:14: error: array bound forbidden after parenthesized type-id
MatrixStore.cc:14: note: try removing the parentheses around the type-id

This can be easily fixed by changing the guilty line to

    mat= new Rational*[n]; // the last column is the $b$ augment

> I tried it with your latest ppl bug fix, it works. Thanks for fixing that.

Thanks to you for your report!

> I have packaged the examples in with the src under lsting-src/Examples
> 
> If you run 
> 
> lsting invcheck < inputfile
> 
> it will print a message prefixed by the word ERROR 
> on the stderr stream if something breaks (i.e, the computed
> invariant fails the inductive check.. which is finally all 
> we care about :-)

Hey, but you proved it correct, didn't you?  :-)

> I hope this works without further troubles.

It seems it does.  We will use your program regularly
for regression testing.  Thanks!
All the best,

     Roberto

-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it