--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on November 2018 ---
[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>