Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Use of Jessie and Value Analysis plug-in

  • Subject: [Frama-c-discuss] Use of Jessie and Value Analysis plug-in
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Thu, 18 Aug 2011 16:57:50 -0300
Hi,
I?m a Brazilian graduate student and I would like to use the Value
Analysis and Jessie plug-in. The case study is spatial critical real
time software, written in C deployed under the RTOS VxWorks. I did
some experiments and I had some doubts.

Value Analysis 1) I selected 9 functions that are part of flight task
responsible by control algorithms that involves a lot of computations
and variable, and depends on the values read from sensors. The task is
cyclic and the values generated are not so much predictable. I
appropriate to use the value analysis in this case? I can provide a
set of nominal values in the start (main).

Value Analysis 2) the entry point was the main function of the task
and its body is showed below. When I executed the analysis, the
plug-in shows the message below.  How I can treat this case?

void main(void)
{...
while(FOREVER){
        ?.
     } /* END OF While FOREVER */
}

[value] Values for function main:
          NON TERMINATING FUNCTION

Value Analysis 3) for refining my analysis, I tried the option
?slevel. The while (cited above) statement must be executed 3000
cycles (I am considering only a part of a task). There is a for
statement with 61 interactions. The correct choice must be 3000?

Value Analysis 4) is much appropriate to do the analysis with an
individual function, providing a main function for each one with the
initial values? In my experiment, I start with the main function of
the task and I was added the function incrementally. I analyzed the
final result. I noticed that when I executed the functions together a
lot of alarms disappear if compared with an analysis with an
individual function.

Value Analysis 5) what to do with functions that access the hardware
board? And the RTOS functions (for example, taskdelay - delay a task
from executing)?

Jessie 1) I have installed the Alt-Ergo 0.91, Simplify 1.5.4, Yices
1.0.29, CVC3 2.2., and Gappa 0.15.0.
My first problem was a short function responsible by limiting a value
in an interval ?6.111111e-2 to +6.111111e-2
I created the annotation below but I didn?t get prove. The code is
showed below. I don?t know what I am doing wrong.

/*@ requires \valid(AB) && \valid(CD);
  @ assigns *AB_Ptr, *CD_Ptr;
  @ ensures \abs(-6.111111e-2) <= *AB <= \abs(6.111111e-2);
  @ ensures \abs(-6.111111e-2) <= *CD <= \abs(6.111111e-2);
  @ */
void limitValue(float *AB, float *CD)
{
?
}

Jessie 2) in another function, with a high number of computations (12
ifs, 28 assignments, 1 loop, 21 pointers accesses.)
The Jessie generated 2725 VCs for the safety checking. Is it normal?
It is appropriate to evaluate this function with Jessie?  (Because the
computer is not a god machine I checked only one part #264).

Jessie 3) in another function, I have problems with union. The manual
says that Jessie works with unions, but a function below (similar to
the code) give an error in the if statement.  What is wrong?

union{
int i;
struct { short s1; short s2; unsigned int T1a : 1;
 } s;

}x;

#pragma JessieIntegerModel(math)
#pragma JessieTerminationPolicy(user)
# pragma JessieFloatModel(math)

void algorithm (void)
{
x.s.s1 = 0;
x.s.T1a  = 0;

   if(x.s.s1 == 0)
	printf("Sucesso");

}

Jessie 4) In case of short functions with only 01 comparison and 01
call of function. It is possible establish some kind of contract for
this function or not?

Jessie 5) I think that in the case of Jessie the better alternative is
to check individual functions, is not?

General question) I used the Boron version. Is there a Carbon version
for Windows?

Sorry for the number of questions, but I would like to use the tool in
my research...
I hope you can help me.

Best regards,
Rovedy