Can anyone tell me how polyspace_main file is generated and works?

6 次查看（过去 30 天）
Pallavi Ingole
Pallavi Ingole 2016-10-26
评论： Rajeev 2021-2-19
I found that if we don't include main file while using polyspace, it creates its own _polyspace_main file. Can anyone tell me, how it get created? what it takes into consideration? how it decides sequence of function calling as main is missing?

请先登录，再回答此问题。

采纳的回答

Alexandre De Barros
Alexandre De Barros 2016-10-28
Hello,
When there is no main, Polyspace considers that the provided code represents an incomplete application. Hence, by default:
  1. the global variables (except the static ones) are treated like they could also be accessed by functions/methods that are not present,
  2. the functions that are not called in the provided code will be called by the generated main.
The main generator will then create a main that will make the global and non-static variables "full range" (i.e. all the values of their type are considered), and that will call the uncalled functions, in any order.
By doing this, the main generator is conservative, so no potential bug is missed.
This default behavior can be tuned, and users can tell how the main generator will treat the global variables, which functions should be called, if an init function should be called before the others, etc...
More information on the way the main is created and the related options can be found here.
Alex

更多回答（0 个）

类别

在 Help Center 和 File Exchange 中查找有关 Polyspace Code Prover 的更多信息

标签

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!

Translated by