Inspect with TrustInSoft CI Analysis(under the snippet of code) to launch TrustInSoft CI Analyzer:
\valid(buf+i)did not hold, by inspecting the variables
\valid(buf+i), then look at the Values widget (bottom):
ialong with the union of all its values until the undefined behavior was found. Since
igets incremented at each iteration of the
whileloop enclosing the undefined behavior,
itakes several values so an integer range between 1 and 33.
bufto look at its values in the Values widget:
bufis a pointer, whose value is the result of the call to
mallocin the function
caesar_encryptline 26. The memory space allocated by
mallocis represented using the symbolic notation
bufor any other expression, to see their values before and after the clicked statement in the Values widget:
iand select Track this term, then click on
bufto simultaneously inspect the values of
__malloc_caesar_encrypt_l26for each iteration of the
whileloop enclosing the undefined behavior:
i = 1, which means that the statement with the undefined behavior is first reached when
i = 1.
bufwith an offset
iequal to 33:
__malloc_caesar_encrypt_l26in the Expression column (see above screenshot) to see its type:
__malloc_caesar_encrypt_l26is an array of char of length 33
(char ). The access with an offset of 33 is therefore out of bounds and it is an undefined behavior.
bufinside the code statement below the functional property, then click on Show Defs.
buf(see video capture below).
bufcontains the result of the encryption of
str, the code should not allocate a buffer of constant size but one of the same size as