search

ftsrg / gazer

An LLVM-based formal verification frontend for C programs.
24 stars 5 forks source link

Support SV-COMP ReachSafety-Heap with BMC #80

Open hajduakos opened 3 years ago

hajduakos commented 3 years ago

This might be tricky, but Gazer does have some sort of memory models

AdamZsofi commented 3 years ago

Not top priority right now, but I'll run some benchmarks for this later, as we didn't even try this category earlier.

sallaigy commented 3 years ago

All of these programs seem to require malloc support, something we do not yet have in our flat memory model. I opened a separate ticket #86 to track that issue.