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