Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
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

- Relationships

-  Notes
(0001392)
lukaszc (reporter)
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 (reporter)
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 (reporter)
2011-01-17 17:13

It also crashes with
switch(taInst->FailResponse)
        {
            case 2:
                break;
        }
(0001395)
lukaszc (reporter)
2011-01-17 17:24

The following code crashes jessie as well

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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker