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] Code proved with Fluorine is more proved with Neon

This code is quite cryptic at a first sight, and I personally don?t have time to look at it deeply.
As a recommandation, may I suggest you to insert intermediate assertions in the code to find where the proof does not work?
Start by copying the ensures into assertions at the end of each branch, then try to infer some intermediate results.
	L.


Le 27 mai 2014 ? 10:36, Christophe Garion <christophe.garion at isae.fr> a ?crit :

> Hello,
> 
> I have some code that was proved with the Fluorine version of Frama-C
> and is no more proved using Neon. A simplified version of the code is
> available in the test_po_time_double_behavior_1.c file. I have tried to
> write the code differently, see test_po_time_double_behavior_2.c and
> test_po_time_double_behavior_3.c (notice also that one postcondition in
> test_po_time_double_behavior_3.c cannot be proved with Fluorine). But
> Neon cannot prove one of the postcondition in a behavior in all files.
> 
> Frama-C and Alt-Ergo were installed via opam and I use the following
> command line :
> 
> frama-c -pp-annot -wp -wp-timeout 60 file.c
> 
> z3 4.3.1 via why3 seems to prove all the assertions under Neon, so it
> may be an Alt-Ergo problem.
> 
> I will look at the generated mlw files by both Frama-C versions, but is
> there something obvious I have missed?
> 
> Thanks in advance,
> 
> Christophe
> 
> --
> Christophe Garion          ISAE/DMIA - SUPAERO/IN
> garion at isae.fr             10 avenue Edouard Belin
> T?l : (33)5 61 33 80 57    BP 54032
> Fax : (33)5 61 33 83 45    31055 Toulouse Cedex 4
> 
> #include <stdint.h>
> 
> typedef struct
> {
>   uint32_t     sec;     /* amount of second     */
>   uint32_t     nsec;    /* amount of nanosecond */
> } my_time;
> 
> /*@
>  @ predicate is_time_struct_correct(my_time *mytime) =
>  @   mytime->sec >= 0 && mytime->sec <= UINT32_MAX &&
>  @   mytime->nsec >= 0 && mytime->nsec < 1000000000;
>  @*/
> 
> /*@ requires \valid(result);
>  @ requires \valid(left);
>  @ requires \valid(right);
>  @ requires is_time_struct_correct(left);
>  @ requires is_time_struct_correct(right);
>  @ requires right->sec + left->sec <= UINT32_MAX - 1;
>  @ requires \separated(result, left, right);
>  @ assigns result->sec, result->nsec;
>  @ behavior nsec_sum_higher_than_1s:
>  @   assumes left->nsec + right->nsec >= 1000000000;
>  @   ensures result->sec == left->sec + right->sec + 1;
>  @   ensures result->nsec == left->nsec + right->nsec - 1000000000;
>  @   ensures is_time_struct_correct(result);
>  @ behavior nsec_sum_less_than_1s:
>  @   assumes left->nsec + right->nsec < 1000000000;
>  @   ensures result->sec == left->sec + right->sec;
>  @   ensures result->nsec == left->nsec + right->nsec;
>  @   ensures is_time_struct_correct(result);
>  @ complete behaviors;
>  @ disjoint behaviors;
>  @*/
> void add_times(my_time* result, const my_time* left, const my_time* right)
> {
>    result->sec = left->sec + right->sec;
>    result->nsec = left->nsec + right->nsec;
> 
>    if (result->nsec >= 1000000000) {
>        result->sec  = result->sec + 1;
>        result->nsec = result->nsec - 1000000000;
>    }
> }
> #include <stdint.h>
> 
> typedef struct
> {
>   uint32_t     sec;     /* amount of second     */
>   uint32_t     nsec;    /* amount of nanosecond */
> } my_time;
> 
> /*@
>  @ predicate is_time_struct_correct(my_time *mytime) =
>  @   mytime->sec >= 0 && mytime->sec <= UINT32_MAX &&
>  @   mytime->nsec >= 0 && mytime->nsec < 1000000000;
>  @*/
> 
> /*@ requires \valid(result);
>  @ requires \valid(left);
>  @ requires \valid(right);
>  @ requires is_time_struct_correct(left);
>  @ requires is_time_struct_correct(right);
>  @ requires right->sec + left->sec <= UINT32_MAX - 1;
>  @ requires \separated(result, left, right);
>  @ assigns result->sec, result->nsec;
>  @ behavior nsec_sum_higher_than_1s:
>  @   assumes left->nsec + right->nsec >= 1000000000;
>  @   ensures result->sec == left->sec + right->sec + 1;
>  @   ensures result->nsec == left->nsec + right->nsec - 1000000000;
>  @   ensures is_time_struct_correct(result);
>  @ behavior nsec_sum_less_than_1s:
>  @   assumes left->nsec + right->nsec < 1000000000;
>  @   ensures result->sec == left->sec + right->sec;
>  @   ensures result->nsec == left->nsec + right->nsec;
>  @   ensures is_time_struct_correct(result);
>  @ complete behaviors;
>  @ disjoint behaviors;
>  @*/
> void add_times(my_time* result, const my_time* left, const my_time* right)
> {
>    uint32_t aux_sec = left->sec + right->sec;
>    uint32_t aux_nsec = left->nsec + right->nsec;
> 
>    if (aux_nsec >= 1000000000) {
>        result->sec  = aux_sec + 1;
>        result->nsec = aux_nsec - 1000000000;
>    } else {
>        result->sec  = aux_sec;
>        result->nsec = aux_nsec;
>    }
> }
> #include <stdint.h>
> 
> typedef struct
> {
>   uint32_t     sec;     /* amount of second     */
>   uint32_t     nsec;    /* amount of nanosecond */
> } my_time;
> 
> /*@
>  @ predicate is_time_struct_correct(my_time *mytime) =
>  @   mytime->sec >= 0 && mytime->sec <= UINT32_MAX &&
>  @   mytime->nsec >= 0 && mytime->nsec < 1000000000;
>  @*/
> 
> /*@ requires \valid(result);
>  @ requires \valid(left);
>  @ requires \valid(right);
>  @ requires is_time_struct_correct(left);
>  @ requires is_time_struct_correct(right);
>  @ requires right->sec + left->sec <= UINT32_MAX - 1;
>  @ requires \separated(result, left, right);
>  @ assigns result->sec, result->nsec;
>  @ behavior nsec_sum_higher_than_1s:
>  @   assumes left->nsec + right->nsec >= 1000000000;
>  @   ensures result->sec == left->sec + right->sec + 1;
>  @   ensures result->nsec == left->nsec + right->nsec - 1000000000;
>  @   ensures is_time_struct_correct(result);
>  @ behavior nsec_sum_less_than_1s:
>  @   assumes left->nsec + right->nsec < 1000000000;
>  @   ensures result->sec == left->sec + right->sec;
>  @   ensures result->nsec == left->nsec + right->nsec;
>  @   ensures is_time_struct_correct(result);
>  @ complete behaviors;
>  @ disjoint behaviors;
>  @*/
> void add_times(my_time* result, const my_time* left, const my_time* right)
> {
>    uint32_t aux_sec = left->sec + right->sec;
>    uint32_t aux_nsec = left->nsec + right->nsec;
> 
>    if (aux_nsec < 1000000000) {
>        result->sec  = aux_sec;
>        result->nsec = aux_nsec;
>    } else {
>        result->sec  = aux_sec + 1;
>        result->nsec = aux_nsec - 1000000000;
>    }
> }
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss