polyspace code prover: variable range does not change after function call
14 visualizaciones (últimos 30 días)
A simmilar code like the following I'm checking with polyspace codeprover 2014b.
x = myState->myVariable;
In the function setAllToZero() the variable myState->myVariable is set to 0. But after the function Call polyspace asumes, that the variable has full range. Why is the range not . Or what I'm doing wrong?
Lucas Lebert el 8 de Dic. de 2016
Since this post is quite old I assume that the issue has already been resolved. Nevertheless I want to leave tips for users who encounter the same issue. The first thing I would check is, whether the struct the pointer is pointing to is a global variable and if it is assigned to a permanent range. To check this just hover over "myVariable" in the third line of the example above. If the range is specified as "permanent range" in the tooltip. The first step is to investigate the "Variable/function range setup" in the "Inputs & Stubbing" pane of the Configurations. For the struct change the Init mode from "Permanent" to for example "Init".
If the struct the pointer is pointing to is not a global variable then it is a whole other story and I would need to have a closer look at it.
Code Verification Polyspace Code Prover Configure and Run Analysis Complete List of Polyspace Code Prover Analysis Options Options at Command Line Only