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
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

- Relationships

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

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

The following code crashes jessie as well void helper() { switch(2) { case 2: break; } }
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker