Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plugin

  • Subject: [Frama-c-discuss] Jessie plugin
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Wed, 2 May 2012 16:14:55 -0300
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>