Frama-C Bug Tracking System - Frama-C
View Issue Details
0001186Frama-CPlug-in > wppublic2012-06-01 13:502012-06-15 19:25
nmuller 
correnson 
normalminoralways
assignedopen 
Frama-C Nitrogen-20111001 
 
0001186: ltl does not accept state charts with transitions invoking dynamic function pointers
We have implemented a general purpose small code allowing to represent any possible state chart. This code is based on a table which contains pointers to functions to be called per origin state and allowed transition. But frama-c seems not to be able to accept the dynamic pointers
frama-c -wp -wp-proof alt-ergo stChart.c [kernel] preprocessing with "gcc -C -E -I. stChart.c" stChart.c:4:[kernel] warning: Body of function f1 falls-through. Adding a return statement stChart.c:8:[kernel] warning: Body of function f2 falls-through. Adding a return statement stChart.c:12:[kernel] warning: Body of function f3 falls-through. Adding a return statement stChart.c:16:[kernel] warning: Body of function f41 falls-through. Adding a return statement stChart.c:20:[kernel] warning: Body of function f42 falls-through. Adding a return statement stChart.c:24:[kernel] warning: Body of function f43 falls-through. Adding a return statement stChart.c:28:[kernel] warning: Body of function f44 falls-through. Adding a return statement stChart.c:32:[kernel] warning: Body of function f5 falls-through. Adding a return statement [kernel] warning: No code for function printf, default assigns generated stChart.c:83:[wp] warning: call through function pointer not implemented yet: ignore called function properties. [kernel] warning: No code for function scanf, default assigns generated [wp] warning: Missing RTE guards [wp] warning: Use -wp-warnings for details about 'Stronger' and 'Degenerated' goals [wp] warning: Stronger goal store_main_assert_1 (24 warnings) [wp] warning: Stronger goal store_main_assert_2 (24 warnings) Erreur de segmentation
No tags attached.
c stChart.c (1,372) 2012-06-01 13:50
https://bts.frama-c.com/file_download.php?file_id=389&type=bug
Issue History
2012-06-01 13:50nmullerNew Issue
2012-06-01 13:50nmullerStatusnew => assigned
2012-06-01 13:50nmullerAssigned To => virgile
2012-06-01 13:50nmullerFile Added: stChart.c
2012-06-01 20:16nmullerNote Added: 0003050
2012-06-02 09:11pascalSummaryltl does accept state charts with transitions invoking dynamic function pointers => ltl does not accept state charts with transitions invoking dynamic function pointers
2012-06-02 09:11pascalNote Edited: 0003050
2012-06-05 06:40monateNote Added: 0003052
2012-06-05 18:39virgileNote Added: 0003054
2012-06-05 18:39virgileAssigned Tovirgile => correnson
2012-06-05 18:39virgileCategoryPlug-in > aoraï => Plug-in > wp
2012-06-15 19:25monateNote Added: 0003141

Notes
(0003050)
nmuller   
2012-06-01 20:16   
(edited on: 2012-06-02 09:11)
Correction : the title is in fact : frama-c does NOT accept state charts where transitions are implemented through dynamic function pointers [EDIT: I have updated the title -- Pascal]
(0003052)
monate   
2012-06-05 06:40   
I see no ltl nor any link with aoraï in your issue. It seems related to WP plugin but won't be noticed as such as long it is associated with Aoraï. @Virgile : can you confirm and reassign accordingly?
(0003054)
virgile   
2012-06-05 18:39   
I confirm that the bug reported here only speaks about WP. The issue with pointer function seems to be resolved in current svn, but wp does not handle the file. with default model (rev. 18704), it ends up with: [wp] warning: Missing RTE guards stChart.c:86:[wp] warning: Missing assigns clause (assigns 'everything' instead) stChart.c:62:[wp] warning: Missing assigns clause (assigns 'everything' instead) [wp] warning: Use -wp-warnings for details about 'Stronger' and 'Degenerated' goals [wp] warning: Stronger goal store_main_assert (20 warnings) [wp] warning: Stronger goal store_main_assert_2 (20 warnings) [kernel] The full backtrace is: Raised by primitive operation at 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 723, characters 2-9 Called from file "src/kernel/cmdline.ml", line 200, characters 4-8 Unexpected error (Stack overflow). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Nitrogen-20111001+dev. Note that a version and 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
(0003141)
monate   
2012-06-15 19:25   
Thanks for the bug report. The stack overflow issue will be fixed at some point. But this will probably not help you answer your real questions. What would you like to prove on this code? The two assertions do not seem interesting. Specifying and proving a program with function pointers using any kind of WP calculus is a very tedious task and probably still an open research problem. Do not hesitate to describe typical code and properties you would like to prove.