--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on May 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plugin



Hi,

I am studying Frama-C with a real case study. I have some questions about
Jessie.
The Alt-Ergo 0.91, Simplify 1.5.4, Z3 2.19, CVC2.2, and Gappa 0.15.0 are
installed.

//
-------------------------------------------------------------------------------------------------------------
1) I would like to use behavior specification (see the function below). But
I couldn?t prove the Vcs
related with the behavior one:

3 - not_assigns(float_P_AB_Ptr_1_alloc_table,
float_P_float_M_AB_Ptr_1,float_P_float_M_AB_Ptr_1_0, pset_empty)
4 - not_assigns(float_P_CD_Ptr_2_alloc_table,
float_P_float_M_CD_Ptr_2,float_P_float_M_CD_Ptr_2_0, pset_empty)
11- not_assigns(float_P_AB_Ptr_1_alloc_table,
float_P_float_M_AB_Ptr_1,float_P_float_M_AB_Ptr_1_0, pset_empty)
12- not_assigns(float_P_CD_Ptr_2_alloc_table,
float_P_float_M_CD_Ptr_2,float_P_float_M_CD_Ptr_2_0, pset_empty)

I didn't understand the problem. If I don?t use behavior , I have all the
proven VCs.


/*@ assigns \nothing;
  @ ensures \result == \abs(x);
@*/
extern double fabs(double x);

#define LIMIT 6.111111e-2

/*@ requires \valid(AB_Ptr) && \valid(CD_Ptr);
@ behavior zero:
    @ assumes \abs (\exact(*AB_Ptr)) > 6.111111e-2 || \abs
(\exact(*CD_Ptr)) > 6.111111e-2;
    @ assigns *AB_Ptr;
    @ assigns *CD_Ptr;
    @ ensures  \abs((\exact(*AB_Ptr)+ (6.111111e-2 - \exact(*AB_Ptr))) -
6.111111e-2) < 0.000000000000001;
    @ ensures  \abs((\exact(*CD_Ptr)+ (6.111111e-2 - \exact(*CD_Ptr))) -
6.111111e-2) < 0.000000000000001;
@ behavior one:
    @ assumes \abs((\exact(*AB_Ptr)+ (6.111111e-2 - \exact(*AB_Ptr))) -
6.111111e-2) < 0.000000000000001 &&
          (\abs((\exact(*CD_Ptr)+ (6.111111e-2 - \exact(*CD_Ptr))) -
6.111111e-2) < 0.000000000000001);
    @ assigns \nothing;
    @ ensures  \abs((\exact(*AB_Ptr)+ (6.111111e-2 - \exact(*AB_Ptr))) -
6.111111e-2) < 0.000000000000001;
    @ ensures  \abs((\exact(*CD_Ptr)+ (6.111111e-2 - \exact(*CD_Ptr))) -
6.111111e-2) < 0.000000000000001;
@ */
void limitValue(float *AB_Ptr, float *CD_Ptr)
{
double Fabs_AB, Fabs_CD;
double max;

    Fabs_AB = fabs (*AB_Ptr);
    Fabs_CD = fabs (*CD_Ptr);
    max = Fabs_AB;

    if (Fabs_CD > Fabs_AB)
       max = Fabs_CD;

    if ( max > LIMIT)
    {
    *AB_Ptr = (float) (((*AB_Ptr) * LIMIT) / max);
    *CD_Ptr = (float) (((*CD_Ptr) * LIMIT) / max);
    }
}

The function without behavior:

/*@ assigns \nothing;
  @ ensures \result == \abs(x);
@*/
extern double fabs(double x);

#define LIMIT 6.111111e-2

/*@ requires \valid(AB_Ptr) && \valid(CD_Ptr);
  @ assigns *AB_Ptr;
  @ assigns *CD_Ptr;
  @ ensures  \abs((\exact(*AB_Ptr)+ (6.111111e-2 - \exact(*AB_Ptr))) -
6.111111e-2) < 0.000000000000001;
  @ ensures  \abs((\exact(*CD_Ptr)+ (6.111111e-2 - \exact(*CD_Ptr))) -
6.111111e-2) < 0.000000000000001;
 */
void limitValue(float *AB_Ptr, float *CD_Ptr)
{
double Fabs_AB, Fabs_CD;
double max;

    Fabs_AB = fabs (*AB_Ptr);
    Fabs_CD = fabs (*CD_Ptr);
    max = Fabs_AB;

    if (Fabs_CD > Fabs_AB)
       max = Fabs_CD;

    if ( max > LIMIT)
    {
    *AB_Ptr = (float) (((*AB_Ptr) * LIMIT) / max);
    *CD_Ptr = (float) (((*CD_Ptr) * LIMIT) / max);
    }
}

//-------------------------------------------------------------------------------------------------------------

2) How do I write a specification to verify the validity of pointer to an
array of structure?

Example:
filter *filter_Ptr[3];

typedef struct
{  float F_K;
   float F_A;
   float F_B1;
} filter;

The variable filter_Ptr is global.


//-------------------------------------------------------------------------------------------------------------

3) How do I write a requires and assigns specification for a
two-dimensional array?

//-------------------------------------------------------------------------------------------------------------

4) I have a function responsible for initializing values. It has no input
parameters. All variables used in the function are global.
In this case, should I put as a pre condition to the validity of pointers
and arrays?

//-------------------------------------------------------------------------------------------------------------

5) In the previous function, I would like to write assigns specifications.
However, the VCS aren?t proved.
The variables are global. what is the problem?

Example:

float Pane [7];
unsigned Sc [7] [3];
float * Tab__Ptr[9];
filter * filter_Ptr[3];


/* @ assigns Pane[0 .. 7-1];
  @ assigns Tab_Ptr[0 .. 9-1];
  @ assigns filter_Ptr[0 .. 3-1];
 */

//-------------------------------------------------------------------------------------------------------------
6) Is there a way to count the number of VCs generated by type (eg 188
poscondition, 50 precondition ...) without being visually?
I searched this information in the directory files generated by jessie but
not found.


Thanks a lot.

Best regards,
Rovedy
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120502/94ea3f55/attachment.html>