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] Uncaught exception

  • Subject: [Frama-c-discuss] Uncaught exception
  • From: tomahawkins at gmail.com (Tom Hawkins)
  • Date: Thu, 6 May 2010 16:42:01 -0500
And a third question.  What could be causing this exception?  (I got a
little too ambitious and threw Frama-C our entire embedded design.)

e0082888 at e0082888-laptop:~/eaton/bus$ make verify
frama-c -jessie stubs.c can.c controls.c evu.c function.c interface.c
probes.c probing.c scheduler.c sensors.c swash.c utils.c vehicle.c
[kernel] preprocessing with "gcc -C -E -I.  -dD stubs.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD can.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD controls.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD evu.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD function.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD interface.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD probes.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD probing.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD scheduler.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD sensors.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD swash.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD utils.c"
[kernel] preprocessing with "gcc -C -E -I.  -dD vehicle.c"
stubs.c:5:[kernel] warning: Incompatible declaration for
ModuleSupport_Reset (included from  stubs.c).
                  Previous was at controls.c:55 (include from controls.c)
                  (different type constructors: int  vs. void )]
stubs.c:6:[kernel] warning: Incompatible declaration for CANA_Transmit
(included from  stubs.c). Previous
                  was at mototron.h:4 (include from can.c)
                  (different type constructors: unsigned char  vs. void )]
[jessie] Starting Jessie translation
[kernel] No code for function faults, default assigns generated
function.c:20:[jessie] warning: skipping all arguments of implicit
prototype faults
[jessie] Producing Jessie files in subdir wholeprogram.jessie
[jessie] File wholeprogram.jessie/wholeprogram.jc written.
[jessie] File wholeprogram.jessie/wholeprogram.cloc written.
[jessie] Calling Jessie tool in subdir wholeprogram.jessie
Generating Why function recv
Generating Why function vehicle
File "jc/jc_interp.ml", line 1756, characters 13-13:
Uncaught exception: File "jc/jc_interp.ml", line 1756, characters
13-19: Assertion failed
[jessie] user error: Jessie subprocess failed:   jessie  -why-opt
-split-user-conj  -v       -locs wholeprogram.cloc wholeprogram.jc




And the problem area in jc_interp.ml reads:

1751 and make_upd_bytes mark pos e1 fi tmp2 =
1752   let e1' = expr e1 in
1753   (* Convert value assigned into bitvector *)
1754   let e2' = match fi.jc_field_info_type with
1755     | JCTenum ri -> make_app (logic_bitvector_of_enum ri) [Var tmp2]
1756     | _ty -> assert false (* TODO *)