Bug 448502

[petro@host-12-116 frama-c-Hydrogen-20080502]$ ./configure 
configure: ******************
configure: * CONFIGURE MAKE *
configure: ******************
checking for make... make
make version is GNU Make 3.81: Good!
configure: *****************************
configure: * CONFIGURE OCAML COMPILERS *
configure: *****************************
checking for ocamlc... ocamlc
ocaml version is 3.10.0: Warning: unsupported version. Compile at your own risks
ocaml library path is /usr/lib/ocaml
checking for ocamlopt... ocamlopt
checking ocamlopt version... ok
checking for ocamlc.opt... ocamlc.opt
checking ocamlc.opt version... ok
checking for ocamlopt.opt... ocamlopt.opt
checking ocamlc.opt version... ok
configure: *******************************************
configure: * CONFIGURE MANDATORY TOOLS AND LIBRARIES *
configure: *******************************************
checking for ocamldep... ocamldep
checking for ocamldep.opt... ocamldep.opt
checking for ocamllex... ocamllex
checking for ocamllex.opt... ocamllex.opt
checking for ocamlyacc... ocamlyacc
checking for camlp4o... no
configure: error: You need to install camlp4.
[petro@host-12-116 frama-c-Hydrogen-20080502]$ rpm -q ocaml-camlp4
ocaml-camlp4-3.10.0-7.fc8
[petro@host-12-116 frama-c-Hydrogen-20080502]$

From the above log it's visible that there is some issue. I can't realise
whether tis issue in our camlp4 package or in Frama-C build scripts.

how about ocaml-camlp4-devel?

$ rpm -qf /usr/bin/camlp4o
ocaml-camlp4-devel-3.10.0-7.fc8

fine! )
I'll try to build it.

Another one issue:

checking for /usr/lib/ocaml/lablgtk2/lablgtk.cma... yes
checking for /usr/lib/ocaml/lablgtk2/lablgtksourceview.cma... no
checking for /usr/lib/ocaml/lablgtksourceview/lablgtksourceview.cma... no
configure: WARNING: lablgtksourceview not found
plugins not fully functional:
  gui

What package provides (if any) this component?

According to this page:
http://helm.cs.unibo.it/software/lablgtksourceview/
It's included in lablgtk 2.10, which we have in Rawhide at the moment, but I didn't
backport (because it's incompatible and would break lots of stuff).

I guess if it's optional, then perhaps we can leave it out for now, as long as it
doesn't disable too much functionality, or you can try building on Rawhide.

Another one option is to package it separately for Fedora [789]. I think it
doesn't break anything in a fragile set of ocaml tools :)

One note - seems that F9 already ships lablgtk 2.10 so we may add this
separately only for F8 (and F7, if someone still use it).

Is this a newly proposed package?

Shouldn't it be open against the Package Review component?

Yes, it's a proposal to package this software.

No package has actually been created yet though.

OK, let's see if I can make a package in the next 45 mins ...

http://www.annexia.org/tmp/ocaml-frama-c.spec

Potential problems:

(1) Entire copy of CIL is included.  Not really surprising, since
upstream CIL project is semi-dead, occasionally twitching a little bit.
I wonder how far Frama-C have modified their private copy?

(2) Puts lots of binaries in /usr/bin with quite generic names that
might conflict with other Fedora packages.

(3) Looks for a program called 'pvs'.  Gets LVM's 'pvs', which I'm
absolutely certain is wrong!

(4) Contains OCaml library files, but they are not installed in
OCaml libdir.  Not clear if we can move them safely.

(5) License situation is complex (but still seems to be free).  Someone
can work out the correct 'License' line for this pile.

(6) Project doesn't use real version numbers.

(7) Random stuff - eg. subproject containing loads of Java files.

(8) Package should probably be called 'frama-c', not 'ocaml-frama-c'.

(9) Includes a copy of 'why' (a verification tool) which IIRC we
already have in Fedora.

I would *really* like to see Frama-C packaged up.  The more recent versions have cleaned up some stuff that *should* simplify packaging.

I got Frama-C installed on Fedora 12 from the tarballs.  "Why" is packaged for Fedora, but needs to be updated to work with Frama-C; I know that Alan Dunn is working on that.

Regarding comment 12:
1. No idea how much CIL has been changed, but a query upstream might resolve this quickly.

2. Generic names could be renamed.

3. PVS has just been packaged, and renamed to "pvs-sbcl".  This no longer affects Frama-C at all (directly), it only affects the "why" package.  You need to modify "Why"'s configure to:
-    PVSLIB=`pvs -where`/lib
+    PVSLIB=`pvs-sbcl -where`/lib
and then invoke ./configure using:
  PVSC=/usr/bin/pvs-sbcl ./configure

4. That should be testable.  Are these library files merely "backups" in case the libraries are not already installed?

Ideally, this would invoke APRON, but packaging that is hard:
  https://bugzilla.redhat.com/show_bug.cgi?id=498604
So I think it'd be best to package WITHOUT APRON, then add that later once APRON is packaged.

5. License situation is far less complex now.  "Why" is now truly separate (instead of being a locally-modified version), and "Why" itself invokes tools that are separable.

6. Project still uses stupid versioning id's.  They're not the only ones, and that can be handled (if nothing else, by using dates).

7. (Skip)

8. I agree, the package should be called "frama-c" not "ocaml-frama-c".  Users won't care what it's implemented in.


I had to install a boatload of packages to get this to compile; my sequence was:
yum groupinstall "Development Libraries"
yum install ocaml ocaml-ocamlgraph gtksourceview lablgtk ocaml-lablgtk
yum install ocaml-lablgtk-devel
yum install ocaml-ocamldoc /usr/lib64/ocaml/lablgtk2/lablgnomecanvas.cmxa
yum install graphviz

yum install libgnomecanvas-devel gtksourceview-devel
# These aren't used now; may be used by APRON later:
yum install ppl ppl-devel ppl-utils ppl-docs

# Install ocaml-ocamlgraph if its version is >= 1.3, else remove it
# because frama-c's detection algorithm seems to be flakey.




To install Why, you'll need these:

# Lower-level tools for Why:
yum instsall cvc3 zenon alt-ergo coq

# Install pvs-sbcl  (currently in draft) for Why.

# These are needed for Why:
yum install ocaml-camlp4 ocaml-camlp4-devel

# No package ltl2ba available in repository.
# Note: lablgtksourceview has been integrated into lablgtk.


After installing Frama-C, you'll get SELinux errors.  Here they are, including the commands to get rid of the errors:

An SELinux secuity alert says:
SELinux is preventing /usr/local/bin/frama-c-gui from loading /usr/local/lib/frama-c/plugins/Jessie.cmxs which requires text relocation.
[frama-c-gui has a permissive type (unconfined_t). This access was not denied.]The frama-c-gui application attempted to load /usr/local/lib/frama-c/plugins/Jessie.cmxs which requires text relocation. This is a potential security problem. Most libraries do not need this permission. Libraries are sometimes coded incorrectly and request this permission. The SELinux Memory Protection Tests web page explains how to remove this requirement. You can configure SELinux temporarily to allow /usr/local/lib/frama-c/plugins/Jessie.cmxs to use relocation as a workaround, until the library is fixed. Please file a bug report.

If you trust /usr/local/lib/frama-c/plugins/Jessie.cmxs to run correctly, you can change the file context to textrel_shlib_t. "chcon -t textrel_shlib_t '/usr/local/lib/frama-c/plugins/Jessie.cmxs'" You must also change the default file context files on the system in order to preserve them even on a full relabel. "semanage fcontext -a -t textrel_shlib_t '/usr/local/lib/frama-c/plugins/Jessie.cmxs'" 
chcon -t textrel_shlib_t '/usr/local/lib/frama-c/plugins/Jessie.cmxs'

 SELinux is preventing /usr/local/bin/frama-c-gui from loading /usr/local/lib/frama-c/plugins/Ltl_to_acsl.cmxs which requires text relocation
If you trust /usr/local/lib/frama-c/plugins/Ltl_to_acsl.cmxs to run correctly, you can change the file context to textrel_shlib_t. "chcon -t textrel_shlib_t '/usr/local/lib/frama-c/plugins/Ltl_to_acsl.cmxs'" You must also change the default file context files on the system in order to preserve them even on a full relabel. "semanage fcontext -a -t textrel_shlib_t '/usr/local/lib/frama-c/plugins/Ltl_to_acsl.cmxs'" 


So, follow the SELinux instructions (above) to make them run without complaint.

I should note that when you install Why version 2.23 (versus version 2.21), there's an important change.  In Why version 2.21, by default you did NOT need to prove termination.  This resulted in some surprises, so starting in version 2.22, termination is required by default.

As a result, many of the documentation's demos require tweaking, because they don't include termination information. See this:
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-January/001736.html

For example, the Jessie tutorial section 2.2 needs to have a "loop variant" added, and this MUST be added using the /*@...*/ form NOT the //@, //@ forms.  Here is what it looks like:
/*@ lemma mean: \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y; */
//@ requires n >= 0 && \valid_range(t,0,n-1);
int binary_search(int* t, int n, int v) {
  int l = 0, u = n-1, p = -1;
  /*@ loop invariant 0 <= l && u <= n-1;
    @ loop variant u-l; */
  while (l <= u ) {
    int m = l + (u - l) / 2; // NOTE this is changed for bounded calculation
    if (t[m] < v)
      l = m + 1;
    else if (t[m] > v)
      u = m - 1;
    else {
      p = m; break;
    }
  }
  return p;
}

NOTE: I just talked with Alan Dunn, who as of 2010-01-12 is working on a frama-c package for Fedora.

I can respond to a number of these points now:

1) It looks like a decent bit - from the distribution in cil/CHANGES:

