[Bug 592579] Review Request: Frama-c - Framework for source code analysis of C software

Fri May 21 22:27:09 UTC 2010

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=592579

--- Comment #3 from David A. Wheeler <dwheeler at dwheeler.com> 2010-05-21 18:27:06 EDT ---
My first step in reviewing the package was reviewing the rpmlint errors
from the spec file and the 2 generated binary RPMs,
which on my system produced 2 errors and 5 warnings.

I'd *really* like input from an OCaml expert (PSST: RICHARD JONES!)
for the "unstripped-binary-or-object" messages, esp. for
"/usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs".  Ignoring that warning
is easy enough, but *should* it be ignored?

With that, here are some initial comments:

* frama-c.i586: E: devel-dependency gtksourceview-devel

You need to fix some "Requires:" lines in the .spec file.
In particular, the problem is that you've specifically included
as "Requires" statements some -devel libraries as "Requires".
You should *not* make "Requires" statements unless you have to;
rpm will figure them out, and will typically do a better job anyway.
The *big* case where you need requires statements is if you need
to state that specific version (minimums) are required.

So, please change the spec as follows, which improves the
spec and gets rid of this rpmlint error:

 Requires: graphviz >= 2.0.0
-Requires:   gtksourceview >= 1.0.0, gtksourceview-devel
-Requires:  ocaml >= 3.11.0, ocaml-findlib-devel, ocaml-lablgtk-devel,
ocaml-ocamlgraph-devel
+Requires: gtksourceview >= 1.0.0
+Requires: ocaml >= 3.11.0

* frama-c.i586: W: invalid-license QPL with modifications
* frama-c-devel.i586: W: invalid-license QPL with modifications

The term "QPL with modifications" is not one of the valid licenses
known to rpmlint.  I looked into what's going on, and I think this
software license is clearly FLOSS, as I describe below.

However, you're going to have to get legal to approve it, as described in:
  http://fedoraproject.org/wiki/Packaging:LicensingGuidelines
"The License: field must be filled with the appropriate license Short
License identifier(s) from the "Good License" tables on the  Fedora
Licensing page. If your license does not appear in the tables, it needs to
be sent to fedora-legal-list at redhat.com (note that this list is moderated,
only members may directly post). If the license is approved, it will be
added to the appropriate table."

They'll also need to approve some sort of short name, since
"QPL with modifications" is not on the approved list.

I'm not a lawyer, but I *did* look at this, and here's what I learned
in the hope that it helps.  At issue seems to be this license:
 ~/rpmbuild/BUILD/frama-c-Beryllium-20090902/licenses/Q_MODIFIED_LICENSE

It's QPL version 1.0, an already-approved FLOSS license, with some
modifications.  I only found 2 modifications:
1. An *additional* permission.  If you DON'T release to your program
   to the general public, you don't have to comply with QPL requirement 6c.
   ("You must ensure that all modifications included in the
   machine-executable forms are available under the terms of this license.")
   I don't see how giving ADDITIONAL permissions makes a FLOSS license
   non-FLOSS.
2. A choice of venue ("This license is governed by the Laws of France.")
   I'm not crazy about choice-of-venue clauses, but other FLOSS licenses
   have them (e.g., CeCILL), so that cannot make it non-FLOSS.

Here's the actual text from the license that shows these modifications:
==============================================================
In the following, "the Library" refers to the following file:
  standard.mly
and "the Generator" refers to all files marked "Copyright INRIA" in the
root directory.

The Generator is distributed under the terms of the Q Public License
version 1.0 with a change to choice of law (included below).

The Library is distributed under the terms of the GNU Library General
Public License version 2 (included below).

As a special exception to the Q Public Licence, you may develop
application programs, reusable components and other software items
that link with the original or modified versions of the Generator
and are not made available to the general public, without any of the
additional requirements listed in clause 6c of the Q Public licence.

As a special exception to the GNU Library General Public License, you
may link, statically or dynamically, a "work that uses the Library"
with a publicly distributed version of the Library to produce an
executable file containing portions of the Library, and distribute
that executable file under terms of your choice, without any of the
additional requirements listed in clause 6 of the GNU Library General
Public License.  By "a publicly distributed version of the Library",
we mean either the unmodified Library as distributed by INRIA, or a
modified version of the Library that is distributed under the
conditions defined in clause 3 of the GNU Library General Public
License.  This exception does not however invalidate any other reasons
why the executable file might be covered by the GNU Library General
Public License.
... [at the end of the QPL]:
                            Choice of Law
This license is governed by the Laws of France.
==============================================================

* frama-c.i586: W: unstripped-binary-or-object
/usr/lib/frama-c/plugins/Ltl_to_acsl.cmxs
* frama-c.i586: W: unstripped-binary-or-object /usr/bin/frama-c.byte
* frama-c.i586: W: unstripped-binary-or-object /usr/bin/frama-c-gui.byte

I'm not an OCaml expert, and these are clearly related to OCaml.
I'd really like the input of an OCaml expert on this point.
For some guidance, I looked here:
  http://fedoraproject.org/wiki/Packaging/OCaml

Rpmlint reports "unstripped-binary-or-object" on /usr/bin/frama-c.byte
and /usr/bin/frama-c-gui.byte but I think it's even more complicated :-(.
Rpmlint correctly reports that it has a symbol table (readelf agrees).

However, trying to run these files reports "No bytecode file specified.",
a tell-tale sign of a (partly) *stripped* bytecode file.

Basically, these two ".byte" files are completely corrupted; they can't
be run as-is.  If this is unfixable, perhaps it'd be better to simply
remove these ".byte" files, since the cannot be run at all, and limit
the package to those architectures which support native executables.

This page:
  http://caml.inria.fr/pub/docs/manual-ocaml/libref/Dynlink.html
explains that .cmxs files are OCaml plugin files in native mode;
basically, they're libraries that can be dynamically loaded at run-time.
Suggestions welcome.

* frama-c.i586: E: forbidden-selinux-command-in-%post chcon
An rpmlint --info gives a little more info:
"A command which requires intimate knowledge about a specific SELinux
policy type was found in the scriptlet. These types are subject to change
on a policy version upgrade. Use the restorecon command which queries
the currently loaded policy for the correct type instead."

At issue is this text in the spec:
%post
chcon -t textrel_shlib_t '%{_libdir}/frama-c/plugins/Ltl_to_acsl.cmxs'
semanage fcontext -a -t textrel_shlib_t
'%{_libdir}frama-c/plugins/Ltl_to_acsl.cmxs'

You need to do this in a cleaner way; you're not supposed to use chcon
in %post.  You may find this useful:
 https://fedoraproject.org/wiki/PackagingDrafts/SELinux/PolicyModules

* BIG ISSUE: Where's the "-jessie" option of frama-c?

When I have a C file, I should be able to invoke:
 frama-c -jessie demo.c
yet "-jessie" isn't available.
I understand that the Jessie plug-in is actually in "Why",
but there needs to be a way to *invoke* it.

* Note: There's a newer version of Frama-C, version Boron 20100401,
  available on their site.  Should we switch to it?
  Obviously, there's an issue of how it invokes Jessie.

* I don't see your name ("Mark Rader") in the ChangeLog at the end.

Hope this helps...

-- 
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.