[PPL-devel] ppl test failures on mac

[Roberto Bagnara]

On 10/06/12 03:24, Mark A. McLaughlin wrote:
> make  check-TESTS
> PASS: C_Expr
> PASS: linearform1
> PASS: linearize
> PASS: digitalfilters1
> PASS: bdshape1
> PASS: bdshape2
> PASS: octagonalshape1
> PASS: octagonalshape2
> tests failed: test04 test05
> FAIL: polyhedron1
> tests failed: test04 test05
> FAIL: polyhedron2
> ======================================
> 2 of 10 tests failed
> Please report to ppl-devel at cs.unipr.it <mailto:ppl-devel at cs.unipr.it>
> ======================================
>
> I just download, configured, compiled, and tested ppl-1.0. Two of
> the tests failed (as listed above). The messages states that I
> should report this.

Hello Mark.

Thanks for the report.  I believe this is due to the fact that
LLVM does not provide support for the -frounding-math option,
and this may result into incorrectness of the floating-point
based domains.  Moreover, llvm-gcc masquerades as gcc, which
defeats our configure script.

If you use the domains that are based on floating-point numbers,
then only solution is to use GCC (the real thing) instead of LLVM.
Please do not hesitate to ask if you need help.
Kind regards,

    Roberto

-- 
      Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                               BUGSENG srl - http://bugseng.com
                               mailto:roberto.bagnara at bugseng.com