Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001186Frama-CPlug-in > wppublic2012-06-01 13:502012-06-15 19:25
Reporternmuller 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001186: ltl does not accept state charts with transitions invoking dynamic function pointers
DescriptionWe 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
Additional Information 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
TagsNo tags attached.
Attached Filesc file icon stChart.c [^] (1,372 bytes) 2012-06-01 13:50 [Show Content]

- Relationships

-  Notes
(0003050)
nmuller (reporter)
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 (reporter)
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 (developer)
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 (reporter)
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.

- Issue History
Date Modified Username Field Change
2012-06-01 13:50 nmuller New Issue
2012-06-01 13:50 nmuller Status new => assigned
2012-06-01 13:50 nmuller Assigned To => virgile
2012-06-01 13:50 nmuller File Added: stChart.c
2012-06-01 20:16 nmuller Note Added: 0003050
2012-06-02 09:11 pascal Summary ltl 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:11 pascal Note Edited: 0003050
2012-06-05 06:40 monate Note Added: 0003052
2012-06-05 18:39 virgile Note Added: 0003054
2012-06-05 18:39 virgile Assigned To virgile => correnson
2012-06-05 18:39 virgile Category Plug-in > aoraï => Plug-in > wp
2012-06-15 19:25 monate Note Added: 0003141


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker