Package Details: frama-c 1:21.1-1

Git Clone URL: https://aur.archlinux.org/frama-c.git (read-only, click to copy)
Package Base: frama-c
Description: Extensible platform dedicated to source-code analysis of C software.
Upstream URL: http://frama-c.com
Licenses: LGPL2.1
Submitter: pherms
Maintainer: aksr
Last Packager: aksr
Votes: 14
Popularity: 0.000001
First Submitted: 2009-10-30 16:24 (UTC)
Last Updated: 2020-10-02 10:30 (UTC)

Latest Comments

Grunzwanzling commented on 2021-12-06 22:17 (UTC)

I am getting that same "missing why3" error.

pirofti commented on 2021-11-03 16:27 (UTC)

Currently I get a missing why3 error when building:

Ocamlc       src/plugins/wp/rformat.cmi
ocamlfind: Package `why3' not found
make: *** [share/Makefile.generic:71: src/plugins/wp/rformat.cmi] Error 2
==> ERROR: A failure occurred in build().
    Aborting...
 -> error making: frama-c

abougouffa commented on 2021-07-22 19:20 (UTC)

The packages can't build any more, the gtksourceview2 dependency is missing

NieDzejkob commented on 2019-04-23 21:06 (UTC)

I needed to do some manipulations to get it to build the gui binary.

  • apply this patch to lablgtk2 to make it build lablgnomecanvas:
Index: lablgtk2/trunk/PKGBUILD
===================================================================
--- lablgtk2/trunk/PKGBUILD (revision 352021)
+++ lablgtk2/trunk/PKGBUILD (working copy)
@@ -7,7 +7,7 @@
 arch=(x86_64)
 license=('LGPL')
 url="http://lablgtk.forge.ocamlcore.org/"
-depends=('gtk2' 'librsvg' 'gtksourceview2')
+depends=('gtk2' 'librsvg' 'gtksourceview2' 'libgnomecanvas')
 makedepends=('ocaml-compiler-libs>=4.0.7' 'camlp4>=4.07')
 optdepends=('ocaml: for using the tools')
 DLAGENTS=('https::/usr/bin/curl -fLC - --insecure --retry 3 --retry-delay 3 -o %o %u')
@@ -14,6 +14,7 @@
 source=("https://forge.ocamlcore.org/frs/download.php/1726/lablgtk-2.18.6.tar.gz")
 md5sums=('30e9eef159eb88db0dce2438a60a6402')
 options=(!makeflags staticlibs)
+group=(modified)

 build() {
   cd "${srcdir}/lablgtk-${pkgver}"
@@ -20,7 +21,6 @@
   ./configure --prefix=/usr \
     --without-glade \
     --without-gnomeui \
-    --without-gnomecanvas \
     --without-panel \
     --without-gtkspell \
     --without-gtksourceview
  • rebuild ocaml-ocamlgraph after installing this modified lablgtk2
  • rebuild frama-c. Make sure that you do this on a clean source tree, otherwise OCaml will complain when linking.

NieDzejkob commented on 2019-04-23 20:31 (UTC)

@oriba: AFAICS, that's expected. Try frama-c --help. If you want the gui, you need to run frama-c-gui. This binary does not build for me, the configure script complains about a missing lablgnomecanvas.

oriba commented on 2019-03-07 20:24 (UTC)

Package can be built and installed, but frama-c starts, does nothing and then ends execution.

HalosGhost commented on 2018-10-08 17:40 (UTC)

Looks like ocaml-findlib needs to be moved into depends, as frama-c plain fails to execute (even with no arguments) without it installed.

Additionally, it looks like the build still fails to enable the gui (due to the missing /usr/lib/ocaml/lablgtk2/lablgnomecanvas.cmxa (as referenced by mathieu.

All the best,

-HG

untitled commented on 2018-08-27 12:23 (UTC) (edited on 2018-08-27 12:24 (UTC) by untitled)

To fix build:

diff --git a/.SRCINFO b/.SRCINFO
index 41faa78..02412b2 100644
--- a/.SRCINFO
+++ b/.SRCINFO
@@ -1,8 +1,6 @@
-# Generated by mksrcinfo v8
-# Sat Jul  7 05:09:59 UTC 2018
 pkgbase = frama-c
    pkgdesc = Extensible platform dedicated to source-code analysis of C software.
-   pkgver = 20180501
+   pkgver = 20180502
    pkgrel = 1
    url = http://frama-c.com
    arch = i686
@@ -18,15 +16,15 @@ pkgbase = frama-c
    makedepends = ocaml-num
    depends = gtksourceview2
    depends = libgnomecanvas
-   depends = zarith
+   depends = ocaml-zarith
    optdepends = lablgtk2
    optdepends = coq
    optdepends = graphviz
    optdepends = ltl2ba
-   source = http://frama-c.com/download/frama-c-Chlorine-20180501.tar.gz
-   md5sums = 2d61aa200ded2dd360a8310c9a03ac50
-   sha1sums = 18281a6b9022bf1009e0f09513b289baa8b447ef
-   sha256sums = 6ff8160f4800e007fb00b1b3f91dc72a97cbb3ee154a0e71181b6e5bad33883a
+   source = http://frama-c.com/download/frama-c-Chlorine-20180502.tar.gz
+   md5sums = 5c152f0859880d48f98377de59d6328a
+   sha1sums = c2e734eeb625cd6011c80b61672c6643b05e2ed7
+   sha256sums = ecc9f5822294b76c345973858a6d8da940bae4042b394ffd3d25fd60114499d4

 pkgname = frama-c

diff --git a/PKGBUILD b/PKGBUILD
index d5f78b5..fe6b04d 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -3,19 +3,19 @@
 # Maintainer: aksr <aksr at="" dot="" me="" t-com="">
 pkgname=frama-c
 _codename=Chlorine
-pkgver=20180501
+pkgver=20180502
 pkgrel=1
 pkgdesc='Extensible platform dedicated to source-code analysis of C software.'
 arch=('i686' 'x86_64')
 license=('LGPL2.1')
 url='http://frama-c.com'
-depends=('gtksourceview2' 'libgnomecanvas' 'zarith')
+depends=('gtksourceview2' 'libgnomecanvas' 'ocaml-zarith')
 makedepends=('lablgtk2' 'coq' 'graphviz' 'ltl2ba' 'ocaml' 'ocaml-ocamlgraph' 'ocaml-findlib' 'ocaml-num')
 optdepends=('lablgtk2' 'coq' 'graphviz' 'ltl2ba')
 source=("http://frama-c.com/download/${pkgname}-${_codename}-${pkgver}.tar.gz")
-md5sums=('2d61aa200ded2dd360a8310c9a03ac50')
-sha1sums=('18281a6b9022bf1009e0f09513b289baa8b447ef')
-sha256sums=('6ff8160f4800e007fb00b1b3f91dc72a97cbb3ee154a0e71181b6e5bad33883a')
+md5sums=('5c152f0859880d48f98377de59d6328a')
+sha1sums=('c2e734eeb625cd6011c80b61672c6643b05e2ed7')
+sha256sums=('ecc9f5822294b76c345973858a6d8da940bae4042b394ffd3d25fd60114499d4')

 build() {
   cd "$srcdir/$pkgname-$_codename-$pkgver"
</aksr>

zorun commented on 2018-03-08 22:47 (UTC)

ocaml-num should be added to the dependencies (it got split off the main ocaml distribution).

greencopper commented on 2018-03-08 05:31 (UTC)

I have installed all the dependencies.

During installation:

Generating META.frama-c-aorai Ocamlc src/plugins/aorai/bool3.cmi ocamlfind: Package `num' not found make: *** [share/Makefile.generic:71: src/plugins/aorai/bool3.cmi] Error 2