CHANGES with respect to original Cil library

a) Replaced custom pretty printers by module Format
b) All types of module Cil are declared in module Cil_types
c) Module Util renamed to Cilutil
d) Modified AST to support logic annotation
e) Some extension from cil/src/ext/ not yet ported.
f) Dataflow module modified (improved ?)
g) type instr contains only one intr not a list of instr.
h) Modified visitor to also visit logic annotations (see item d)

At minimum, (at least) items d and h are certainly important for this
project and are not going to be ported back into the original Cil as
the logic annotations are specific to Frama-C. While one might say
that they could've written this in a way that composes nicely with the
original Cil, I think that it would be fine (at least for now) allow
the modified cil distribution in - it will never be confused with the
original as the resultant files will come out in %{_libdir}/frama-c
and these files are likely necessary for Frama-C plugin development.

2) I don't see any particularly generic names. Perhaps you are
referring to the names that are in bin/ while Frama-C is being built?
They are copied into sensible places upon install. The "most generic",
that is, not containing "frama-c", name I can find is "ptests", and
this is one executable.

3) Addressed by David.

4) The libraries are included so that plugins can be created (the Why
distribution now has a Jessie plugin that is compiled using these
files - note that this means that when we're doen Why will
BuildRequire Frama-C).

It is true that the "library files" are installed in
%{_libdir}/frama-c as opposed to, say,
%{_libdir}/ocaml/frama-c. Moving these files may not be too
problematic as the makefiles appear to have variables that allow this
location to be changed. That being said, the makefiles are decently
complicated, so I would have to see if something like this
works. Would this move have to be done?

5) David - I disagree. The licensing situation is as complicated as
before given that the licensing difficulties actually come from the
sources within Frama-C (especially from the testing section). It seems
to me that the licensing line should read:

LGPLv2 and GPL+ and GPLv2 and GPLv2+ and BSD and (QPL with modifications)

I have a breakdown in an attached file (which describes part of my
method for determination). This generally agrees with the one from the
Debian folks
(http://packages.debian.org/changelogs/pool/main/f/frama-c/frama-c_20090901+beryllium+dfsg-2/frama-c.copyright),
save that it appears that they missed external/unmarshal* as being
BSD. (I don't see those listed at all actually...)

For the "modifications" part of the QPL, they stipulate a modification
that I believe makes the licensing "more free", though I could submit
the modifications (attached) to the fedora legal list.

I furthermore just noticed that their Makefile gives an indication of
which files they intended to put under which licenses (it manages the
headers for their files). This seems to match my analysis.

6) We could use dates, but the date doesn't convey the main
information that one would want - the main version is conveyed by an
element (we are now on "Beryllium"). We could take element -> number -
Frama-C Beryllium 2 = 1.4.2.

7) Why would the java files be a problem?

8) I agree that it should be called frama-c (this is consistant with Debian).

9) There is now a version without Why bundled.

Another two points -

1) I've never packaged anything that requires SELinux
changes before. It seems that the approaches one might use are along
the lines of http://fedoraproject.org/wiki/PackagingDrafts/SELinux, or
is there some better source I should be consulting? (Also, is this a
Frama-C bug? I can confirm that when I tried Frama-C out on F12 I got
the same errors as David.)

2) The "Modified Q License" bit is somewhat odd in that the files it
mentions are somewhat odd - eg: "standard.mly", which I don't see in
the distribution at all. This will probably require clarification from
upstream.

Created attachment 384647 [details]
Classification of licensing

Created attachment 384648 [details]
Q License and modifications

We should ask dwalsh about the selinux issues.  They probably
require changes to the base selinux-policy package.

(In reply to comment #17)
> 2) The "Modified Q License" bit is somewhat odd in that the files it
> mentions are somewhat odd - eg: "standard.mly", which I don't see in
> the distribution at all. This will probably require clarification from
> upstream.    

Clarification from upstream received:

http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-January/001755.html

Alan Dunn is developing a package for Frama-C.  There's more to do, but I asked him to publish his early draft so people could comment / make suggestions, and he's done so:
https://bugzilla.redhat.com/show_bug.cgi?id=564520

Can we keep everything in one bug please ...

*** This bug has been marked as a duplicate of bug 564520 ***