Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>