--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on February 2012 ---
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>