--- layout: fc_discuss_archives title: Message 8 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, 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.

Jessie reports
[jessie] warning: Unsupported feature(s).
                  Jessie plugin can not be used on your code.

wp gives a segmentation fault when trying to prove the assertion.

Also, the ACSL-implementation document doesn't mention concurrency,
which is what distinguishes multithreaded programs from singlethreaded
code. So, what do you mean with "Frama-C and some of its plugins do
handle multithreaded programs"?

---------------------------------------------------------------------------
#include <pthread.h>
#include <stdio.h>
#include <unistd.h>

int g;

void *thread1() {
	g = 0;
	return NULL;
}

int main() {
    pthread_t thread;
    int x;

	g = 1;
    pthread_create(&thread, NULL, thread1, NULL);
    sleep(1);
    //@ assert g == 1;
    x = g;
    return 0;
}

-- 
Best regards,
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120203/eff1a1d6/attachment-0001.htm>