|
|
Memory Representation for Model Checker of C/C++
Kouba, Jan ; Šerý, Ondřej (advisor) ; Kofroň, Jan (referee)
We describe the design and C++ implementation of the newly created memory module (MM) in this work. It will be used in the GIMPLE Model Checker, an explicit state model checker, to represent the memory of checked program. MM diers from other code model checkers in the fact, that it stores ordinary C++ objects fullling a given interface as values. This allows to store, e.g., value data together with its type, a symbolic value used in a symbolic execution or a predicate over a stored value used in predicate abstraction. MM uses delta saving, incremental hashing and incremental heap canonicalization to save the state, canonicalize the heap and compute the hash of the state eciently.
|
guest ::
RSS feed.