Spinroot

A forum for Spin users

You are not logged in.

#1 2015-10-06 17:04:50

Schachtschabel
Member
Registered: 2015-08-28
Posts: 15

Generating a model of sequential C-Code with Modex

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

#2 2015-10-08 19:37:40

spinroot
forum
Registered: 2010-11-18
Posts: 700
Website

Re: Generating a model of sequential C-Code with Modex

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

#3 2015-10-09 12:58:16

Schachtschabel
Member
Registered: 2015-08-28
Posts: 15

Re: Generating a model of sequential C-Code with Modex

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

#4 2015-10-09 16:25:32

spinroot
forum
Registered: 2010-11-18
Posts: 700
Website

Re: Generating a model of sequential C-Code with Modex

you cannot tell modex this (at least, i can't think of a good way to do that),
but you could postprocess the output from modex, for instance with a sed or awk script
to get the names right

Offline

Board footer

Powered by FluxBB