diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c
index d8c669d7f95f764ab139b08d794821627a227418..973e1ab2d09deadcfcddf3d9759ff148a6c289ce 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c
@@ -334,9 +334,16 @@ static pt_node_t *pt_get_leaf_node_from_leaf(const pt_struct_t *pt,
return curr;
}
-void pt_remove(pt_struct_t *pt, pt_leaf_t leaf) {
- pt_node_t *leaf_node_to_delete = pt_get_leaf_node_from_leaf(pt, leaf);
- DASSERT(leaf_node_to_delete->leaf == leaf);
+/** Remove the given leaf node from the patricia trie.
+ *
+ * Internal function for `pt_remove()` and `pt_remove_if()`. The function will
+ * delete the given leaf node and copy its sibling if it exists to the parent
+ * node.
+ */
+static void pt_remove_leaf_node(pt_struct_t *pt,
+ pt_node_t *leaf_node_to_delete) {
+ DASSERT(leaf_node_to_delete != NULL);
+ DASSERT(leaf_node_to_delete->is_leaf);
if (leaf_node_to_delete->parent == NULL) {
// the leaf is the root
@@ -367,9 +374,49 @@ void pt_remove(pt_struct_t *pt, pt_leaf_t leaf) {
}
/* necessary ? -- end */
}
+ pt->clean_leaf_fct(leaf_node_to_delete->leaf);
private_free(leaf_node_to_delete);
}
+void pt_remove(pt_struct_t *pt, pt_leaf_t leaf) {
+ DASSERT(pt != NULL);
+ pt_node_t *leaf_node_to_delete = pt_get_leaf_node_from_leaf(pt, leaf);
+ DASSERT(leaf_node_to_delete->leaf == leaf);
+
+ pt_remove_leaf_node(pt, leaf_node_to_delete);
+}
+
+/** Starting at `node`, remove all leaves that satisfy the given predicate from
+ * the patricia trie. Return 1 if `node` is a leaf that is removed, 0
+ * otherwise.
+ * Internal function for `pt_remove_if()`. */
+int pt_remove_node_if(pt_struct_t *pt, pt_node_t *node,
+ pt_predicate_t predicate) {
+ DASSERT(pt != NULL);
+ if (node != NULL) {
+ if (node->is_leaf) {
+ if (predicate(node->leaf)) {
+ pt_remove_leaf_node(pt, node);
+ return 1;
+ }
+ } else {
+ // If `node->left` is a leaf that is removed, then `node->right` is
+ // copied to node and we have `node->left == \old(node->right->left)`
+ // (see `pt_remove_leaf_node()Ì€).
+ // We need to call `pt_remove_node_if()` on `node->left` until it is not
+ // a removed leaf.
+ while (pt_remove_node_if(pt, node->left, predicate)) {}
+ pt_remove_node_if(pt, node->right, predicate);
+ }
+ }
+ return 0;
+}
+
+void pt_remove_if(pt_struct_t *pt, pt_predicate_t predicate) {
+ DASSERT(pt != NULL);
+ pt_remove_node_if(pt, pt->root, predicate);
+}
+
pt_leaf_t pt_lookup(const pt_struct_t *pt, void *ptr) {
DASSERT(pt != NULL);
DASSERT(pt->root != NULL);
@@ -452,6 +499,29 @@ pt_leaf_t pt_find(const pt_struct_t *pt, void *ptr) {
}
}
+static pt_leaf_t pt_find_if_rec(pt_node_t *node, pt_predicate_t predicate) {
+ DASSERT(node != NULL);
+ if (node->is_leaf) {
+ return predicate(node->leaf) ? node->leaf : NULL;
+ } else {
+ pt_node_t *result = pt_find_if_rec(node->left, predicate);
+ if (result == NULL) {
+ result = pt_find_if_rec(node->right, predicate);
+ }
+ return result;
+ }
+}
+
+pt_leaf_t pt_find_if(const pt_struct_t *pt, pt_predicate_t predicate) {
+ DASSERT(pt != NULL);
+
+ if (pt->root == NULL) {
+ return NULL;
+ } else {
+ return pt_find_if_rec(pt->root, predicate);
+ }
+}
+
static void pt_clean_rec(const pt_struct_t *pt, pt_node_t *ptr) {
if (ptr == NULL) {
return;
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h
index ad237b701ded36e72eff23711067a2fc7ba2d608..63a050271a909260468450edc05bc772a1ca433e 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h
@@ -47,6 +47,9 @@ typedef int (*contains_ptr_fct_t)(pt_leaf_t, void *);
typedef void (*clean_leaf_fct_t)(pt_leaf_t);
/*! \brief Function pointer to a function that prints the content of a leaf. */
typedef void (*print_leaf_fct_t)(pt_leaf_t);
+/*! \brief Function pointer to a predicate function that returns true (!= 0) or
+ false (== 0) for a given leaf. */
+typedef int (*pt_predicate_t)(pt_leaf_t leaf);
/*! \brief Opaque structure of a patricia trie. */
typedef struct pt_struct pt_struct_t;
@@ -92,6 +95,16 @@ void pt_insert(pt_struct_t *pt, pt_leaf_t leaf);
@ assigns *pt \from *pt, leaf, indirect:__fc_heap_status; */
void pt_remove(pt_struct_t *pt, pt_leaf_t leaf);
+/*! \brief Remove all leaves that satisfy the given predicate from the patricia
+ trie.
+ \param pt Patricia trie to update.
+ \param predicate Predicate to test the leaves of the trie. */
+/*@ requires \valid(pt);
+ @ requires \valid_function(pt_predicate_t predicate);
+ @ assigns __fc_heap_status \from __fc_heap_status;
+ @ assigns *pt \from *pt, indirect:predicate, indirect:__fc_heap_status; */
+void pt_remove_if(pt_struct_t *pt, pt_predicate_t predicate);
+
/*! \brief Look for the leaf representing exactly the given pointer.
Given the function `get_fct_ptr` provided at the trie creation and a leaf
@@ -119,6 +132,15 @@ pt_leaf_t pt_lookup(const pt_struct_t *pt, void *ptr);
@ assigns \result \from *pt, indirect:ptr; */
pt_leaf_t pt_find(const pt_struct_t *pt, void *ptr);
+/*! \brief Look for the first leaf that satisfies the given predicate.
+ \param pt Patricia trie where to look for.
+ \param predicate Predicate to test the leaves of the trie.
+ \return The first leaf satisfying the given predicate. */
+/*@ requires \valid_read(pt);
+ @ requires \valid_function(pt_predicate_t predicate);
+ @ assigns \result \from *pt, indirect:predicate; */
+pt_leaf_t pt_find_if(const pt_struct_t *pt, pt_predicate_t predicate);
+
/*! \brief Clean the content of the given patricia trie.
Contrary to `pt_destroy()`, this function removes all leaves of the trie but