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] Runtime problem on ARM

  • Subject: [Frama-c-discuss] Runtime problem on ARM
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Fri, 9 Aug 2013 21:54:54 +0200
  • In-reply-to: <CAHCOHQ=2x1iXmzrWYS=RRMzGkDrUSAYeqLH2=q-qe0AokVGksw@mail.gmail.com>
  • References: <CAHCOHQ=2x1iXmzrWYS=RRMzGkDrUSAYeqLH2=q-qe0AokVGksw@mail.gmail.com>
Hello,


On Fri, Aug 9, 2013 at 9:27 PM, Jerry James <loganjerry at gmail.com> wrote:

>
> Fedora recently promoted ARM to primary architecture status, which means
> that all Fedora packages are now built for i386, x86_64, and arm.
>

This is an interesting development. Is this 32-bit ARM or 64-bit ARM?


> On i386 and x86_64, the build of Frama-C Fluorine 20130601 behaves
> normally.  But on ARM, running frama-c, regardless of command line
> arguments, immediately results in this:
>
> Fatal error: exception Invalid_argument("String.sub")
>
> With a little gdb work, I have tracked that down to this code in external/
> unmarshal.ml, lines 212 to 224:
>

The problem you are encountering on ARM seems to be with a bit of
initialization code (run at start-up) in a low-level library, for a
functionality that Frama-C does not use. Therefore, a workaround is to
disable the functionality as in the attached patch. This does not seem to
cause any regression (I am on x86-64).

I have no idea what is different about the marshaling of closures on ARM.
Quick Googling does not reveal it as being either unsupported or as
operating on different principles from the other architectures.

I will forward your report to the anonymous author(s) of unmarshal.ml.

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130809/769eae70/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: disable_unmarshal_closure.patch
Type: application/octet-stream
Size: 1253 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130809/769eae70/attachment.obj>