[ldv-project] Verification tasks that depend on strings

[Evgeny Novikov]

Hi Dirk,

I prepared very simple verification tasks in accordance with Linux 
kernel API usage rules. These tasks are based on basic string 
operations. But this is just for start. Then we will need to 
compare/copy/etc. strings or buffers and perform similar checks for all 
operations.

I don't insist on suggested names like __VERIFIER_buflen and so on! I 
hope that you will think out more correct ones.

At last we shouldn't forget about Z3-str 
(https://www.cs.purdue.edu/homes/zheng16/str/). From its test cases one 
can easily build C programs with corresponding reachability problems.

-- 
Best regards, Evgeny Novikov.
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: novikov at ispras.ru

-------------- next part --------------
A non-text attachment was scrubbed...
Name: string_verification_tasks.tar.bz2
Type: application/x-bzip
Size: 800 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20131115/ec156c41/attachment.bin>