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] New Frama-C version: Fluorine

  • Subject: [Frama-c-discuss] New Frama-C version: Fluorine
  • From: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Fri, 19 Apr 2013 15:41:55 +0200
  • In-reply-to: <CAEt_dEohQ_aL9UhxzmAN=1reSMwWewwuXFERnAaPFh2ft7tu0w@mail.gmail.com>
  • References: <CAEt_dEohQ_aL9UhxzmAN=1reSMwWewwuXFERnAaPFh2ft7tu0w@mail.gmail.com>
Thanks for the bug report.
Current status :

1. pointer comparison is actually missing in Why3 resources ;
2. pointer difference is incorrectly translated in WP ;
3. pointer comparison requires pointers to have the same base, which is actually missing in your loop invariant, but can be proved.
4. It seems that Alt-Ergo has some difficulties in guessing the final existential. An intermediate assertion with the witness solves the problem.

I guess your axiomatic definitions are something like :

/*@ 
  axiomatic String {

  predicate Length_of_str_is(char * s,integer n) =
   0 <= n &&
    \valid( s + (0..n) ) &&
    s[n] == 0 &&
    \forall integer k ; 0 <= k < n ==> s[k] !=0
  ;

  logic integer Length{L}(char *s) reads s[..] ;

  axiom Length_def :
    \forall char *s;
    \forall integer n; 
       Length_of_str_is(s,n) ==> Length(s)==n ;

  }
*/

Things to be added for points 3 and 4 : loop invariant BASE and assertion END, below:

/*@
   requires \exists integer i; Length_of_str_is(s,i);
   assigns \nothing;
   ensures \exists integer i; Length_of_str_is(s,i) && \result == i;
 @*/
int strlen(const char *s) {
  const char *ss = s;
  /*@
      loop invariant BASE: \base_addr(s) == \base_addr(ss) ;
      loop invariant RANGE: s <= ss <= s+Length(s);
      loop invariant ZERO: \forall integer i; 0 <= i < (ss-s) ==> s[i] != 0;
      loop assigns ss;
      loop variant Length(s) + (s-ss) ;
   @*/
  while (*ss)
    ss++;

  /*@ assert END: Length_of_str_is(s,ss-s); */
  return ss - s;
}

frama-c -wp addr.i -wp-par 1
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 14 goals scheduled
[wp] [Alt-Ergo] Goal typed_strlen_post : Valid (Qed:1ms) (57ms) (32)
[wp] [Qed] Goal typed_strlen_loop_inv_BASE_preserved : Valid (1ms)
[wp] [Qed] Goal typed_strlen_loop_inv_BASE_established : Valid
[wp] [Alt-Ergo] Goal typed_strlen_loop_inv_RANGE_preserved : Valid (Qed:2ms) (215ms) (57)
[wp] [Alt-Ergo] Goal typed_strlen_loop_inv_RANGE_established : Valid (Qed:1ms) (103ms) (30)
[wp] [Alt-Ergo] Goal typed_strlen_loop_inv_ZERO_preserved : Valid (Qed:1ms) (131ms) (44)
[wp] [Qed] Goal typed_strlen_loop_inv_ZERO_established : Valid
[wp] [Alt-Ergo] Goal typed_strlen_assert_END : Valid (Qed:1ms) (192ms) (55)
[wp] [Qed] Goal typed_strlen_loop_assign : Valid
[wp] [Qed] Goal typed_strlen_assign_part1 : Valid
[wp] [Qed] Goal typed_strlen_assign_part2 : Valid
[wp] [Qed] Goal typed_strlen_assign_part3 : Valid (1ms)
[wp] [Qed] Goal typed_strlen_loop_term_decrease : Valid (1ms)
[wp] [Alt-Ergo] Goal typed_strlen_loop_term_positive : Valid (Qed:2ms) (77ms) (39)


Regards,
	L.

  


Le 19 avr. 2013 ? 13:05, Cristiano Sousa a ?crit :

> I'm very excited in finally having a new version of frama-c.
> 
> Installation went smooth, and the first thing I did was checking POs of the project I'm currently am working on.
> 
> The new memory model seems powerfull, sadly I cannot prove a simple function using alt-ergo (previously i could), and also cannot use why3 as it returns an error related to unbound variables:
> 
> File "/Users/xxxxx/.frama-c-wp/typed/Axiomatic.why", line 16, characters 8-11: unused variable x_0
> 
> http://pastebin.com/JZHEskC5
> 
> 
> Error while reading file '../typed/strlen_Why3_ide.why': File "/Users/xxxxx/.frama-c-wp/project.session/../typed/strlen_Why3_ide.why", line 36, characters 4-11: Unbound symbol 'addr_le'
> 
> http://pastebin.com/hxzBu0xw
> 
> 
> function: http://pastebin.com/ahvWeYXh
> 
> 
> -- 
> Regards,
> Cristiano Sousa
> _______________________________________________
> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130419/b17f4084/attachment-0003.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: addr.i
Type: application/octet-stream
Size: 919 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130419/b17f4084/attachment-0002.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130419/b17f4084/attachment-0004.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: wp.patch
Type: application/octet-stream
Size: 8220 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130419/b17f4084/attachment-0003.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130419/b17f4084/attachment-0005.html>