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] I wrote a blog post about my experiences with Frama-C so far

Hi Tomas,
Thanks a lot for sharing your experience !
I'm just wondering how you stressed WP with strings :-) because, basically, modelling for string literals are supposed to be fairly implemented, eg:

$ less str.i
void foo() {
  char *a = "abc";
  char *b = "abc";
  char *c = "def";
  //@ assert \valid_read(a+(0..3));
  //@ assert !\valid(a+(0..3));
  //@ assert \separated({a,b},c);
  //@ assert \forall integer k; 0 <= k <= 3 ==> a[k] == b[k];
}
$ frama-c -wp str.i
[kernel] Parsing str.i (no preprocessing)
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] Proved goals:    4 / 4
  Qed:             0  (0.49ms-1ms-1ms)
  Alt-Ergo:        4  (18ms-24ms) (51)

(\separated(a,b) can not be proved, it is compiler dependent).

So, if you faced problems with strings, there might be some bug somewhere that we should investigate !
Regards,
	L.



> Le 21 nov. 2018 à 12:01, Tomas Härdin <tjoppen at acc.umu.se> a écrit :
> 
> Hi
> 
> As I've written earlier on this list, I'm still a beginner. But I think
> someone might still find my experiences so far useful, so I decided to
> document them:
> 
> http://www.härdin.se/blog/2018/11/20/trying-out-frama-c/
> 
> TL;DR: I've been just as successful with Frama-C as SPARK, but aliasing
> has been causing grief. I didn't get that far earlier because I don't
> know enough Ada to mess around with strings or arrays.
> 
> /Tomas
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181126/887e5f33/attachment.html>