--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on February 2012 ---
On Fri, Feb 3, 2012 at 3:36 PM, Boris Hollas < hollas at informatik.htw-dresden.de> wrote: > ** > On Fri, 2012-02-03 at 13:44 +0000, MONATE Benjamin 205998 wrote: > > Hi, > Frama-C and some of its plugins do handle multithreaded programs : what kind of analysis do you have in mind? > > > On the following code, Frama-C reports that is doesn't know about > pthread_create > > [kernel] warning: No code for function pthread_create, default assigns > generated for default behavior > > Value analysis reports x \in {1} for main, which is wrong. > The value analysis is not one of the plug-ins that handle multithread programs, but it is used to analyze the effects of a single thread at a time by the undistributed Frama-C plug-in for semantic analysis of multithreaded programs. That plug-in gives a meaning to pthread_create(), amongst other primitives. As Benjamin says, it is only a matter of defining the kind of target code one is talking about and the kind of properties one has in mind, and perhaps we can help. Pascal -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120207/20ae8cdb/attachment-0001.htm>