[Bug 456398] Review Request: why - Why software verification platform
bugzilla at redhat.com
bugzilla at redhat.com
Sat Aug 2 03:24:24 UTC 2008
Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug report.
Summary: Review Request: why - Why software verification platform
https://bugzilla.redhat.com/show_bug.cgi?id=456398
------- Additional Comments From amdunn at gmail.com 2008-08-01 23:24 EST -------
I made a new version to incorporate your suggested changes:
SRPM: http://www.duke.edu/~amd34/why/why-2.14-2.fc9.src.rpm
SPEC: http://www.duke.edu/~amd34/why/why.spec
(In reply to comment #10)
> Okay, I've looked this over, installed on my own system and tested it, etc.
> It's generally quite good, but there are a few issues... but I think they'll be
> really easy to fix.
>
> * rpmls of each binary package looks fine (permissions reasonable)
>
> - MUST: rpmlint must be run on every package. The output should be posted in the
> review.
> Ok. No errors, and the warning is a well-known one
> that is the fault of the ocaml compiler. See:
> https://bugzilla.redhat.com/show_bug.cgi?id=450551
> http://caml.inria.fr/mantis/view.php?id=4564
> http://groups.google.com/group/fa.caml/browse_thread/thread/2d247a192eb92826
>
> But you could do better; apply "execstack -c" to ELF files in /usr/bin,
> and the programs will run without an executable stack.
> That's a better idea; OCaml doesn't actually require an executable stack,
> and the noexec stack will protect the low-level C routines it calls.
>
> $ rpmlint SPECS/why.spec SRPMS/why-2.14-1.fc9.src.rpm \
> RPMS/i386/why-2.14-1.fc9.i386.rpm
> why.i386: W: executable-stack /usr/bin/why-stat
> why.i386: W: executable-stack /usr/bin/why2html
> why.i386: W: executable-stack /usr/bin/why-dp
> why.i386: W: executable-stack /usr/bin/caduceus
> why.i386: W: executable-stack /usr/bin/rv_merge
> why.i386: W: executable-stack /usr/bin/why
> why.i386: W: executable-stack /usr/bin/jessie
> why.i386: W: executable-stack /usr/bin/simplify2why
> why.i386: W: executable-stack /usr/bin/why-obfuscator
> why.i386: W: executable-stack /usr/bin/krakatoa
> 2 packages and 1 specfiles checked; 0 errors, 10 warnings.
Fixed - turns out that (as I mentioned to you separately) I was not seeing these
warnings due to an old version of rpmlint (oops). I took your suggestion -
running execstack -c on all (native code) binaries.
> - MUST: The package must be named according to the Package Naming Guidelines
> OK.
>
> - MUST: The spec file name must match the base package %{name}, in the format
> %{name}.spec unless your package has an exemption on Package Naming Guidelines.
> OK
>
> - MUST: The package must meet the Packaging Guidelines.
> OK (I didn't see any errors)
>
> - MUST: The package must be licensed with a Fedora approved license and meet the
> Licensing Guidelines.
> OK (GPLv2)
>
> - MUST: The License field in the package spec file must match the actual license.
> Yes; README, INSTALL, and COPYING all quite explicit that it is GPLv2.
>
> - MUST: If (and only if) the source package includes the text of the license(s)
> in its own file, then that file, containing the text of the license(s) for the
> package must be included in %doc.
>
> FAIL. At _least_ install file "COPYING" in %doc, and go ahead and include "GPL"
> too.
Fixed.
> - MUST: The spec file must be written in American English.
> OK
>
> - MUST: The spec file for the package MUST be legible. If the reviewer is unable
> to read the spec file, it will be impossible to perform a review. Fedora is not
> the place for entries into the Obfuscated Code Contest (http://www.ioccc.org/).
> OK
>
> - MUST: The sources used to build the package must match the upstream source, as
> provided in the spec URL. Reviewers should use md5sum for this task. If no
> upstream URL can be specified for this package, please see the Source URL
> Guidelines for how to deal with this.
> OK
>
> - MUST: The package must successfully compile and build into binary rpms on at
> least one supported architecture.
> OK
>
> - MUST: If the package does not successfully compile, build or work on an
> architecture, then those architectures should be listed in the spec in
> ExcludeArch. Each architecture listed in ExcludeArch needs to have a bug filed
> in bugzilla, describing the reason that the package does not compile/build/work
> on that architecture. The bug number should then be placed in a comment, next to
> the corresponding ExcludeArch line. New packages will not have bugzilla entries
> during the review process, so they should put this description in the comment
> until the package is approved, then file the bugzilla entry, and replace the
> long explanation with the bug number. The bug should be marked as blocking one
> (or more) of the following bugs to simplify tracking such issues:
> FE-ExcludeArch-x86 , FE-ExcludeArch-x64 , FE-ExcludeArch-ppc ,
FE-ExcludeArch-ppc64
> OK
>
> - MUST: All build dependencies must be listed in BuildRequires, except for any
> that are listed in the [wiki:Self:Packaging/Guidelines#Exceptions exceptions
> section of Packaging Guidelines] ; inclusion of those as BuildRequires is
> optional. Apply common sense.
> OK (builds in mock)
(Still builds in mock.)
> - MUST: The spec file MUST handle locales properly. This is done by using the
> %find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.
> OK (No locale issue).
>
> - MUST: Every binary RPM package which stores shared library files (not just
> symlinks) in any of the dynamic linker's default paths, must call ldconfig in
> %post and %postun....
> OK (N/A)
>
> - MUST: If the package is designed to be relocatable...
> OK (N/A)
>
> - MUST: A package must own all directories that it creates. If it does not
> create a directory that it uses, then it should require a package which does
> create that directory. Refer to the Guidelines for examples.
> OK
>
> - MUST: A package must not contain any duplicate files in the %files listing.
> OK
>
> - MUST: Permissions on files must be set properly. Executables should be set
> with executable permissions, for example. Every %files section must include a
> %defattr(...) line.
> OK. I checked the permissions on the binary RPMs using rpmls, looks okay.
>
> - MUST: Each package must have a %clean section, which contains rm -rf
> %{buildroot} ([wiki:Self:Packaging/Guidelines#UsingBuildRootOptFlags or
> $RPM_BUILD_ROOT] ).
> OK
>
> - MUST: Each package must consistently use macros, as described in the
> [wiki:Self:Packaging/Guidelines#macros macros section of Packaging Guidelines].
> OK
>
> - MUST: The package must contain code, or permissable content. This is described
> in detail in the [wiki:Self:Packaging/Guidelines#CodeVsContent code vs. content
> section of Packaging Guidelines] .
> OK
>
> - MUST: Large documentation files should go in a -doc subpackage. (The
> definition of large is left up to the packager's best judgement, but is not
> restricted to size. Large can refer to either size or quantity)
> OK (N/A)
>
> - MUST: If a package includes something as %doc, it must not affect the runtime
> of the application. To summarize: If it is in %doc, the program must run
> properly if it is not present.
> OK
>
> - MUST: Header files must be in a -devel package.
> OK (N/A)
>
> - MUST: Static libraries must be in a -static package.
> OK (N/A)
>
> - MUST: Packages containing pkgconfig(.pc) files must 'Requires: pkgconfig' (for
> directory ownership and usability).
> OK (N/A)
>
> - MUST: If a package contains library files with a suffix (e.g. libfoo.so.1.1),
> then library files that end in .so (without suffix) must go in a -devel package.
> OK (N/A)
>
> - MUST: In the vast majority of cases, devel packages must require the base
> package using a fully versioned dependency: Requires: %{name} =
> %{version}-%{release}
> OK (N/A)
>
> - MUST: Packages must NOT contain any .la libtool archives, these should be
> removed in the spec.
> OK (N/A)
>
> - MUST: Packages containing GUI applications must include a %{name}.desktop
> file, and that file must be properly installed with desktop-file-install in the
> %install section.
> OK (Verified on desktop)
>
> - MUST: Packages must not own files or directories already owned by other
> packages. The rule of thumb here is that the first package to be installed
> should own the files or directories that other packages may rely upon. This
> means, for example, that no package in Fedora should ever share ownership with
> any of the files or directories owned by the filesystem or man package. If you
> feel that you have a good reason to own a file or directory that another package
> owns, then please present that at package review time.
> OK. I don't know how to check that automatically, but a look using rpmls at the
> binary files looks okay.
>
> - MUST: At the beginning of %install, each package MUST run rm -rf %{buildroot}
> ([wiki:Self:Packaging/Guidelines#UsingBuildRootOptFlags or $RPM_BUILD_ROOT] ).
> See [wiki:Self:Packaging/Guidelines#PreppingBuildRootForInstall Prepping
> BuildRoot For %install] for details.
> OK
>
> - MUST: All filenames in rpm packages must be valid UTF-8.
> OK.
>
>
> Serious problems:
> * gwhy fails if the .c file isn't in the current directory (home directory if
> invoked from the GUI).
Fixed (change to gwhy.sh, further correction to my patch).
> * In the Zenity patch, use --file-selection not --entry to get the filename.
> That way, people can use a GUI to traverse the directory structure and click on
> the right file.
Changed.
> Strongly recommend fixing:
> * apply "execstack -c" to ELF files in /usr/bin, as noted above. (But only if
> they're ELF, don't do that to bytecode). That will enable the exec-stack
> protection, there's no reason it should be disabled.
Fixed, see above.
> * In the description, change "Furthermore, in theory," to just "Furthermore".
> To a lot of people, "in theory" means "not really". Since they've demonstrated
> the truth of the claim for 2 rather different languages, I think they've proved
> that claim.
Changed.
> * By default gwhy gives a HUGE list of potential provers, even when they aren't
> installed. That's a big pain - you want beginning users to have a reasonable
> view when they start!! In the long term, I think upstream should modify gwhy so
> that at start-up it detects which provers exist, and only shows the ones that
> are installed. For the short term, can you modify the defaults so that by
> default, if the user hasn't made any selections, only Zenon, Ergo, and CVC3 are
> shown?
Changed, patch to config.ml.
> Other suggestions:
> * Simplify this comment:
> # Native ocaml builds do not seem to work on ppc64 (not the first
> # package for which this has been true)
> to something shorter like this:
> # Native ocaml builds don't work on ppc64 (many packages have this problem)
Changed.
> * I think you should modify the %files list to use wildcards and %exclude,
> instead of (for example) listing every file in /usr/bin. It would simplify the
> %files list greatly. It would also make updates much easier; if a future
> version of the package installs some new files (e.g., in /usr/bin), the spec
> file would be more likely to "just work" if it used wildcards. E.G., I suggest
> something like this:
> %files
> %{_bindir}/*
> %exclude %{_bindir}/gwhy*
> ...
> You must _not_ say "%{bindir}/" (that tries to grab /usr/bin itself), but
> %{bindir}/* is fine... and in this case, I think it's preferable.
>
Fixed.
Also, re:
Most of the SHOULDs don't apply, but I think this one does:
- SHOULD: Usually, subpackages other than devel should require the base package
using a fully versioned dependency.
The subpackages aren't fully versioned. Is there a reason for that?
Fixed this too.
Let me know what you think (and if you think any more changes would be good).
--
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, or are watching someone who is.
More information about the package-review
mailing list