Как вызвать аксиомы о строковых функциях libc во Frama-C? - PullRequest
Новая
       19

Как вызвать аксиомы о строковых функциях libc во Frama-C?

0 голосов
/ 27 июня 2018

Frama-C предоставляет аксиоматические спецификации для строковых функций из стандартной библиотеки C в заголовочном файле __fc_string_axiomatic.h. Например, одна такая запись с указанием memset() гласит: 

/*@ axiomatic MemSet {
  @ logic ? memset{L}(char *s, ℤ c, ℤ n)
  @   reads s[0..n - 1];
  @ // Returns [true] iff array [s] contains only character [c]
  @
  @ axiom memset_def{L}:
  @   \forall char *s; \forall ℤ c; \forall ℤ n;
  @      memset(s,c,n) <==> \forall ℤ i; 0 <= i < n ==> s[i] == c;
  @ }
  @*/

В моем собственном аннотированном C-файле я пытаюсь использовать эту аксиоматическую спецификацию memset() следующим образом: 

int n = strlen(argv[1]);
//@ assert n >= 0;
char dest[n+1];
//@ assert \valid(dest+ (0..n));
//@ assert \valid(argv[1]+ (0..n));


memset(dest,0,n+1);
//@ assert \forall integer k; 0 <= k < n+1 ==> dest[k] == 0;

Хотя окончательное утверждение кажется заменой предиката в memset_def, и Frama-C действительно оценила показанный выше axiomatic, Alt-Ergo не может доказать это утверждение. Я не заинтересован в проверке самой стандартной библиотеки C; мой вопрос: как я могу заставить Frama-C вызвать эту аксиому в своих собственных утверждениях?

1 Ответ

0 голосов
/ 27 июня 2018

Ваше утверждение подтверждается, например, мгновенно. Z3 4.4.1, но на самом деле не Alt-Ergo. Таким образом, проблема заключается в стратегии, используемой Alt-Ergo для решения цели, а не в том, что генерирует Frama-C. Можно было бы добавить триггеры, чтобы помочь Alt-Ergo, но мне не ясно, где мы могли бы их разместить.

...