--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Can the tools be used with intrinsic in customer simulators



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>