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] question about slicer

Hello,

Thank you for your quick responses. The program is of an interrupt
driven device and each thread modifies a shared global variable
ErrorStatus. So you can imagine many |= and &= type assignments to the
variable from the threads and the some nested if tests. There is a main
function with an infinite loop(i dont know whether that is significant
for code slicing). My aim is to slice the threads and the main function
giving me a reduced set of instructions that each thread performs on
ErrorStatus. I get no output from attempting to slice the main loop so I
added fake assignments such as ErrorStatus=someconstant to see how far
it gets. It gets to a certain point in the main loop even under the
infinite while loop but it stops just before one assignment. I will try
to learn more through the value analysis.

Thank you again
Damien

Anne Pacalet wrote:
> Pascal Cuoq wrote :
>> One possibility, which is only a special case of the situation Anne
>> described, is that Frama-C thinks that a run-time error is certainly
>> happening. 
>
> To find this kind of problem, I suggest that you try run Frama-C with
> its GUI,
> and to analyze your application with the value analysis (option -val).
> Dead code should be highlighted in red.
> This code is ignored by the slicing tool.
>
> Maybe it can help to understand the problem ?
>