2021-01-26 06:58 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001186Frama-CPlug-in > wppublic2012-06-15 19:25
Reporternmuller 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
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 Files
  • c file icon stChart.c (1,372 bytes) 2012-06-01 13:50 -
    #include <stdio.h>
    int f1()
    {
    printf("function 1\n");
    }
    int f2()
    {
    printf("function 2\n");
    }
    int f3()
    {
    printf("function 3\n");
    }
    int f41()
    {
    printf("function 4 from state 1\n");
    }
    int f42()
    {
    printf("function 4 from state 2\n");
    }
    int f43()
    {
    printf("function 4from state 3\n");
    }
    int f44()
    {
    printf("function 4 from state 4\n");
    }
    int f5()
    {
    printf("function 5\n");
    }
    
    void main()
    {
    
    typedef struct tt
    {
    void * pfunc;
    int targetState;
    } tTransCell;
    
    tTransCell Trans[][6] =
    {
    {{0,0}, {0,0}, {0,0}, {0,0}, {0,0}},
    {{f1,1}, {f1,2}, {f1,3}, {f1,4}, {f1,0}},
    {{0,1}, {0,2}, {0,3}, {f2,4}, {f2,0}},
    {{f3,1}, {f3,2}, {f3,3}, {f3,4}, {f3,0}},
    {{f41,1}, {f42,2}, {f43,3}, {f44,4}, {f41,0}},
    {{0,1}, {f5,2}, {0,3}, {f5,4}, {0,0}}
    };
    
    int trans;
    int curState=0; // etat initial
    void (*fpointer)();
    void * pt;
    
    while (1)
    {
    printf("entrez le numero de la transition (uniquement une valeur numerique) :");
    //getc(trans);
    scanf("%d", &trans);
    
    if (trans == 0) {break;}
    printf("transition executee %d ", trans);
    printf("a partir de l etat %d\n ", curState);
    
    pt = Trans[trans][curState].pfunc;
    if (pt == 0)
    {
    int ptt;
    printf("transition interdite\n");
    ptt = 5*4+2-8;
    }
    else
    {
    fpointer = pt;
    //@ assert (fpointer == pt);
    curState = Trans[trans][curState].targetState;
    //@ assert (curState == Trans[trans][curState].targetState);
    printf("nouvel état %d\n",curState);
    fpointer();
    }
    }
    
    }
    
    c file icon stChart.c (1,372 bytes) 2012-06-01 13:50 +

-Relationships
+Relationships

-Notes

~0003050

nmuller (reporter)

Last edited: 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)

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)

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)

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.
+Notes

-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
+Issue History