+int mc_important_snapshot(mc_snapshot_t snapshot);
+
+size_t* mc_take_page_snapshot_region(void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages);
+void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count);
+void mc_restore_page_snapshot_region(mc_mem_region_t region, size_t page_count, uint64_t* pagemap, mc_mem_region_t reference_region);
+
+mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, size_t size, mc_mem_region_t ref_reg);
+void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg);
+void mc_softdirty_reset();
+
+typedef struct s_mc_pages_store s_mc_pages_store_t, * mc_pages_store_t;
+mc_pages_store_t mc_pages_store_new();
+
+static inline bool mc_snapshot_region_linear(mc_mem_region_t region) {
+ return !region || !region->data;
+}
+
+void* mc_snapshot_read_region(void* addr, mc_mem_region_t region, void* target, size_t size);
+void* mc_snapshot_read(void* addr, mc_snapshot_t snapshot, void* target, size_t size);
+int mc_snapshot_memcp(
+ void* addr1, mc_snapshot_t snapshot1,
+ void* addr2, mc_snapshot_t snapshot2, size_t size);
+
+static inline void* mc_snapshot_read_pointer(void* addr, mc_snapshot_t snapshot)
+{
+ void* res;
+ return *(void**) mc_snapshot_read(addr, snapshot, &res, sizeof(void*));
+}
+
+/** @brief State of the model-checker (global variables for the model checker)
+ *
+ * Each part of the state of the model chercker represented as a global
+ * variable prevents some sharing between snapshots and must be ignored.
+ * By moving as much state as possible in this structure allocated
+ * on the model-chercker heap, we avoid those issues.
+ */
+typedef struct s_mc_model_checker {
+ // This is the parent snapshot of the current state:
+ mc_snapshot_t parent_snapshot;
+ mc_pages_store_t pages;
+ int fd_clear_refs;
+ int fd_pagemap;
+} s_mc_model_checker_t, *mc_model_checker_t;
+
+extern mc_model_checker_t mc_model_checker;
+
+void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region);
+
+/** \brief Translate a pointer from process address space to snapshot address space
+ *
+ * The address space contains snapshot of the main/application memory:
+ * this function finds the address in a given snaphot for a given
+ * real/application address.
+ *
+ * For read only memory regions and other regions which are not int the
+ * snapshot, the address is not changed.
+ *
+ * \param addr Application address
+ * \param snapshot The snapshot of interest (if NULL no translation is done)
+ * \return Translated address in the snapshot address space
+ * */
+void* mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot);
+
+/** \brief Translate a pointer from the snapshot address space to the application address space
+ *
+ * This is the inverse of mc_translate_address.
+ *
+ * Does not work for per-page snapshot, we change the logic to handle this.
+ *
+ * \param addr Address in the snapshot address space
+ * \param snapsot Snapshot of interest (if NULL no translation is done)
+ * \return Translated address in the application address space
+ */
+uintptr_t mc_untranslate_address(void* addr, mc_snapshot_t snapshot);
+