ltl does not accept state charts with transitions invoking dynamic function pointers
ID0001186: This issue was created automatically from Mantis Issue 1186. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001186 | Frama-C | Plug-in > wp | public | 2012-06-01 | 2012-06-15 |
| Reporter | nmuller | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | - |
Description :
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
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