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

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>