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

  • Subject: [Frama-c-discuss] cant analysis openmp code with frama-c
  • From: diarr_rokiatou at yahoo.fr (Rokiatou DIARRA)
  • Date: Tue, 12 Dec 2017 13:23:30 +0000 (UTC)
  • References: <489846413.5504442.1513085010824.ref@mail.yahoo.com>
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>