--- layout: fc_discuss_archives title: Message 5 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,

First, I  have modified the function (see the function below). However, the
VCs were not proved in the behavior 'one' (actually the VCs are not the
same of previous function):

1.single_value (select(float_P_float_M_AB_Ptr_1,AB_Ptr))=
single_value(select(float_P_float_M_AB_Ptr_1_0, AB_Ptr))
2.single_value (select(float_P_float_M_AB_Ptr_2,CD_Ptr))=
single_value(select(float_P_float_M_CD_Ptr_2_0, CD_Ptr))
7.single_value (select(float_P_float_M_AB_Ptr_1,AB_Ptr))=
single_value(select(float_P_float_M_AB_Ptr_1_0, AB_Ptr))
8.single_value (select(float_P_float_M_CD_Ptr_2,CD_Ptr))=
single_value(select(float_P_float_M_CD_Ptr_2_0, CD_Ptr))

@*/
extern double fabs(double x);

#define LIMIT 6.111111e-2

/*@ requires \valid(AB_Ptr) && \valid(CD_Ptr);
    @ assigns *AB_Ptr;
    @ assigns *CD_Ptr;
@ behavior zero:
    @ assumes \abs (\exact(*AB_Ptr)) > 5.235988e-2 || \abs
(\exact(*CD_Ptr)) > 5.235988e-2;
    @ assigns *AB_Ptr;
    @ assigns *CD_Ptr;
    @ ensures  \abs((\exact(*AB_Ptr)+ (5.235988e-2 - \exact(*AB_Ptr))) -
5.235988e-2) < 0.000000000000001;
    @ ensures  \abs((\exact(*CD_Ptr)+ (5.235988e-2 - \exact(*CD_Ptr))) -
5.235988e-2) < 0.000000000000001;
@ behavior one:
    @ assumes \abs((\exact(*AB_Ptr)+ (5.235988e-2 - \exact(*AB_Ptr))) -
5.235988e-2) < 0.000000000000001 &&
          (\abs((\exact(*CD_Ptr)+ (5.235988e-2 - \exact(*CD_Ptr))) -
5.235988e-2) < 0.000000000000001);
    @ ensures \old(*AB_Ptr) == *AB_Ptr;
    @ ensures \old(*CD_Ptr) == *CD_Ptr;
    @ ensures  \abs((\exact(*AB_Ptr)+ (5.235988e-2 - \exact(*AB_Ptr))) -
5.235988e-2) < 0.000000000000001;
    @ ensures  \abs((\exact(*CD_Ptr)+ (5.235988e-2 - \exact(*CD_Ptr))) -
5.235988e-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);
    }
}

I didn?t understand why I need to put the assigns in the default behavior.
What is the problem?

Thanks.



2012/5/3 Lo?c Correnson <loic.correnson at cea.fr>

> Hi,
> Maybe the problem comes from the different assigns clauses in each
> behavior (to be confirmed).
> You may try the following :
>  - put the weaker assigns clauses in default behavior  (assigns *AB_Ptr,
> *CD_ptr)
>  - in behavior "one", turn the assign-nothing clause into ensures
> \old(*AB_Ptr) = *AB_ptr (resp. CD_Ptr)
> Regards,
>        L.
>
>
> Le 2 mai 12 ? 21:14, Rovedy Aparecida Busquim e Silva a ?crit :
>
>  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
>>
>>
>> ______________________________**_________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.**inria.fr<Frama-c-discuss at lists.gforge.inria.fr>
>> http://lists.gforge.inria.fr/**cgi-bin/mailman/listinfo/**frama-c-discuss<http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss>
>>
>
>
> ______________________________**_________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.**inria.fr<Frama-c-discuss at lists.gforge.inria.fr>
> http://lists.gforge.inria.fr/**cgi-bin/mailman/listinfo/**frama-c-discuss<http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120503/87982a0b/attachment.html>