What is the proper way to use this function?
crt uobjrtl function implementations and specifications are explicitly designed to work with the uberSpark verification process and will obey their functional correctness specifications as written.
As you can see from the speficiation of
uobjrtl/crt/src/strlen.c) , the
requires clause uses the
Length_of_str_is predicate. This predicate is defined within
uobjrtl/crt/include/string.h and establishes the validity of the input string memory locations, the final
NULL termination character, and returns the length of the string.
This predicate allows us to verify the functional correctness of strlen implementation separately via deductive verification using weakest precondition calculus.
Further, the sources to strlen along with the function contract is passed through to the uobject memory value analysis phase where abstract interpretation is used to verify valid memory accesses of the entire uobject (including invoking strlen if present). This phase will trigger an error if the
requires clause of strlen is not satisfied (e.g., by passing to a malformed string buffer to strlen, the validity of whose memory locations and resulting length cannot be established).
So, if the uobject memory access verification phase succeeeds, it means there are only valid uses of strlen. If there an invalid uses of strlen, the verification phase will report an error.
So, use strlen with a valid string buffer with valid length within a uobject so that the verification can succeed.
Examples of accesses which will pass verification follow:
int mylen; mylen = uberspark_uobjrtl_crt__strlen("hello world");
int mylen; char buf; uberspark_uobjrtl_crt__strcpy(buf, "hello"); mylen = uberspark_uobjrtl_crt__strlen(buf);
Hope this helps.
Thanks! In the two code examples, do I need to check mylen >=0 before using it? If I understand it correctly, I do not need to do it in uxmhf or uspark because they’ll be verified
You are correct. If you used either of the above two approaches, this should pass verification.
Well if the string is of length 0, then mylen will be 0, else it will be the length of the string.