如何在z3中實現指針的解引用

試圖用python中的z3分析一些C程序，並用指針引起麻煩。我與條款的工作，如：如何在z3中實現指針的解引用

float * buffer = (float*)malloc(5*sizeof(float))

我解釋緩衝區作爲BitVec(32)值所以*buffer應該Real()。就應該沒什麼問題，但我應該寫什麼斷言的術語如

*(buffer+3) or *(buffer+i)

應該如何斷言寫，如果我索引出像

*(buffer-1) or *(buffer+10)

來源

2017-08-15 Robert

如果您使用C編程，那麼只能使用該標籤。不要使用無關標籤（語言或其他方式）發送垃圾郵件。 –

另外，在C中不需要施加'malloc'的返回值 - 它只能掩蓋錯誤。 –

一種解決方案是編碼程序堆作爲從位置到值的地圖H。在Z3中，陣列理論可以用來編碼地圖。

指針/地址是整數位置，整數算術編碼指針算術;這將允許在您的編碼中約束如H(buffer + i) > 0。如果您要編碼OO語言，則可以使用該對（接收者，字段名稱）對地址進行編碼。例如。 H(r, f) > 0將對應於r.f > 0。請注意，這種地圖編碼自然會佔用別名，例如如果buffer1 == buffer2和i == 3然後H(buffer1 + i) == H(buffer + 3)。

查看論文Heaps and Data Structures: A Challenge for Automated Provers，瞭解基於地圖的堆編碼的有趣比較。

基於映射的編碼通常由工具根據驗證條件使用，如Frama-C,Dafny和Boogie。基於符號執行的工具，如Silicon（它是Viper verification infrastructure的一部分）和VeriFast通常使用不同的編碼;見例如Heap-Dependent expressions in separation logic。

來源

2017-08-15 11:22:10

如何在z3中實現指針的解引用

回答

相關問題