[Bug 529404] Review Request: cvc3 - Validity checker of many-sorted first-order formulas with theories

[bugzilla at redhat.com]

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug.


https://bugzilla.redhat.com/show_bug.cgi?id=529404





--- Comment #2 from David A. Wheeler <dwheeler at dwheeler.com>  2009-10-16 17:01:57 EDT ---
I just built the package; I have an rpmlint error, as well as several warnings.
 I think you HAVE to fix the rpmlint error, at least.  So, here's what I've
found so far in my review:

An "rpmlint cvc3.spec" works just fine:
0 packages and 1 specfiles checked; 0 errors, 0 warnings.

But when I built in on a 32-bit "i586" system and did rpmlint, I got this:
$ rpmlint ../RPMS/i586/cvc3-*.rpm ../SRPMS/cvc3-2.1-1.fc11.src.rpm 
cvc3.i586: W: unstripped-binary-or-object /usr/lib/libcvc3.so.1.0.0
cvc3.i586: W: shared-lib-calls-exit /usr/lib/libcvc3.so.1.0.0 exit at GLIBC_2.0
cvc3.i586: W: shared-lib-calls-exit /usr/lib/libcvc3.so.1.0.0 exit@@GLIBC_2.0
cvc3-devel.i586: E: zero-length
/usr/share/doc/cvc3-devel-2.1/html/classHash_1_1hash__table__inherit__graph.png
cvc3-emacs.i586: W: no-documentation
cvc3-emacs-el.i586: W: no-documentation
cvc3-xemacs.i586: W: no-documentation
cvc3-xemacs-el.i586: W: no-documentation
8 packages and 0 specfiles checked; 1 errors, 7 warnings.

The error is "zero-length
/usr/share/doc/cvc3-devel-2.1/html/classHash_1_1hash__table__inherit__graph.png".
 This is merely in a missing figure in the *documentation*, not in the
executing program, so it's not a crisis.  It'd be nice if you could make sure
it generates into a real graph, but if that fails, you should "remove this file
if length is zero" since it's not supposed to have rpmlint errors.

The "unstripped-binary-or-object" warning is odd; shouldn't that info have been
moved into "cvc3-debuginfo"?

The rest are probably non-events.  The 4 'no-documentation' warnings are
probably irrelevant, since the documentation presumably was put in the
"cvc3-doc" package.  I don't have a problem with shared libraries calling exit,
unless users were expecting something else, so I don't think that's an issue
either.

I noticed some warnings during compilation, though that's depressingly common
nowadays.  When running doxygen, I noticed these:
 Generating docs for page INSTALL...
 /home/dwheeler/rpmbuild/BUILD/cvc3-2.1/INSTALL:198: Error: Unexpected
character `"'
 ...
 Generating dependency graph for group ExprPkg
 /home/dwheeler/rpmbuild/BUILD/cvc3-2.1/src/include/expr.h:392: Error:
Unexpected character `"'

I'm wondering if these expressions are causing it trouble:
 "debug)
 contains the condition "f"

Also, there's are 'useless rule' warnings from bison:
 bison -d -y -o parsesmtlib.cpp -p smtlib --debug -v smtlib.y
 conflicts: 3 shift/reduce
 PL.y:1531.24-1536.25: warning: rule useless in parser due to conflicts:  
AndExpr: AndExpr "AND" Expr
 PL.y:1549.25-1554.25: warning: rule useless in parser due to conflicts:
OrExpr: OrExpr "OR" Expr


I did a quick trial run, and it seems to work correctly:
cd ~/rpmbuild/BUILD/cvc3-2.1
LD_LIBRARY_PATH=`pwd`/lib bin/cvc3 +int
 CVC>  i, j: INT; ASSERT i = j + 1; QUERY i>j;
 Valid.
 CVC>   QUERY i<j; COUNTERMODEL;
 Invalid.
 Current scope level is 8.
 %Satisfiable  Variable Assignment: % 
 ASSERT (i = 0);
 ASSERT (j = -1);


It'd be *nice* (though it's not required) if this had a %check section for
automatic regression testing, e.g., something like:
 %check
 LD_LIBRARY_PATH=`pwd`/lib make regress4

-- 
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.