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