--- layout: fc_discuss_archives title: Message 1 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



I'm new in frama-c. I tried to run value analysis plugin on the following c code with openmp directives : 
static void kernel_2mm(int ni, int nj, int nk, int nl, float alpha, float beta, float *tmp, float *A, float *B, float *C, float *D) {
int i, j, k;
/* D := alpha*A*B*C + beta*D */
#pragma omp parallel for collapse(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];
    }
#pragma omp parallel for collapse(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 := alphaABC + betaD */
 
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 := alphaABC + betaD */
 
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20171212/ee0672f1/attachment.html>