Spinroot

A forum for Spin users

You are not logged in.

#1 2016-05-09 16:16:32

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

Modex: Problem with implicit double/int conversions

Greetings!

I am currently working with Spin and Modex again to create and verify models of software on embedded systems.
Now, the following Code extract created some problems when it is transformed into a model and afterwards into a verifier:

#define OPVPFACTOR 				4.56522	
#define ADCMAXMV 				320.0
#define ADCMAX 					65535
#define RESISTANCESHUNT 			0.00025	

static const double ADCFACTOR = (ADCMAXMV * 2.0 / (ADCMAX));

int current = 0;
int *currentpointer = &current;

void calc_test () 
{
	int rawADC = 33000;
	*currentpointer = rawADC;

	double conversion;
	conversion = *currentpointer * ADCFACTOR;
	conversion = conversion - ADCMAXMV;
	conversion = conversion / OPVPFACTOR;
	conversion = conversion / RESISTANCESHUNT;
	*currentpointer = (int) conversion;
}

The task of this function is just to perform some transformations regarding the raw digital output of an ADC. Nothing special, and I also don't intend to include this explicit part in my verification, since Spin is not designed to check such computations in great detail. However, this part is still needed in the overall model, so I wanted to transform it with Modex and convert all of it into c_code{}-statements. The functionality of this part should just be exactly like the original C Code.

However, there were some unexpected results regarding the result of the computation. No matter what value I choose for "rawADC", the value within the "current" variable after these statements was always some huge, negative number. After some debugging and experimenting, I found out that the problem lies within the initialisation of the variable "ADCFACTOR": it is supposed to store a static value in a double type based on some pre-defined system values, which is later used in the computation. The right side of the assignment is a formula, and Modex will turn this declaration into the following c_state{}-statement:

 c_state "double  ADCFACTOR " "Global" "((320*2)/65535)"

So far, so good, but now the initialisation of this variable within the verifier pan.c looks like this:

void
globinit(void)
{
	now.ADCFACTOR   =  ((320*2)/65535) ;
	now.currentpointer   =  &(now.current) ;
}

Now, the result of this computation is sadly interpreted as an integer by the compiler, before it is assigned to the double type. Since the value is smaller than 1, this variable will always contain 0, leading to the stated behaviour of the model.
When replacing the right-hand side if the initialisation with the actual value (0.009765774), everything works fine. But I think this won't be the only time that I encounter expressions of this kind, and there may be other unwished consequences due to this way of translating these declarations in c_state{}-blocks.

Now that I wrote everything down here, I noticed that this problem seems extremly specific for this one case, but maybe this is a hint to a small flaw within the detailed workings of Modex and Spin that could occur on other occasions as well.

Thanks for reading!

So long,
- Max

Offline

#2 2016-05-10 03:46:18

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

Re: Modex: Problem with implicit double/int conversions

Thanks very much for the detailed example.
On a next revision of the modex distribution I'll see if this can be fixed.
Thanks!

Offline

Board footer

Powered by FluxBB