--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on May 2010 ---
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 *)