Merge branch 'master' of https://github.com/seahorn/crab into fast-re…

…gion

README.md

@@ -13,18 +13,10 @@
   </tr>
 </table>
 
-If you use this library please cite the paper using the bibtex reference below.
 
-```
-@inproceedings{GN2021,
-  author={Arie Gurfinkel and Jorge A. Navas},
-  title={Abstract Interpretation of {LLVM} with a Region-based Memory Model},
-  booktitle = {Software Verification - 13th International Conference, {VSTTE} 2021,
-               and 14th International Workshop, {NSV} 2021, 
-               October 18-19, 2021, Revised Selected Papers},
-  year={2021}
-}
-```
+**If you use this library please cite this [paper](https://dblp.uni-trier.de/rec/conf/vstte/GurfinkelN21.html).**
+
+---
 
 # Description #
 

include/crab/domains/array_adaptive.hpp

@@ -345,22 +345,24 @@ class offset_map_t {
   class join_op : public binary_op_t {
     // apply is called when two bindings (one each from a
     // different map) have the same key(i.e., offset).
-    std::pair<bool, boost::optional<cell_set_t>> apply(const cell_set_t &x,
-                                                       const cell_set_t &y) {
+    std::pair<bool, boost::optional<cell_set_t>> apply(const offset_t &,
+						       const cell_set_t &x,
+                                                       const cell_set_t &y) override {
       return {false, cell_set_impl::set_union(x, y)};
     }
     // if one map does not have a key in the other map we add it.
-    bool default_is_absorbing() { return false; }
+    bool default_is_absorbing() override { return false; }
   };
 
   class meet_op : public binary_op_t {
-    std::pair<bool, boost::optional<cell_set_t>> apply(const cell_set_t &x,
-                                                       const cell_set_t &y) {
+    std::pair<bool, boost::optional<cell_set_t>> apply(const offset_t &,
+						       const cell_set_t &x,
+                                                       const cell_set_t &y) override {
       return {false, cell_set_impl::set_union(x, y)};
     }
     // if one map does not have a key in the other map we ignore
     // it.
-    bool default_is_absorbing() { return true; }
+    bool default_is_absorbing() override { return true; }
   };
 
   class domain_po : public partial_order_t {
@@ -944,15 +946,15 @@ class array_adaptive_domain final
   class array_state_map_t {
   private:
     using patricia_tree_t = ikos::patricia_tree<variable_t, array_state>;
-    using key_binary_op_t = typename patricia_tree_t::key_binary_op_t;
+    using binary_op_t = typename patricia_tree_t::binary_op_t;
 
   public:
     using iterator = typename patricia_tree_t::iterator;
 
   private:
     patricia_tree_t m_tree;
 
-    class join_op : public key_binary_op_t {
+    class join_op : public binary_op_t {
       cell_varmap_t &m_cvm_left;
       smashed_varmap_t &m_svm_left;
       base_domain_t &m_dom_left;
@@ -969,16 +971,16 @@ class array_adaptive_domain final
             m_dom_right(dom_right) {}
 
       std::pair<bool, boost::optional<array_state>>
-      apply(const variable_t &k, const array_state &x, const array_state &y) {
+      apply(const variable_t &k, const array_state &x, const array_state &y) override {
         array_state z = x.join(k, y, m_cvm_left, m_svm_left, m_dom_left,
                                m_cvm_right, m_svm_right, m_dom_right);
         return {false, boost::optional<array_state>(z)};
       }
 
-      bool default_is_absorbing() { return true; }
+      bool default_is_absorbing() override { return true; }
     }; // class join_op
 
-    class meet_op : public key_binary_op_t {
+    class meet_op : public binary_op_t {
       cell_varmap_t &m_cvm_left;
       smashed_varmap_t &m_svm_left;
       base_domain_t &m_dom_left;
@@ -995,15 +997,15 @@ class array_adaptive_domain final
             m_dom_right(dom_right) {}
 
       std::pair<bool, boost::optional<array_state>>
-      apply(const variable_t &k, const array_state &x, const array_state &y) {
+      apply(const variable_t &k, const array_state &x, const array_state &y) override {
         array_state z = x.meet(k, y, m_cvm_left, m_svm_left, m_dom_left,
                                m_cvm_right, m_svm_right, m_dom_right);
         return {false, boost::optional<array_state>(z)};
       }
-      bool default_is_absorbing() { return false; }
+      bool default_is_absorbing() override { return false; }
     }; // class meet_op
 
-    patricia_tree_t apply_operation(key_binary_op_t &o, patricia_tree_t t1,
+    patricia_tree_t apply_operation(binary_op_t &o, patricia_tree_t t1,
                                     const patricia_tree_t &t2) const {
       bool res = t1.merge_with(t2, o);
       if (res) {