Ошибка компиляции E-ACSL FRAMA-C

Question

Я новичок в фреймворке Frama-C и пытаюсь провести некоторое контрактное тестирование с помощью C-программ. Я намерен использовать плагин E-ACSL для этого, и я попробовал тестовую программу, чтобы увидеть, как она работает, но я получаю некоторые ошибки компиляции. Вот мой код:

#include <stdio.h>
#include <stdlib.h>

int main(void) {
int x = 0;
  /*@ assert x == 1;*/
  /*@ assert x == 0;*/
  return 0;
}

Далее приведен аннотированный код Frama-C:

/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
struct __e_acsl_mpz_struct {
   int _mp_alloc ;
   int _mp_size ;
   unsigned long *_mp_d ;
};
typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct;
typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
/*@ ghost extern int __e_acsl_init; */

/*@ ghost extern int __e_acsl_internal_heap; */

extern size_t __e_acsl_heap_allocation_size;

/*@
predicate diffSize{L1, L2}(ℤ i) =
  \at(__e_acsl_heap_allocation_size,L1) -
  \at(__e_acsl_heap_allocation_size,L2) ≡ i;

*/
int main(void)
{
  int __retres;
  int x = 0;
  /*@ assert x ≡ 1; */ ;
  /*@ assert x ≡ 0; */ ;
  __retres = 0;
  return __retres;
}

Наконец, я пытаюсь скомпилировать его с помощью gcc и флагов, указанных в руководстве (стр. 13), но я получаю следующие ошибки (и предупреждения):

$ gcc monitored_second.c -o monitored_second -leacsl -leacsl-gmp -leacsl -jemalloc -lpthread -lm

monitored_second.c:10:1: warning: ‘__FC_BUILTIN__’ attribute directive ignored [-Wattributes]
 typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];

monitored_second.c:18:55: warning: ‘__FC_BUILTIN__’ attribute directive ignored [-Wattributes]
                                                   int line);
                                                   ^
monitored_second.c:25:60: warning: ‘__FC_BUILTIN__’ attribute directive ignored [-Wattributes]
                                                        size_t ptr_size);
                                                        ^
/usr/bin/ld: cannot find -leacsl
/usr/bin/ld: cannot find -leacsl-jemalloc
collect2: error: ld returned 1 exit status

Я также удалил метку "-rtl-bittree", потому что она возвращает другую ошибку.

Последняя версия Frama-C: Sulphur-20171101 Есть идеи о том, что происходит?

Спасибо!

Answer 1

Обычно у вас должен быть скрипт e-acsl-gcc.sh установлен в том же каталоге, что и frama-c двоичный, который может позаботиться о вызове gcc с соответствующими опциями. Его основное использование описано в разделе 2.2 руководства, и man e-acsl-gcc.sh дает более подробную информацию о вариантах, которые могут быть использованы. Короче говоря, вы должны быть в состоянии напечатать

e-acsl-gcc.sh -c \
  --oexec-eacsl=first_monitored \
  --oexec=first \
  --ocode=first_monitored.i \
  first.i

чтобы получить

• исполняемый файл first_monitored с инструментами e-acsl
• исполняемый файл first с оригинальной программой
• исходный файл first_monitored.i с кодом e-acsl, сгенерированным C

Редактировать Глядя на команду связывания, используемую сценарием, я бы сказал, что предложенная ранее в руководстве командная строка устарела (в частности, она относится к eacsl-jemalloc в то время как e-acsl-gcc.sh кажется, предпочитает eacsl-dlmalloc), о которой, вероятно, можно сообщить как об ошибке на https://bts.frama-c.com/