--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on December 2017 ---
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>