Skip to content
Snippets Groups Projects
Commit bce0a754 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

[RTL] Reworked splay tree memory model to have the same structure as 

Patricia trie (bittree)  memory model.
See commit e3d588eed2e9909f481371a6bbd4950dcb725291
parent 7ada28e8
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h
+ 0
− 1
View file @ bce0a754
...@@ -340,7 +340,6 @@ static struct _block * __get_exact (void * ptr) { ...@@ -340,7 +340,6 @@ static struct _block * __get_exact (void * ptr) {
return tmp->leaf; return tmp->leaf;
} }
/* return the block B containing ptr, such as : /* return the block B containing ptr, such as :
begin addr of B <= ptr < (begin addr + size) of B begin addr of B <= ptr < (begin addr + size) of B
or NULL if such a block does not exist */ or NULL if such a block does not exist */
......
src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.c → src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.h
+ 27
− 29
View file @ bce0a754
...@@ -20,18 +20,22 @@ ...@@ -20,18 +20,22 @@
/* */ /* */
/**************************************************************************/ /**************************************************************************/
#include "e_acsl_mmodel_api.h" #ifndef E_ACSL_SPLAYTREE
#include "e_acsl_mmodel.h" #define E_ACSL_SPLAYTREE
#include "stdio.h"
struct _node { #include "e_acsl_syscall.h"
#include "e_acsl_printf.h"
#include "e_acsl_assert.h"
#include "e_acsl_adt_api.h"
static struct _node {
struct _block * value; struct _block * value;
struct _node * left, * right, * parent; struct _node * left, * right, * parent;
}; };
struct _node * __root = NULL; static struct _node * __root = NULL;
void left_rotate(struct _node * x) { static void left_rotate(struct _node * x) {
struct _node* y = x->right; struct _node* y = x->right;
x->right = y->left; x->right = y->left;
if( y->left ) y->left->parent = x; if( y->left ) y->left->parent = x;
...@@ -43,7 +47,7 @@ void left_rotate(struct _node * x) { ...@@ -43,7 +47,7 @@ void left_rotate(struct _node * x) {
x->parent = y; x->parent = y;
} }
void right_rotate(struct _node *x ) { static void right_rotate(struct _node *x ) {
struct _node *y = x->left; struct _node *y = x->left;
x->left = y->right; x->left = y->right;
if( y->right ) y->right->parent = x; if( y->right ) y->right->parent = x;
...@@ -55,7 +59,7 @@ void right_rotate(struct _node *x ) { ...@@ -55,7 +59,7 @@ void right_rotate(struct _node *x ) {
x->parent = y; x->parent = y;
} }
void splay(struct _node *x ) { static void splay(struct _node *x ) {
while( x->parent ) { while( x->parent ) {
if( !x->parent->parent ) { if( !x->parent->parent ) {
if( x->parent->left == x ) right_rotate( x->parent ); if( x->parent->left == x ) right_rotate( x->parent );
...@@ -79,25 +83,25 @@ void splay(struct _node *x ) { ...@@ -79,25 +83,25 @@ void splay(struct _node *x ) {
} }
} }
} }
struct _node* subtree_minimum(struct _node *u ) { static struct _node* subtree_minimum(struct _node *u ) {
while( u->left ) u = u->left; while( u->left ) u = u->left;
return u; return u;
} }
struct _node* subtree_maximum(struct _node *u ) { static struct _node* subtree_maximum(struct _node *u ) {
while( u->right ) u = u->right; while( u->right ) u = u->right;
return u; return u;
} }
void replace(struct _node *u, struct _node *v ) { static void replace(struct _node *u, struct _node *v ) {
if( !u->parent ) __root = v; if( !u->parent ) __root = v;
else if( u == u->parent->left ) u->parent->left = v; else if( u == u->parent->left ) u->parent->left = v;
else u->parent->right = v; else u->parent->right = v;
if( v ) v->parent = u->parent; if( v ) v->parent = u->parent;
} }
void __remove_element(struct _block* ptr) { static void __remove_element(struct _block* ptr) {
struct _node * z = __root; struct _node * z = __root;
while(z != NULL) { while(z != NULL) {
if(z->value->ptr > ptr->ptr) z = z->left; if(z->value->ptr > ptr->ptr) z = z->left;
...@@ -122,8 +126,7 @@ void __remove_element(struct _block* ptr) { ...@@ -122,8 +126,7 @@ void __remove_element(struct _block* ptr) {
} }
} }
static void __add_element(struct _block* ptr) {
void __add_element(struct _block* ptr) {
struct _node *z = __root, *p = NULL; struct _node *z = __root, *p = NULL;
while( z ) { while( z ) {
p = z; p = z;
...@@ -141,8 +144,7 @@ void __add_element(struct _block* ptr) { ...@@ -141,8 +144,7 @@ void __add_element(struct _block* ptr) {
splay( z ); splay( z );
} }
static struct _block* __get_exact(void* ptr) {
struct _block* __get_exact(void* ptr) {
struct _node * tmp = __root; struct _node * tmp = __root;
while(tmp != NULL) { while(tmp != NULL) {
if(tmp->value->ptr > (size_t)ptr) tmp = tmp->left; if(tmp->value->ptr > (size_t)ptr) tmp = tmp->left;
...@@ -152,8 +154,7 @@ struct _block* __get_exact(void* ptr) { ...@@ -152,8 +154,7 @@ struct _block* __get_exact(void* ptr) {
return NULL; return NULL;
} }
static struct _block* _get_cont_rec(struct _node * node, void* ptr) {
struct _block* _get_cont_rec(struct _node * node, void* ptr) {
if(node == NULL) return NULL; if(node == NULL) return NULL;
else if(node->value->ptr > (size_t)ptr) return _get_cont_rec(node->left, ptr); else if(node->value->ptr > (size_t)ptr) return _get_cont_rec(node->left, ptr);
else if(node->value->size == 0 && node->value->ptr == (size_t)ptr) else if(node->value->size == 0 && node->value->ptr == (size_t)ptr)
...@@ -162,13 +163,11 @@ struct _block* _get_cont_rec(struct _node * node, void* ptr) { ...@@ -162,13 +163,11 @@ struct _block* _get_cont_rec(struct _node * node, void* ptr) {
else return _get_cont_rec(node->right, ptr); else return _get_cont_rec(node->right, ptr);
} }
static struct _block* __get_cont(void* ptr) {
struct _block* __get_cont(void* ptr) {
return _get_cont_rec(__root, ptr); return _get_cont_rec(__root, ptr);
} }
static void __clean_rec(struct _node * ptr) {
void __clean_rec(struct _node * ptr) {
if(ptr == NULL) return; if(ptr == NULL) return;
__clean_block(ptr->value); __clean_block(ptr->value);
__clean_rec(ptr->left); __clean_rec(ptr->left);
...@@ -177,12 +176,11 @@ void __clean_rec(struct _node * ptr) { ...@@ -177,12 +176,11 @@ void __clean_rec(struct _node * ptr) {
ptr = NULL; ptr = NULL;
} }
void __clean_struct() { static void __clean_struct() {
__clean_rec(__root); __clean_rec(__root);
} }
static void __debug_rec(struct _node * ptr) {
void __debug_rec(struct _node * ptr) {
if(ptr == NULL) return; if(ptr == NULL) return;
__debug_rec(ptr->left); __debug_rec(ptr->left);
printf("\t\t\t"); printf("\t\t\t");
...@@ -190,9 +188,9 @@ void __debug_rec(struct _node * ptr) { ...@@ -190,9 +188,9 @@ void __debug_rec(struct _node * ptr) {
__debug_rec(ptr->right); __debug_rec(ptr->right);
} }
void __debug_struct() { static void __debug_struct() {
printf("\t\t\t------------DEBUG\n"); printf("\t\t\t------------DEBUG\n");
__debug_rec(__root); __debug_rec(__root);
printf("\t\t\t-----------------\n"); printf("\t\t\t-----------------\n");
} }
#endif
src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree_mmodel.c 0 → 100644
+ 24
− 0
View file @ bce0a754
/**************************************************************************/
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
/* Copyright (C) 2012-2016 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file license/LGPLv2.1). */
/* */
/**************************************************************************/
#include "e_acsl_adt_mmodel.h"
#include "e_acsl_splaytree.h"
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment