--- layout: fc_discuss_archives title: Message 22 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



mån 2018-11-26 klockan 11:38 +0100 skrev Loïc Correnson:
> Hi Tomas,
> Thanks a lot for sharing your experience !
> I'm just wondering how you stressed WP with strings :-)

There's a number of things, but what caused me the most grief was
tokenizing a string like "foo bar doot" into char terms[128][128],
using strcspn().

I was actually able to get so far as strcspn() either giving me zero
length (if at end of string, or a space), or a proper string, and loop
variant strlen(remaning_string) always decreasing, assigns clauses
being fulfilled.. All that good stuff. But as soon as I assign
terms[][] it gets massively confused.

I've tried things like putting \separated loop invariants for all char*
involved, only ever assigning terms[0][0] = 0 (so I can at least say
valid_string((char*)terms)) and other stuff. WP is even able to reason
that \separated indeed holds, until I go assigning terms. And yes, I
have loop assigns ((char*)terms)[0..(sizeof(terms)-1)];

Just a simple thing like strcspn(str, " ") thinking " " can alias str
despite str being char * restrict.

> 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).

Indeed, but char a[4] = "abc", b[4] = "abc" should work.

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

Perhaps I can come up with a minimal example..

/Tomas