December 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Removed redundant code.
by Roberto Amadini 07 Dec '09

07 Dec '09

Module: ppl/ppl Branch: floating_point Commit: 307af1367ed63e9492beec84f4949f365e8078ba URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=307af1367ed6… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Dec 7 18:41:03 2009 +0100 Removed redundant code. --- tests/Floating_Point_Expression/Makefile.am | 5 +- tests/Floating_Point_Expression/digitalfilters1.cc | 13 -- tests/Floating_Point_Expression/ratelimiter.cc | 197 -------------------- 3 files changed, 1 insertions(+), 214 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=307af136…

1 0

[GIT] ppl/ppl(floating_point): Fixed comments.
by Roberto Amadini 02 Dec '09

02 Dec '09

Module: ppl/ppl Branch: floating_point Commit: 96ac4ea63bf306c669e97a6abc58281be0647cb9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=96ac4ea63bf3… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Wed Dec 2 23:43:32 2009 +0100 Fixed comments. --- tests/Floating_Point_Expression/digitalfilters1.cc | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 205c23d..bcadc9e 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -473,7 +473,7 @@ test05() { assign_r(M, max_analyzer, ROUND_DOWN); // We have to check that Y not overflows. - // FIXME: We could take any value of M >= 145. + // FIXME: We could take any value of M >= 144. Constraint_System cs; cs.insert(Y <= M); cs.insert(Y >= -M); @@ -665,7 +665,7 @@ test06() { // Y + Y <= 2 * M = +inf and -Y - Y <= -2 * M = +inf. // For a more precise analysis, it is better to insert the // constraints Y <= N and Y >= -N, where N = M / 2. - // However, we could take any value of N such that 145 <= N <= M / 2. + // However, we could take any value of N such that 144 <= N <= M / 2. div_2exp_assign_r(N, M, 1, ROUND_DOWN); // We have to check that Y not overflows. Constraint_System cs; @@ -855,7 +855,7 @@ test07() { assign_r(M, max_analyzer, ROUND_DOWN); // We have to check that Y not overflows. - // FIXME: We could take any value of M >= 145. + // FIXME: We could take any value of M >= 144. Constraint_System cs; cs.insert(Y <= M); cs.insert(Y >= -M);

1 0

[GIT] ppl/w3ppl(master): Link to Julia updated.
by Roberto Bagnara 02 Dec '09

02 Dec '09

Module: ppl/w3ppl Branch: master Commit: 1f70ebed7d07fc173be00988f77af3d296257071 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=1f70ebed7d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Dec 2 18:57:39 2009 +0100 Link to Julia updated. --- htdocs/Applications/Applications.raw | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/htdocs/Applications/Applications.raw b/htdocs/Applications/Applications.raw index 93eda5a..490fd08 100644 --- a/htdocs/Applications/Applications.raw +++ b/htdocs/Applications/Applications.raw @@ -18,7 +18,7 @@ Here are the ones we are aware of. </LI> <P> <LI> - <A HREF="http://spy.sci.univr.it/JuliaWeb/">Julia</A>: + <A HREF="http://julia.scienze.univr.it/">Julia</A>: a generic static analyser for full sequential Java bytecode. Julia is written in Java and accesses the PPL via its Java interface. </LI>

1 0

[GIT] ppl/w3ppl(master): Added a link to Fortuna, a model checker for priced probabilistic timed automata.
by Roberto Bagnara 02 Dec '09

02 Dec '09

Module: ppl/w3ppl Branch: master Commit: 2a7eb04eb7158c9a06469fde3dda1f8829717670 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=2a7eb04eb7… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Dec 2 18:55:37 2009 +0100 Added a link to Fortuna, a model checker for priced probabilistic timed automata. --- htdocs/Applications/Applications.raw | 6 ++++++ 1 files changed, 6 insertions(+), 0 deletions(-) diff --git a/htdocs/Applications/Applications.raw b/htdocs/Applications/Applications.raw index db120d1..93eda5a 100644 --- a/htdocs/Applications/Applications.raw +++ b/htdocs/Applications/Applications.raw @@ -24,6 +24,12 @@ Here are the ones we are aware of. </LI> <P> <LI> + <A HREF="http://www.cs.ru.nl/~jasperb/fortuna/">Fortuna</A> + is a model checker for priced probabilistic timed automata. + It heavily uses the Parma Polyhedra Library. + </LI> +<P> + <LI> <A HREF="http://gcc.gnu.org/wiki/MiddleEndLispTranslator">MELT</A> (Middle End Lisp Translator), an experimental branch of <A HREF="http://gcc.gnu.org/">GCC</A> (the GNU Compiler

1 0