--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Uncaught exception



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 *)