why the orange warning for next line is not happened when array use just one index?

Hi @Anirban,

At line 1971, array ps2g_csain_KArInFarCorIndirElimDistFr uses index u1s_csain_EmBumpTypeIndex, Orange warning is happened.

Size ps2g_csain_KArInFarCorIndirElimDistFr = 4

Range value of u1s_csain_EmBumpTypeIndex= [0..9]

Line 1791 and col 84 are orange warning. Please take a look Pic below:

Sequence Flow cod leads to warning: Please take a look Pic below:

At line 1973, array ps2g_csain_KArInFarCorIndirElimDistRr uses index u1s_csain_EmBumpTypeIndex, Green warning is happened.

Size ps2g_csain_KArInFarCorIndirElimDistRr = 4

Range value of u1s_csain_EmBumpTypeIndex= [0..3]

Line 1793 and col 84 are Green warning. Please take a look Pic below:

At line 1791Range value of u1s_csain_EmBumpTypeIndex = [0..9]. u1s_csain_EmBumpTypeIndex is not assigned from 1791 to 1793.

Please let me know why Range value of u1s_csain_EmBumpTypeIndex at line 1793 = [0..3]

BR

Thang Tran

[Tran Thang]

Hi @Anirban,

I have tried a checking. I creased size of ps2g_csain_KArInFarCorIndirElimDistFr from 4 to 10. And color of at line 1791 becomes GREEN

Please take a look picture below:

But color at line 1793 become ORANGE

At line 1793 Range value of u1s_csain_EmBumpTypeIndex = [0..9].

u1s_csain_EmBumpTypeIndex is not assigned from 1793 to 1794.

Please let me know why Range value of u1s_csain_EmBumpTypeIndex at line 1794 = [0..3]

I think that u1s_csain_EmBumpTypeIndex at line 1794 should be = [0..9]

BR

Thang Tran

Answer 1

[Anirban]

Hi,

Following an orange check, the analysis eliminates execution paths that lead to an error. This is intended to save you from reviewing many, many orange checks from the exact same root cause. That is why, in the line after the orange Out of bounds array index, the analysis only considers execution paths where the array index is within bounds.

See Code Prover Analysis Following Red and Orange Checks.