seahorn / crab

A library for building abstract interpretation-based analyses
Apache License 2.0
234 stars 32 forks source link

Region Domain: MRU Cache #42

Closed LinerSu closed 2 years ago

LinerSu commented 3 years ago

This PR includes the following updates: (1) Add a new variable domain that is used to represent the base address of an allocated object symbolically. The Hasse diagram is:

                   Top
        /     /     |     \   
...  var1   var2   ...  varn  ...
        \      \    |     /     
                   Bot

(2) Enable MRU cache in region domain. The basic process is during load_ref / store_ref: If load/store a data for a object by reference within a region: