Hi David, I have submitted the v2 patch of the model strnlen on the patch list. However, during testing I identified two significant limitations: 1) Partailly Initialization: For a buf[16], where only buf[0] is set, model-> read_bytes (...) fails to flag uninitialized read at buf[1]. 2) Symbolic constraints: In test_abstract, the analyzer returns UNKNOWN for (length <= n), I am thinking whether its my path failure logic? Can you guide me for this?
I would like to propose a 350 hours GSoC project. My aim is to expand the analyzers coverage of POSIX string and memory functions. My aim is to implement 8 core functions and 3 additional once if time permits, also TODO list resolution in string testsuite. Core function: memccpy, mempcpy, stpcpy, stpncpy, strncat, strcspn, strspn, strpbrk. If time persists: memmove, strtok_r, strsignal. TODO List implementation of strcpy-4.c, strcpy-1.c, strdup-1.c, strlen-1.c. I want your guidance if those implementations are sufficient for a 350 hrs. Your sincerely, Saish Kambali.
