Frama-C Bug Tracking System - Frama-C
View Issue Details
0000674Frama-CPlug-in > jessiepublic2011-01-17 16:522011-10-10 14:14
Reporterlukaszc 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
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. "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:
         http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines


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

Notes
(0001392)
lukaszc   
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
(0001393)
lukaszc   
2011-01-17 17:05   
When I uncommented some code again I discovered that this piece of code causes the problem
switch(taInst->FailResponse)
        {
            case TRIP_ALARM_FAIL_RESPONSE_HOLD:
                break;
        }
where

#define TRIP_ALARM_FAIL_RESPONSE_HOLD 2
(0001394)
lukaszc   
2011-01-17 17:13   
It also crashes with
switch(taInst->FailResponse)
        {
            case 2:
                break;
        }
(0001395)
lukaszc   
2011-01-17 17:24   
The following code crashes jessie as well

void helper() {
    switch(2)
    {
      case 2:
      break;
    }
}
(0001673)
cmarche   
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