モデル変数は Frama-C マニュアル (仕様と「実装」バージョンの両方) で説明されています。
ただし、マニュアルにあるような単純なフラグメントを解析することはできません。
//@ model set<integer > forbidden = \empty;
あるいは
//@ model integer x = 0;
解析エラーにつながります。
モデル変数は本当にサポートされていますか? もしそうなら、私は何を間違っていますか？私が使用しているframa-cのバージョンは、MacOSのNitrogenです。
ありがとう、エドゥアルド