--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on December 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] cant analysis openmp code with frama-c



A reply to your Stack Overflow question 
(https://stackoverflow.com/questions/47773680) has just been posted 
(incidentally, before I noticed your question here). I believe it would 
be more productive to continue the discussion over there.


On 12/12/17 14:23, Rokiatou DIARRA wrote:
>
> I'm new in frama-c. I tried to run value analysis plugin on the 
> following c code with openmp directives :
>
> |staticvoidkernel_2mm(intni,intnj,intnk,intnl,floatalpha,floatbeta,float*tmp,float*A,float*B,float*C,float*D){inti,j,k;/* 
> D := alpha*A*B*C + beta*D */#pragmaomp parallel forcollapse(2)for(i 
> =0;i <ni;i++)for(j =0;j <nj;j++){tmp[i *nj +j]=0.0;for(k =0;k 
> <nk;++k)tmp[i *nj +j]+=alpha *A[i *nk +k]*B[k *nj +j];}#pragmaomp 
> parallel forcollapse(2)for(i =0;i <ni;i++)for(j =0;j <nl;j++){D[i *nl 
> +j]*=beta;for(k =0;k <nj;++k)D[i *nl +j]+=tmp[i *nj +k]*C[k *nl +j];}|
>
> }
>
> But I got the following errors:
>
>     rouki at rouki-VirtualBox:~/Téléchargements/frama-c$ frama-c -val
>     2mm_mp.c
>
>     [kernel] Parsing
>     FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
>
>     [kernel] Parsing 2mm_mp.c (with preprocessing)
>
>     [kernel] syntax error at 2mm_mp.c:78:
>
>     76 int i, j, k;
>
>     77 /* D := alpha/A/B/C + beta/D */
>
>     78 #pragma omp parallel for collapse(2)
>
>     |^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^|
>
>     79 for (i = 0; i < ni; i++)
>
>     80 for (j = 0; j < nj; j++) {
>
>     [kernel] Frama-C aborted: invalid user input.
>
> When I tried to add |-fopenmp| flag to the preprocesseur options with:
>
>     frama-c -machdep gcc_x86_64 -val -cpp-command 'gcc -fopenmp -C -E
>     -I. ' 2mm_mp.c
>
> I got another error message:
>
>
>     [kernel] Parsing
>     FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
>
>     [kernel] warning: your preprocessor is not known to handle option
>     `-nostdinc'. If pre-processing fails because of it, please add
>     -no-cpp-frama-c-compliant option to Frama-C's command-line. If you
>     do not want to see this warning again, explicitly use option
>     -cpp-frama-c-compliant.
>
>     [kernel] warning: your preprocessor is not known to handle option
>     `-dD'. If pre-processing fails because of it, please add
>     -no-cpp-frama-c-compliant option to Frama-C's command-line. If you
>     do not want to see this warning again, explicitly use option
>     -cpp-frama-c-compliant.
>
>     [kernel] Parsing 2mm_mp.c (with preprocessing)
>
>     [kernel] warning: trying to preprocess annotation with an unknown
>     preprocessor.
>
>     [kernel] syntax error at 2mm_mp.c:78:
>
>     76 int i, j, k;
>
>     77 /* D := alpha/A/B/C + beta/D */
>
>     78 #pragma omp parallel for collapse(2)
>
>     |^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^|
>
>     79 for (i = 0; i < ni; i++)
>
>     80 for (j = 0; j < nj; j++) {
>
>     [kernel] Frama-C aborted: invalid user input.
>
> How to make it that frama-c can analyze codes openmp?
>
> Is there a way to force frama-c to use another compiler than gcc (eg: 
> clang, pgcc)?
>
> I use frama-c Phosphorus-20170501 version, with gcc (Ubuntu 
> 5.4.0-6ubuntu1~16.04.5).
>
> Thanks.
> Rokiatou DIARRA
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
André Maroneze
Researcher/Engineer CEA/LIST
Software Reliability and Security Laboratory

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20171212/0f039e12/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3797 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20171212/0f039e12/attachment-0001.bin>