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 ## Attachments - [stChart.c](/uploads/78d55a097c8cda08c31e8f3a3946338d/stChart.c)