A forum for Spin users
You are not logged in.
Greetings to all,
I am currently facing a problem with generating an appropriate model of a C program with Modex.
Since most of the C-Code is executed sequential, there is basically just one process that calls different functions, waits for them to return and loops. I would like to model this behaviour as is, meaning I want to put all of the converted C-Code into one single proctype.
In the beginning, I tell Modex in my test harness what functions I want to include and if I want to turn them into certain kinds of processes. By using the '-n' flag, I just get the transformed C-Code without encapsulation and am able to put it somewhere I see fit within the model. The following is an extract from my current test harness:
%D velo_header.h
%X -L voltage.lut -n voltageUpdate
%X -L voltage.lut -n voltageGetAll
%L voltage
// some specific translations...
voltageGetAll() keep
%%
%P
inline voltageGetAll()
{
#include "_modex_voltageGetAll.pml"
}
inline voltageUpdate ()
{
#include "_modex_voltageUpdate.pml"
}
init
{
// some initilaziations...
do
:: true -> voltageUpdate()
od;
}
%%
I want to omit to put all functions of my code into processes, like Modex initialy does, because this creates enourmous overhead and additional side effects. After some research I found the possibiliy to define an 'inline' block, which creates a quite familiar view comparing to function calls in the original C-Code and does not invoke an additional process. My idea is now to put all the imported functions into corresponding inline blocks and keep the function calls of the original code, which should create a process that runs through the code line by line without any unwanted parallelism.
Now, this approach creates new kinds of problems, namely that the local variables of each imported function appear in a struct with a name corresponding to the process (e.g. "Pp_voltageUpdate->...") which is not defined when I use these inline blocks instead of proctypes.
Since I think that using inlines for each function would help me much with my current model extraction process, I would ask if anyone has some ideas how to get around this named problem or if there is an even easier way to get around the each-function-is-a-proctype-topic without changing the actual source code.
Kind regards.
Max
Offline
Maybe it's possible, and simplest, to postprocess the code for the inlines, so that you get the right scope.
Modex cannot know which proctypes will end up including the inlines, so I guess it can't always get the scope right by default.
Offline
Good thinking, but what do you exactly mean by "postprocess the code"?
In the end, I want all variables of every function to be in the scope of one proctype, since this process will be the one which includes all the inline-calls and thus all the code in sequential order.
How could I tell Modex this?
-Max
Offline
Offline