And it fails to build.

khouli commented on 2017-10-07 18:53 (UTC)

Changes to bring PKGBUILD up to date: [...] _codename=Phosphorus pkgver=20170501 pkgrel=1 [...] md5sums=('996a4690cce7c4812dae74837cf0faa3') sha1sums=('d9372127ba80636cc1c692a141a7a02dee8325da') sha256sums=('614f384ea487206df2ba42ddf66de610cc45846bb7b7aeafcbc40e5d99626c99') [...]

bms commented on 2017-07-30 20:29 (UTC)

@Mathieu, did you find a way to compile this in the meantime?

mathieu.clabaut commented on 2017-06-29 09:13 (UTC)

Since some time /usr/lib/ocaml/lablgtk2/lablgnomecanvas.cmxa is not packed anymore in lablgtk2 (https://bugs.archlinux.org/task/52796) which prevents to build frama-c-gui. Any tip on how to circumvent this problem is welcome.

zorun commented on 2017-01-07 17:28 (UTC)

ocaml-findlib is needed as a makedepends, otherwise this package fails to build. Also, for some reason, the build system does not find zarith, even though it is installed: checking for Zarith... configure: WARNING: Zarith not found: will use the default less efficient library instead checking for Apron... not found. The corresponding domains won't be available in Eva It seems that zarith does not contain a META file, maybe this is why frama-c does not find it?

mthowe commented on 2015-08-17 06:22 (UTC)

I've added the zarith and ltl2ba dependencies back into the AUR and this now builds. Unfortunately I don't think I can undo the out-of-date flagging, sorry about that.

mthowe commented on 2015-08-17 03:40 (UTC)

This no longer builds, as it seems both zarith and ltl2ba dependencies have disappeared. I'm going to try to look into why that is the case. If they were just no longer maintained, I've found the old PKGBUILDs for both of them and can hopefully get them brought up to date.

Barthalion commented on 2014-12-28 23:00 (UTC)

I haven't found time to fix it during last two months, so it makes sense to me to orphan it.

saabzero commented on 2014-11-19 00:29 (UTC)

I managed to build this, but i get segmentation fault (core dumped) when starting the GUI version. Any ideas? Also, is there a way to get the Fluorine version of frama-c to build? I modified the PKGBUILD to do so, but compilation fails with: File "src/ai/abstract_interp.mli", line 166, characters 4-33: Error: In this `with' constraint, the new definition of O does not match its original definition in the constrained signature: ... The value `of_list' is required but not provided The value `find' is required but not provided Any help appreciated!

voins commented on 2014-11-17 00:09 (UTC)

aksr, the problem is in zarith package. Just add options=staticlibs to the zarith's PKGBUILD.

commented on 2013-04-04 02:04 (UTC)

@pherms, I picked up and run several lines from your PKGBUILD successfully. Now I can use frama-c,Version: Oxygen-20120901 on my Ubuntu. Thank you.

commented on 2013-04-03 06:11 (UTC)

Sorry for my repeated comments, I thought I could remove my comments by clicking red X button. I'm very new to Frama-c and almost new to Ubuntu. Now I've resognized the PKGBUILD on this page. Could you tell me how to use it. Thank you in advance. Ted

commented on 2013-04-03 02:56 (UTC)

Sorry for my repeated comments, I thought I could remove my comments by clicking red X button. I'm very new to Frama-c and almost new to Ubuntu. Now I've resognized the PKGBUILD on this page. Could you tell me how to use it. Thank you in advance. Ted

commented on 2013-04-03 02:23 (UTC)

Yes, I've got the same error message as ViktorCodes had.

commented on 2013-04-03 02:21 (UTC)

Yes, I've got the same error message as ViktorCodes had.

commented on 2013-04-03 01:31 (UTC)

Yes, I've got the same error message as ViktorCodes had.

pherms commented on 2013-04-01 10:59 (UTC)

The current PKGBUILD script patches the configure script. Are you sure it's the same problem you have?

commented on 2013-04-01 05:17 (UTC)

@pherms Please tell me where the updated configure script is. I have the same problem.

pherms commented on 2013-03-05 23:55 (UTC)

That is due to an incompatibility with ocamlgraph if its compiled with lablgtk. I patched the configure script to make it chose a locally compiled ocamlgraph.

commented on 2013-03-04 22:50 (UTC)

im kind of new here, and correct me if i'm wrong, but graphviz (available from the official repo) should be added as a dependency or perhaps an optional dependency. the same goes with ltl2ba (http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ltl2ba-1.1.tar.gz), which after compiled with make, the executable "ltl2ba" only needs to go in a directory defined in PATH like /usr/bin/ all of this is for the the gui to be fully available, according to the warnings from the configure file Also it does not compile. I'm getting the following error: File "src/gui/debug_manager.ml", line 25, characters 0-11: Error: Unbound module Dgraph make: *** [src/gui/debug_manager.cmo] Error 2

pherms commented on 2012-10-31 21:13 (UTC)

Ok, then this is a bug of the lablgtk2 package. You may want to file a bug at https://www.archlinux.org/packages/extra/x86_64/lablgtk2/

Mindless commented on 2012-10-31 19:22 (UTC)

Both ocaml and lablgtk2 were the official packages from extra for x86_64. I rebuilt lablgtk2 from source and was then able to build frama-c, so it looks like you're right.

pherms commented on 2012-10-31 17:24 (UTC)

For me it seems your installation of lablgtk wasn't compiled with your installation of OCaml, which is strange if you installed only packages from the official repositories...

Mindless commented on 2012-10-31 04:00 (UTC)

> ocamlc.opt -g -o view_graph/viewgraph.byte -I +lablgtk2 -I view_graph -I src -I lib -I . \ > lablgtk.cma gtkInit.cmo lablgnomecanvas.cma unix.cma graph.cma view_graph/viewgraph.cmo > File "_none_", line 1: > Error: Files /usr/lib/ocaml/lablgtk2/lablgtk.cma(Gpointer) > and /usr/lib/ocaml/stdlib.cma(StdLabels) > make inconsistent assumptions over interface StdLabels > make[1]: *** [view_graph/viewgraph.byte] Error 2 Seems to not compile?

pherms commented on 2011-05-31 09:38 (UTC)

I changed it to gtksourceview2, which is used by lablgtk2. I don't use gnome and I haven't installed gtksourceview3 and for me it works like this.

mathieu.clabaut commented on 2011-05-31 09:01 (UTC)

gtksourceview doesn't exist anymore. You have to use gtksourceview3 or do I make a mistake ?

pherms commented on 2011-01-31 22:17 (UTC)

Didn't test it but now it's added. Please report if there are problems

reflectionalist commented on 2011-01-31 19:53 (UTC)

Why is 'i686' missing. I have no trouble compiling it. There's only a minor issue which warned package has reference to srcdir, but did not report exactly what it is.

commented on 2011-01-19 07:17 (UTC)

> I have another problem: > ... > make: *** [test.stat] Error 139 > [jessie] user error: Jessie subprocess failed: make -f test.makefile gui Strangely enough, deleting a file ".gtkrc-2.0" helped me solve this problem. It was generated by "gtk-chtheme". With ".gtkrc-2.0" generated by "gtk-theme-switch2" everything works well.

pherms commented on 2010-12-20 17:10 (UTC)

Well, this should not happen. I think the developers should hear about it, but the frama-c team is not concerned. Rather submit a bug report at http://why.lri.fr

incubos commented on 2010-12-20 16:06 (UTC)

pherms, thanks! I have another problem: $ frama-c -jessie test.c [kernel] preprocessing with "gcc -C -E -I. -dD test.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir test.jessie [jessie] File test.jessie/test.jc written. [jessie] File test.jessie/test.cloc written. [jessie] Calling Jessie tool in subdir test.jessie Generating Why function max [jessie] Calling VCs generator. gwhy-bin [...] why/test.why Computation of VCs... Computation of VCs done. Reading GWhy configuration... Loading .gwhyrc config file GWhy configuration loaded... Creating GWhy Tree view... GWhy Tree view created... Creating GWhy views... /bin/sh: line 1: 2440 Segmentation fault WHYLIB=/usr/lib/why gwhy-bin -split-user-conj -explain -locs test.loc /usr/lib/why/why/jessie.why why/test.why make: *** [test.stat] Error 139 [jessie] user error: Jessie subprocess failed: make -f test.makefile gui Should I post a bug to frama-c developers?

pherms commented on 2010-12-20 14:47 (UTC)

Yes, that was a bug in the why package. Should work now.

incubos commented on 2010-12-20 13:35 (UTC)

I have a problem with running jessie plugin: $ frama-c -jessie test.c [kernel] user error: option `-jessie' is unknown. use `frama-c -help' for more information. [kernel] Frama-C aborted because of invalid user input. The environment: * coq 8.3-4 * frama-c 20101202_beta2-1 * why 2.28-1 (built and installed after frama-c) why-config tells: $ why-config ... prover version info invocation ------------------------------------------------------ Alt-Ergo 0.92 (not supported) alt-ergo Simplify 1.5.4 simplify Z3 2.2 z3 -smt Yices 1.0.24 yices -smt CVC3 not found CVCL not found Gappa not found Coq 8.3 (not supported) coqc PVS not found VeriT not found ------------------------------------------------------

commented on 2010-10-18 20:52 (UTC)

namcap (sanity checking tools for arch linux packages and PKGBUILDs) report: frama-c E: Dependency detected and not included (gtksourceview2) from files ['usr/bin/frama-c-gui.byte', 'usr/bin/frama-c-gui'] frama-c W: Dependency included and not needed ('gtksourceview') Based on what I can find it is correct here.

pherms commented on 2010-04-13 21:34 (UTC)

The jessie plugin is now in the separated why package. Build it after frama-c is installed.