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: loganjerry at (Jerry James)
  • Date: Fri, 9 Aug 2013 13:27:29 -0600


Fedora recently promoted ARM to primary architecture status, which means
that all Fedora packages are now built for i386, x86_64, and arm.  I am
having a problem with the frama-c package that I'm having some difficulty
figuring out.  I am hopeful that somebody here can give me some advice.

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/, lines 212 to 224:

let (code_area_start, cksum) =
  let s = Marshal.to_string id [Marshal.Closures] in
  let cksum = String.sub s 0x1E 16 in
  let c0 = Char.code s.[0x1D] in
  let c1 = Char.code s.[0x1C] in
  let c2 = Char.code s.[0x1B] in
  let c3 = Char.code s.[0x1A] in
  let ofs = Int32.logor (Int32.shift_left (Int32.of_int c3) 24)
                        (Int32.of_int ((c2 lsl 16) lor (c1 lsl 8) lor c0))
  let start = Obj.add_offset (Obj.field (Obj.repr id) 0) (Int32.neg ofs) in
  (start, cksum)

If I am reading the GDB information correctly, the variable s is a pointer
to a block of 0 bytes (a zero-length string?).

I would be grateful for any ideas on how to proceed.  Regards,
Jerry James
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>