質問で述べたように、ステートメントprintf("%d\n", *c);は未定義の動作を公開します。undefinedであるため、それに対する期待はすべて誤りです。これには、特定のエラーまたはエラーの発生が含まれます。
C ランタイム ライブラリは、プログラムがメモリにアクセスする方法をチェックしません。それができれば、プログラムの実行速度ははるかに遅くなります。ヒープに関しては、C ランタイム ライブラリがいくつかの基本的なチェックを行います。たとえば、0プログラムの起動時にアドレスに特定の値を設定し、プログラムの終了時にその値がまだそこにあるかどうかを確認します。値が変更された場合、null ポインターは書き込みのために逆参照され、これについて警告することができます。
の後c = c + 20;、cほとんどの場合、プログラムに属するメモリ ブロックを指します。ヒープ上の空き領域にすることも、ヒープ マネージャーがヒープを処理するために使用するデータ構造内にすることもできますが、同じメモリ ページ上にある可能性が高くなります。
(不運な) 運がありc + 20、格納されているメモリ ページの外に出たc場合、オペレーティング システムによって処理される例外的な状況が発生します。プログラムを終了し、質問に記載されているものと同様のエラー メッセージを表示します (考え方は同じですが、言葉と表現は OS ごとに異なります)。
アップデート
メモリの割り当ては、ある種の魔法ではありません。プログラムは、この目的のために OS によってプログラムに割り当てられたメモリのブロック ( 「ヒープ」と呼ばれる) から開始します。
C ランタイム ライブラリには、ヒープを管理するコードが含まれています。このコードは、簿記のためにこのメモリのごく一部を使用します。<memory.h>一般的な実装では、二重リンク リストが使用されます。リストの各ノードのペイロードは、 (など)malloc()で宣言された関数を使用してプログラムによって "割り当てられた" メモリ ブロックです。calloc()への呼び出しがmalloc()発生すると、このコードが実行され、リストに新しいノードが作成され、ノードのペイロードのアドレス (ヒープ内のアドレス) が返されます。
プログラムはこのポインタを必要に応じて使用します。c-1たとえば、あなたのプログラムは自由に書くことができます。実際、その中malloc()には実際にそこに情報が書かれていました。return の後、あなたのコードは at にも書くことができmalloc()ます。観点からは、これら 2 つの書き込み操作に違いはありません。また、マネージ言語またはインタープリター言語ではないため、作成したコードの動作を監視したり、間違った場所に書き込まないように手を握ったりするコードがプログラムに含まれていません。cc-1OSC
で書き込むとc-1、ヒープ マネージャーが使用するデータ構造が破損する可能性が高くなります。すぐに悪いことは起こりません。エラー メッセージは表示されず、プログラムは正常に動作し続けます。しかし、ヒープを処理する関数への次の呼び出し (メモリ割り当てまたは解放) で、プログラムは大混乱を引き起こし始めます。ヒープ データ構造が壊れていると、何かが起こる可能性があります。
CBMCに関しては、私はそれがどのように機能するかわかりません。そのような状況を検出できない可能性があります。cまたは、プログラムがインクリメントされた後に書き込みを行わないため、プログラムが安全であると報告される場合があります。