2021-03-05 08:23 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000674Frama-CPlug-in > jessiepublic2011-10-10 14:14
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityhave not tried
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000674: Crash
Descriptionfor command
frama-c -main TripAlarm_IsVarAlarming -lib-entry -pp-annot -cpp-extra-args="-Ilibrary -IBSP" ./library/trip_alarm.c -jessie

console output
[kernel] preprocessing with "gcc -C -E -I. -Ilibrary -IBSP -dD ./library/trip_alarm.c"
[jessie] Starting Jessie translation
[kernel] No code for function GetDataQuality, default assigns generated
[kernel] No code for function Persist_float32, default assigns generated
[kernel] No code for function Persist_int16, default assigns generated
[kernel] No code for function Persist_uint8, default assigns generated
[kernel] No code for function SeqMonitor_Process, default assigns generated
[kernel] No code for function Timer_Init, default assigns generated
[kernel] No code for function Timer_Reset, default assigns generated
[kernel] No code for function Timer_Timeout, default assigns generated
./library/trip_alarm.c:213:[jessie] failure: Unexpected failure.
                  Please submit bug report (Ref. "interp.ml:2029:18").
[kernel] The full backtrace is:
         Raised at file "src/kernel/log.ml", line 507, characters 30-31
         Called from file "src/kernel/log.ml", line 501, characters 2-9
         Re-raised at file "src/kernel/log.ml", line 504, characters 8-9
         Called from file "src/type/type.ml", line 599, characters 39-44
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 36, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 660, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 173, characters 4-8
         Plug-in jessie aborted because of internal error.
         Please report as 'crash' at http://bts.frama-c.com/
         Note that a backtrace alone often does not have information to
         understand the bug. Guidelines for reporting bugs are at:

Line 213 of trip_alarm.c is "switch(taInst->FailResponse)"
TagsNo tags attached.
Attached Files




lukaszc (reporter)

When I commented out the switch statement (in which values to a field of a structure are only assigned) frama-c works fine


lukaszc (reporter)

When I uncommented some code again I discovered that this piece of code causes the problem



lukaszc (reporter)

It also crashes with
            case 2:


lukaszc (reporter)

The following code crashes jessie as well

void helper() {
      case 2:


cmarche (developer)

This behavior does not show up in the current SVN Frama-C / Why so
I guess it was fixed as a side-effect of changing something in the Frama-C front-end

-Issue History
Date Modified Username Field Change
2011-01-17 16:52 lukaszc New Issue
2011-01-17 16:52 lukaszc Status new => assigned
2011-01-17 16:52 lukaszc Assigned To => cmarche
2011-01-17 17:00 lukaszc Note Added: 0001392
2011-01-17 17:05 lukaszc Note Added: 0001393
2011-01-17 17:13 lukaszc Note Added: 0001394
2011-01-17 17:24 lukaszc Note Added: 0001395
2011-04-01 15:21 cmarche Note Added: 0001673
2011-04-01 15:21 cmarche Resolution open => fixed
2011-04-01 15:22 cmarche Status assigned => resolved
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
+Issue History