--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New Frama-C version: Fluorine



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>