January 2009 - PPL-devel - BUGSENG Mailman

ppl ./NEWS ./README.configure ./configure.ac i ...
by Roberto Bagnara 24 Jan '09

24 Jan '09

1 0

ppl ./NEWS ./README.configure ./configure.ac i ...
by Roberto Bagnara 23 Jan '09

23 Jan '09

CVSROOT: /cvs/ppl Module name: ppl Changes by: bagnara(a)cs.unipr.it 2009-01-23 22:13:14 Modified files: . : NEWS README.configure configure.ac interfaces/OCaml: Makefile.am interfaces/OCaml/tests: Makefile.am Log message: New configuration option `--with-mlgmp=DIR' allows to specify the installation directory of the ML GMP package. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/NEWS.diff?cvsroot=ppl&r1=1.28… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/README.configure.diff?cvsroot… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/configure.ac.diff?cvsroot=ppl… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/interfaces/OCaml/Makefile.am.… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/interfaces/OCaml/tests/Makefi…

1 0

ppl/demos/ppl_lpsol ppl_lpsol.c
by Roberto Bagnara 23 Jan '09

23 Jan '09

CVSROOT: /cvs/ppl Module name: ppl Changes by: bagnara(a)cs.unipr.it 2009-01-23 13:30:55 Modified files: demos/ppl_lpsol: ppl_lpsol.c Log message: Added missing const qualifier. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/demos/ppl_lpsol/ppl_lpsol.c.d…

1 0

Problem installing ppl-0.9 in ubuntu 8.10 with ciao and swi prolog interfaces
by Miky Zamalloa 21 Jan '09

21 Jan '09

Hi, I have succesfully installed PPL v0.9 several times in my ubuntu system with interfaces to ciao_prolog and swi_prolog. Now, I have just re-installed ubuntu (version 8.10), and want to install PPL 0.9 again but this time I am getting the following problem: -------------------------------------------------------------------------- home-hp-root:/usr/local/src/ppl-0.9 [26]> ./configure --prefix=/usr/local --with-cflags=-I/home/mzamalloa/Systems/CiaoDE/ciao/include/LINUXi86/ --with-cxxflags=-I/home/mzamalloa/Systems/CiaoDE/ciao/include/LINUXi86/ --enable-interfaces=ciao_prolog,swi_prolog ... ... ... home-hp-root:/usr/local/src/ppl-0.9 [27]> make make all-recursive make[1]: Entering directory `/usr/local/src/ppl-0.9' Making all in utils make[2]: Entering directory `/usr/local/src/ppl-0.9/utils' if g++ -DHAVE_CONFIG_H -I. -I. -I.. -W -Wall -g -O2 -MT timings.o -MD -MP -MF ".deps/timings.Tpo" -c -o timings.o timings.cc; \ then mv -f ".deps/timings.Tpo" ".deps/timings.Po"; else rm -f ".deps/timings.Tpo"; exit 1; fi timings.cc: In function ‘void start_clock()’: timings.cc:53: error: ‘exit’ was not declared in this scope timings.cc: In function ‘void print_clock(std::ostream&)’: timings.cc:64: error: ‘exit’ was not declared in this scope make[2]: *** [timings.o] Error 1 make[2]: Leaving directory `/usr/local/src/ppl-0.9/utils' make[1]: *** [all-recursive] Error 1 make[1]: Leaving directory `/usr/local/src/ppl-0.9' make: *** [all] Error 2 home-hp-root:/usr/local/src/ppl-0.9 [28]> ------------------------------------------------------------------------ Any ideas? Thanks in advance! Miky Zamalloa

2 1

w3ppl/htdocs/MailingLists MailingLists.raw
by Roberto Bagnara 21 Jan '09

21 Jan '09

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: bagnara(a)cs.unipr.it 2009-01-21 10:54:17 Modified files: htdocs/MailingLists: MailingLists.raw Log message: Spurious semicolon removed. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/MailingLists/Mailing…

1 0

w3ppl/htdocs/MailingLists MailingLists.raw
by Roberto Bagnara 21 Jan '09

21 Jan '09

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: bagnara(a)cs.unipr.it 2009-01-21 10:51:44 Modified files: htdocs/MailingLists: MailingLists.raw Log message: Tried to make it clear that, while everyone is welcome to subscribe our mailing lists, subscription is not necessary to post a message. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/MailingLists/Mailing…

1 0

ppl/interfaces/OCaml Makefile.am
by Enea Zaffanella 21 Jan '09

21 Jan '09

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2009-01-21 09:36:24 Modified files: interfaces/OCaml: Makefile.am Log message: Corrected so as to behave correctly when using parallel builds: the build of <file>.cmx also generates <file>.o, which is a dependency for the generation of *.a. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/interfaces/OCaml/Makefile.am.…

1 0

Re: [PPL-devel] [Fwd: Fwd: Info on PPL]
by Giorgio 21 Jan '09

21 Jan '09

Enea, thanks a lot for the prompt reply. > Giorgio Delzanno wrote: > > Enea, > > together with Ahmed Rezine (in cc) we'd like to use PPL for defining a > > sort of "extrapolation" method > > (to be applied as a subroutine of a verification process). > > To give you an example, suppose we compute (forward) a sequence of > > tuples of values > > (valuation of variables) like (0,0) (1,1) (2,2)... > > From this we would like to "extrapolate" the constraint X=Y without > > fixing in advance the > > shape of equations (e.g. Y=MX+Q) we have to consider. > > > > Is there some kind of acceleration/widening that can be applied in this > > case? > > Thanks in advance, > > Giorgio > > ps: ... eventually, we started using PPL :> > > > > > > Giorgio, > > the simple case above can be modeled using several (weakly) relational > abstract domains, such as polyhedra, octagonal shapes and BD shapes, and > probably using several variations of the standard widening of Cousot and > Halbwachs. > > Practically, suppose that you choose topologically closed polyhedra > (i.e., class C_Polyhedron in the C++ interface of the PPL), using the > standard widening (i.e., method H79_widening_assign in the C++ interface > of the PPL). Let P_0, P_1, ..., P_i, ... be the sequence of polyhedra, > where each P_i is a 2-dim polyhedron defined by the constraints > { x = i, y = i }. > Then, you will end up computing the sequence of Q_i where > > Q_0 := P_0 = { x = 0, y = 0 }; > > Q_1 := hull_1.H79_widening_assign(Q_0) = { x = y, y >= 0 }, > where > hull_1 := the poly-hull of P_1 and Q_0 > = { x = y, 0 <= y <= 1 } > > Q_2 := hull_2.H79_widening_assign(Q_1) = Q_1 (fixpoint) > where > hull_2 := the poly-hull of P_2 and Q_1 > = { x = y, 0 <= y <= 2 } > > Hope this is what you really meant. > Ok. Is this the same as CH78 widening (based on constraint deletion)? We tried CC76_extrapolation on BDS but we probably forgot to compute the union. To have a similar results for BDS, would it be correct to use something like bds1= x=0,y=0 bds2= x=1,y=1 bds2=upper_bound_assign(bds1); // smallest bds union of bds1 and bds2 bd2=bds2.H79_widening_assign(bds1); (I am writing from home and cannot test it right now). Thanks, Giorgio & Ahmed

2 1

w3ppl/htdocs/Links Links.raw
by Roberto Bagnara 21 Jan '09

21 Jan '09

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: bagnara(a)cs.unipr.it 2009-01-21 08:46:39 Modified files: htdocs/Links : Links.raw Log message: Added links to "Git from the bottom up", by John Wiegley, and "Git for Computer Scientists", by Tommi Virtanen. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Links/Links.raw.diff…

1 0

w3ppl/htdocs/Documentation ppl_citations.bib
by Roberto Bagnara 20 Jan '09

20 Jan '09

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: bagnara(a)cs.unipr.it 2009-01-20 21:30:17 Modified files: htdocs/Documentation: ppl_citations.bib Log message: Entries reordered. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Documentation/ppl_ci…

1 0