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