Ego-Lane-Derived-Digests for Privatizations: `Lock- ` & `Write-Centered` Privatizations

goblint / analyzer

Static analysis framework for C

https://goblint.in.tum.de

MIT License

172 stars 72 forks source link

Ego-Lane-Derived-Digests for Privatizations: `Lock- ` & `Write-Centered` Privatizations #1399

Closed michael-schwarz closed 6 months ago

michael-schwarz commented 6 months ago

Add tid variants of the remaining privatizations to be evaluated for my thesis.

This attempts to make the construction from #1398 a bit more general, by replacing unknowns [α] with unknowns [α,A] for A from some ego-lane derived digest. Implementation-wise this is the same map construction as outlined in the PR for Protection-TID.

TODO:

[x] Write-Centered
[x] Combined

Follow-up to #1398.