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