--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on March 2010 ---
[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 ?
>