Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C 15 Phosphorus is out

  • Subject: [Frama-c-discuss] Frama-C 15 Phosphorus is out
  • From: mehdi at dogguy.org (Mehdi Dogguy)
  • Date: Fri, 11 Aug 2017 16:19:01 -0400
  • In-reply-to: <CA+yPOVgmjyU_h8_Y8+bdfQMbtUfTK-6hT_cqTJKbwV_7rvCOmw@mail.gmail.com>
  • References: <CA+yPOVgmjyU_h8_Y8+bdfQMbtUfTK-6hT_cqTJKbwV_7rvCOmw@mail.gmail.com>
Hi,

On 31/05/2017 11:34, Virgile Prevosto wrote:
> Dear list,
> 
> it is with utmost pleasure that we celebrate the 200th anniversary of
> the première of La Gazza Ladra by Gioachino Rossini at La Scala in
> Milan by announcing the release of Frama-C 15 Phosphorus.
> 
> Main changes with respect to Frama-C 14 - Silicon include:
> 
> [snip]
>

Do you still support architecture w/o native dynlink? I didn't see this
statement in the changelog whereas I get this build failure on (e.g. mips)
when I try to compile Frama-C:

configure: *******************************************************
configure: * CONFIGURE TOOLS AND LIBRARIES USED BY SOME PLUG-INS *
configure: *******************************************************
Ocamlfind -> using +lablgtk2.(/usr/lib/ocaml/lablgtk2,/usr/lib/ocaml/lablgtk2)
checking for /usr/lib/ocaml/lablgtk2/lablgtksourceview2.cma... yes
checking for /usr/lib/ocaml/lablgtk2/lablgnomecanvas.cma... yes
checking for /usr/lib/ocaml/lablgtk2/lablgtk.cma... yes
checking for dot... yes
configure: error: native dynlink does not work.
debian/rules:13: recipe for target 'override_dh_auto_configure' failed
make[1]: *** [override_dh_auto_configure] Error 2
make[1]: Leaving directory '/<<BUILDDIR>>/frama-c-20170501+phosphorus+dfsg'
debian/rules:65: recipe for target 'build-arch' failed
make: *** [build-arch] Error 2

So the test is the configure script goes like:

if ($OCAMLOPT -shared -linkall -o test_dynlink.cmxs test_dynlink.ml) \
  2> /dev/null ; \
then
  { $as_echo "$as_me:${as_lineno-$LINENO}: result: native dynlink works fine.
Great." >&5
$as_echo "native dynlink works fine. Great." >&6; }
else
  as_fn_error $? "native dynlink does not work." "$LINENO" 5
fi

So it tests two things at once:
- presence of a native compiler
- native dynlink

So bytecode architectures look like they are not supported anymore as well,
which is a pity.

> - Bash and Zsh completion for Frama-C options

Can you please clarify where are the completion scripts? I didn't find them
in the tarball, but maybe I was looking at the wrong place.

Regards,

-- 
Mehdi