malloc - Frama-C での動的割り当ての処理

Question

Frama-C を使用して、動的メモリ割り当てを含む C コードの安全性を検証しようとしています。現在のバージョンの ACSL 仕様言語 (1.8) では、動的に割り当てられたメモリについて多くのことを表現できるようです。ただし、そのほとんどはまだ Frama-C Neon に実装されていません。

次のコード スニペットを使用するとします。

#include <stdlib.h>

/*@ requires \valid(p) && \valid(q) && \separated(p, q);
  @ ensures \valid(q);
  @*/
void test(char *p, char *q) {
  free(p);
}

int main(void) {
  char *p = (char *) malloc(10);
  char *q = (char *) malloc(10);

  test(p, q);

  return 0;
}

そのため、main は 2 つのメモリ ブロックを割り当て、それらへのポインタを関数 test に渡します。テストは、p が指すブロックを解放しますが、q が指すブロックは解放しません。テストの最後に、ポインター q がまだ有効であることを証明したいとします。どのように進めますか？

自分でヒープをモデル化する必要があるようです: ヒープについて話すいくつかの述語を公理化し、それらを使用して malloc と free を指定し、ACSL の実装されていない部分を模倣します。上記の例を確認できるように、それを行う最も簡単な方法は何ですか?