Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2033

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

Attachments

  • stChart.c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking