Inspect with TrustInSoft CI Analysis
(under the snippet of code) to launch TrustInSoft CI Analyzer:assert Value
. These properties are written using the ACSL specification language. They contain predicates, such as \valid(buf+i)
, that TrustInSoft CI tries to verify to prove the absence of undefined behaviors.\valid(buf+i)
did not hold, by inspecting the variables buf
and i
.i
inside \valid(buf+i)
, then look at the Values widget (bottom):i
along with the union of all its values until the undefined behavior was found. Since i
gets incremented at each iteration of the while
loop enclosing the undefined behavior, i
takes several values so an integer range between 1 and 33.buf
to look at its values in the Values widget:buf
is a pointer, whose value is the result of the call to malloc
in the function caesar_encrypt
line 26. The memory space allocated by malloc
is represented using the symbolic notation __malloc_caesar_encrypt_l26
.i
, buf
or any other expression, to see their values before and after the clicked statement in the Values widget:i
and select Track this term, then click on buf
to simultaneously inspect the values of i
and buf
:i
and __malloc_caesar_encrypt_l26
for each iteration of the while
loop enclosing the undefined behavior:i = 1
, which means that the statement with the undefined behavior is first reached when i = 1
.buf
with an offset i
equal to 33:__malloc_caesar_encrypt_l26
in the Expression column (see above screenshot) to see its type:__malloc_caesar_encrypt_l26
is an array of char of length 33 (char [33])
. The access with an offset of 33 is therefore out of bounds and it is an undefined behavior.buf
inside the code statement below the functional property, then click on Show Defs.buf
(see video capture below).malloc
. Since buf
contains the result of the encryption of str
, the code should not allocate a buffer of constant size but one of the same size as str
.