Frama-C Bug Tracking System - Frama-C
View Issue Details
0000674Frama-CPlug-in > jessiepublic2011-01-17 16:522011-10-10 14:14
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
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. "").
[kernel] The full backtrace is:
         Raised at file "src/kernel/", line 507, characters 30-31
         Called from file "src/kernel/", line 501, characters 2-9
         Re-raised at file "src/kernel/", line 504, characters 8-9
         Called from file "src/type/", line 599, characters 39-44
         Called from file "", line 134, characters 6-20
         Called from file "src/kernel/", line 36, characters 4-20
         Called from file "src/kernel/", line 660, characters 2-9
         Called from file "src/kernel/", line 173, characters 4-8
         Plug-in jessie aborted because of internal error.
         Please report as 'crash' at
         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

2011-01-17 17:00   
When I commented out the switch statement (in which values to a field of a structure are only assigned) frama-c works fine
2011-01-17 17:05   
When I uncommented some code again I discovered that this piece of code causes the problem

2011-01-17 17:13   
It also crashes with
            case 2:
2011-01-17 17:24   
The following code crashes jessie as well

void helper() {
      case 2:
2011-04-01 15:21   

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
2011-01-17 16:52lukaszcNew Issue
2011-01-17 16:52lukaszcStatusnew => assigned
2011-01-17 16:52lukaszcAssigned To => cmarche
2011-01-17 17:00lukaszcNote Added: 0001392
2011-01-17 17:05lukaszcNote Added: 0001393
2011-01-17 17:13lukaszcNote Added: 0001394
2011-01-17 17:24lukaszcNote Added: 0001395
2011-04-01 15:21cmarcheNote Added: 0001673
2011-04-01 15:21cmarcheResolutionopen => fixed
2011-04-01 15:22cmarcheStatusassigned => resolved
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed