diff --git a/.envrc b/.envrc
new file mode 100644
index 0000000000000000000000000000000000000000..3550a30f2de389e537ee40ca5e64a77dc185c79b
--- /dev/null
+++ b/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/config/a.out b/config/a.out
new file mode 100755
index 0000000000000000000000000000000000000000..f395b27c32da1457269fd6bb4e09c3e16c25ea53
Binary files /dev/null and b/config/a.out differ
diff --git a/config/cert_exp_33.c b/config/cert_exp_33.c
index c4fe87dcaaa750ddb5fe19c8053b12b3a334c10f..7d7f3c67dc35ca72dc38e04ad1f61b9ab436556c 100644
--- a/config/cert_exp_33.c
+++ b/config/cert_exp_33.c
@@ -1,17 +1,23 @@
+#include <stddef.h>
+
 void set_flag(int number, int *sign_flag) {
   if (NULL == sign_flag) {
     return;
   }
 
-  if (number > 0) {
+  // if (number > 0) {
+  // Correcte code
+  if (number >= 0) {
     *sign_flag = 1;
   } else if (number < 0) {
     *sign_flag = -1;
   }
+  Frama_C_show_each_set_flag(number, *sign_flag);
 }
 
 int is_negative(int number) {
   int sign;
   set_flag(number, &sign);
+  Frama_C_show_each_is_negative(number, sign);
   return sign < 0;
 }
diff --git a/config/cert_exp_33_realloc.c b/config/cert_exp_33_realloc.c
index 30cbd3e28a454416cdb24c1baf5210d603e59c87..b009490efb42cba87fe581316a090278e1fdb5b0 100644
--- a/config/cert_exp_33_realloc.c
+++ b/config/cert_exp_33_realloc.c
@@ -1,5 +1,5 @@
-#include <stdlib.h>
 #include <stdio.h>
+#include <stdlib.h>
 enum { OLD_SIZE = 10, NEW_SIZE = 20 };
 
 int *resize_array(int *array, size_t count) {
@@ -8,6 +8,7 @@ int *resize_array(int *array, size_t count) {
   }
 
   int *ret = (int *)realloc(array, count * sizeof(int));
+  //@ split ret==0;
   if (!ret) {
     free(array);
     return 0;
diff --git a/config/cert_exp_33_realloc_compliant.c b/config/cert_exp_33_realloc_compliant.c
new file mode 100644
index 0000000000000000000000000000000000000000..089c07e777f1e69306201746edb2061612ca3618
--- /dev/null
+++ b/config/cert_exp_33_realloc_compliant.c
@@ -0,0 +1,47 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+enum { OLD_SIZE = 10, NEW_SIZE = 20 };
+
+int *resize_array(int *array, size_t old_count, size_t new_count) {
+  if (0 == new_count) {
+    return 0;
+  }
+
+  int *ret = (int *)realloc(array, new_count * sizeof(int));
+  //@ split ret==0;
+  if (!ret) {
+    free(array);
+    return 0;
+  }
+
+  if (new_count > old_count) {
+    memset(ret + old_count, 0, (new_count - old_count) * sizeof(int));
+  }
+
+  return ret;
+}
+
+void func(void) {
+
+  int *array = (int *)malloc(OLD_SIZE * sizeof(int));
+  if (0 == array) {
+    /* Handle error */
+    return;
+  }
+
+  for (size_t i = 0; i < OLD_SIZE; ++i) {
+    array[i] = i;
+  }
+
+  array = resize_array(array, OLD_SIZE, NEW_SIZE);
+  if (0 == array) {
+    /* Handle error */
+    return;
+  }
+
+  for (size_t i = 0; i < NEW_SIZE; ++i) {
+    printf("%d ", array[i]);
+  }
+}
diff --git a/config/cwe20.c b/config/cwe20.c
index 9a723653eb1eb7474248a502ab6c75b6e3b0d4e4..02d126b3e2feabd986d0e31289ce01993706e9ef 100644
--- a/config/cwe20.c
+++ b/config/cwe20.c
@@ -1,8 +1,8 @@
 #include <stdio.h>
 #include <stdlib.h>
-void die(const char* s) {
-    printf("%s",s);
-    exit(2);
+void die(const char *s) {
+  printf("%s", s);
+  exit(2);
 }
 
 #define MAX_DIM 15
@@ -11,27 +11,30 @@ typedef int board_square_t;
 
 /* board dimensions */
 
-int main () {
-    int m,n, error;
-    board_square_t *board;
-    printf("Please specify the board height: \n");
-    error = scanf("%d", &m);
-    if ( EOF == error ){
+int main() {
+  int m, n, error;
+  board_square_t *board;
+  printf("Please specify the board height: \n");
+  error = scanf("%d", &m);
+  if (EOF == error) {
     die("No integer passed: Die evil hacker!\n");
-    }
-    printf("Please specify the board width: \n");
-    error = scanf("%d", &n);
-    if ( EOF == error ){
+  }
+  printf("Please specify the board width: \n");
+  error = scanf("%d", &n);
+  if (EOF == error) {
     die("No integer passed: Die evil hacker!\n");
-    }
-    if ( m > MAX_DIM || n > MAX_DIM ) {
+  }
+  if (m > MAX_DIM || n > MAX_DIM) {
     die("Value too large: Die evil hacker!\n");
+  }
+  board = (board_square_t *)malloc(m * n * sizeof(board_square_t));
+  for (int i = 0; i < m; i++) {
+    for (int j = 0; j < n; j++) {
+      board[n * i + j] = 0;
     }
-    board = (board_square_t*) malloc( m * n * sizeof(board_square_t));
-    for (int i = 0; i < m; i++) {
-        for (int j = 0; j < n; j++) {
-            board[n*i+j] = 0;
-        }
-    }
-    if (board[(m-1)*n] == 0) return 0; else return 1;
+  }
+  if (board[(m - 1) * n] == 0)
+    return 0;
+  else
+    return 1;
 }
diff --git a/config/cwe20_compliant.c b/config/cwe20_compliant.c
new file mode 100644
index 0000000000000000000000000000000000000000..d1b85df30e3bc7e8fdad9d79e0e2beb6aa138e62
--- /dev/null
+++ b/config/cwe20_compliant.c
@@ -0,0 +1,49 @@
+#include <stdio.h>
+#include <stdlib.h>
+void die(const char *s) {
+  printf("%s", s);
+  exit(2);
+}
+
+#define MAX_DIM 15
+
+typedef int board_square_t;
+
+/* board dimensions */
+
+int main(void) {
+  unsigned int m, n, error;
+  board_square_t *board;
+  printf("Please specify the board height: \n");
+  error = scanf("%d", &m);
+  if (EOF == error) {
+    die("No integer passed: Die evil hacker!\n");
+  }
+  printf("Please specify the board width: \n");
+  error = scanf("%d", &n);
+  if (EOF == error) {
+    die("No integer passed: Die evil hacker!\n");
+  }
+  if (m > MAX_DIM || m <= 0 || n > MAX_DIM) {
+    die("Value too large: Die evil hacker!\n");
+  }
+
+  board = (board_square_t *)malloc(m * n * sizeof(board_square_t));
+
+  // Check that is memory is properly allocated
+  if (!board) {
+    return 2;
+  }
+
+  for (unsigned int i = 0; i < m; i++) {
+    for (unsigned int j = 0; j < n; j++) {
+      board[n * i + j] = 0;
+    }
+  }
+
+  //@ split m == 0;
+  if (board[(m - 1) * n] == 0)
+    return 0;
+  else
+    return 1;
+}
diff --git a/config/libstring.c b/config/libstring.c
index c8a87c267e122d100bf1d92c06567448fa796fe0..35050644fb8d4e86c0747225646d29019bcceb4f 100644
--- a/config/libstring.c
+++ b/config/libstring.c
@@ -1,24 +1,55 @@
-#include <string.h>
-#include <stdlib.h>
-#include <ctype.h>
+#include <__fc_builtin.h>
 #include <assert.h>
-#include <unistd.h>
+#include <ctype.h>
 #include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
 
-
-#define unlikely(x)    __builtin_expect(!!(x), 0)
+#define unlikely(x) __builtin_expect(!!(x), 0)
 
 #include "libstring.h"
 
 #define BUF_LEN 65536
 #define CAP_DEFAULT 10
 
+int main(void) {
+  char char_string1[255];
+  char char_string2[255];
+  for (int i = 0; i < 254; i++) {
+    char_string1[i] = Frama_C_interval(1, 127);
+    char_string2[i] = Frama_C_interval(1, 127);
+  }
+  char_string1[254] = '\0';
+  char_string2[254] = '\0';
+  string_t *string1 = string_new(char_string1);
+  string_t *string2 = string_new(char_string2);
+  if (!string1 || !string2) {
+    printf("Invalid strings before concatenation !");
+    return -2;
+  }
+  string_t *string_final = string_concat(string1, string2);
+  free(string1);
+  free(string2);
+  if (!string_final) {
+    printf("Invalid string after concatenation !");
+    return -1;
+  }
+  string_print(string_final);
+  free(string_final);
+  return 0;
+}
+
+/**********************************************************************/
 
 string_t *string_colored(const char *str, enum stringcolor c) {
-  int n =  strlen(str) + strlen(COLOR_DEFAULT) + strlen(COLOR_BLACK);
+  int n = strlen(str) + strlen(COLOR_DEFAULT) + strlen(COLOR_BLACK);
   string_t *s = malloc(sizeof(string_t) + n);
-  if(unlikely(s == NULL)) return NULL;
+  if (unlikely(s == NULL))
+    return NULL;
   s->len = n;
+  // clang-format off
   switch(c) {
   case BLACK:   memcpy(s->buf,COLOR_BLACK,strlen(COLOR_BLACK));     break;
   case RED:     memcpy(s->buf,COLOR_RED,strlen(COLOR_RED));         break;
@@ -30,8 +61,9 @@ string_t *string_colored(const char *str, enum stringcolor c) {
   case WHITE:   memcpy(s->buf,COLOR_WHITE,strlen(COLOR_WHITE));     break;
   default: break;
   }
+  // clang-format on
   memcpy(&(s->buf[strlen(COLOR_BLACK)]), str, strlen(str));
-  n -=  strlen(COLOR_DEFAULT);
+  n -= strlen(COLOR_DEFAULT);
   memcpy(&(s->buf[n]), COLOR_DEFAULT, strlen(COLOR_DEFAULT));
   return s;
 }
@@ -40,7 +72,8 @@ string_t *string_colored(const char *str, enum stringcolor c) {
 
 string_t *string_nnew(const char *str, size_t len) {
   string_t *s = malloc(sizeof(string_t) + len);
-  if(unlikely(s == NULL)) return NULL;
+  if (unlikely(s == NULL))
+    return NULL;
   s->len = len;
   memcpy(s->buf, str, len);
   return s;
@@ -48,9 +81,7 @@ string_t *string_nnew(const char *str, size_t len) {
 
 /**********************************************************************/
 
-string_t *string_new(const char *str) {
-  return string_nnew(str, strlen(str));
-}
+string_t *string_new(const char *str) { return string_nnew(str, strlen(str)); }
 
 /**********************************************************************/
 
@@ -62,8 +93,9 @@ string_t *string_clone(const string_t *str) {
 
 string_t *string_readfd(int fd) {
   char buf[BUF_LEN];
-  int n = read(fd ,buf, BUF_LEN-1);
-  if(unlikely(n<0) ) return string_new("");
+  int n = read(fd, buf, BUF_LEN - 1);
+  if (unlikely(n < 0))
+    return string_new("");
   buf[n] = '\0';
   return string_new(buf);
 }
@@ -72,65 +104,71 @@ string_t *string_readfd(int fd) {
 
 string_t *string_readline(FILE *stream) {
   char buf[BUF_LEN];
-  if(!fgets(buf, BUF_LEN-1, stream)) return string_new("");
-  buf[strlen(buf)-1] = '\0';
+  if (!fgets(buf, BUF_LEN - 1, stream))
+    return string_new("");
+  buf[strlen(buf) - 1] = '\0';
   return string_new(buf);
 }
 
-
 /**********************************************************************/
 
 string_t *string_concat(const string_t *s1, const string_t *s2) {
   string_t *s = malloc(sizeof(string_t) + s1->len + s2->len);
-  if(unlikely(s == NULL)) return NULL;
+  if (unlikely(s == NULL))
+    return NULL;
   s->len = s1->len + s2->len;
   memcpy(s->buf, s1->buf, s1->len);
-  memcpy(s->buf+s1->len, s2->buf, s2->len);
+  memcpy(s->buf + s1->len, s2->buf, s2->len);
   return s;
 }
 
 /**********************************************************************/
 
 string_t *string_trim(const string_t *str) {
-  size_t l=0;
-  int r= str->len-1;
-  while(l < str->len && isspace(str->buf[l])) l+=1;
-  while(r>=0 && isspace(str->buf[r])) r-=1;
-  r+=1;
-  
-  if( unlikely(l> (size_t) r)) return string_new("");
+  size_t l = 0;
+  int r = str->len - 1;
+  while (l < str->len && isspace(str->buf[l]))
+    l += 1;
+  while (r >= 0 && isspace(str->buf[r]))
+    r -= 1;
+  r += 1;
+
+  if (unlikely(l > (size_t)r))
+    return string_new("");
 
-  return string_nnew( &(str->buf[l]), r-l);
+  return string_nnew(&(str->buf[l]), r - l);
 }
 
 /**********************************************************************/
 
 string_t *string_map(charfunc_t fun, const string_t *str) {
   string_t *s = string_clone(str);
-  if(unlikely(s == NULL)) return NULL;
-  for(size_t i=0;i<s->len;i++) {
+  if (unlikely(s == NULL))
+    return NULL;
+  for (size_t i = 0; i < s->len; i++) {
     s->buf[i] = fun(s->buf[i]);
   }
-  return s;                             
+  return s;
 }
 
 /**********************************************************************/
 
 string_t *string_filter(boolfunc_t fun, const string_t *str) {
-  int c=0;
+  int c = 0;
   char *tmp = malloc(str->len);
-  memcpy(tmp,str->buf,str->len);
-  for(size_t i=0; i < str->len; i++)
-    if(fun(str->buf[i])) tmp[c++] = str->buf[i]; 
+  memcpy(tmp, str->buf, str->len);
+  for (size_t i = 0; i < str->len; i++)
+    if (fun(str->buf[i]))
+      tmp[c++] = str->buf[i];
   tmp[c] = '\0';
   string_t *s = string_new(tmp);
   free(tmp);
-  return s;                             
+  return s;
 }
 
 /**********************************************************************/
 
-int string_compare(const string_t *s1,const string_t *s2) {
+int string_compare(const string_t *s1, const string_t *s2) {
   int n = (s1->len < s2->len) ? s1->len : s2->len;
   int r = strncmp(s1->buf, s2->buf, n);
 
@@ -140,40 +178,44 @@ int string_compare(const string_t *s1,const string_t *s2) {
 /**********************************************************************/
 
 bool string_equal(const string_t *s1, const string_t *s2) {
-  if(s1->len != s2->len) return false;
-  return strncmp(s1->buf,s2->buf,s1->len) == 0 ? true : false;   
+  if (s1->len != s2->len)
+    return false;
+  return strncmp(s1->buf, s2->buf, s1->len) == 0 ? true : false;
 }
 
 /**********************************************************************/
 
-string_t *string_substring(const string_t *str, size_t start, size_t end){
-  if(unlikely(!(start <= end) && (end <= str->len))) return NULL;
+string_t *string_substring(const string_t *str, size_t start, size_t end) {
+  if (unlikely(!(start <= end) && (end <= str->len)))
+    return NULL;
 
-  return string_nnew(&(str->buf[start]), end-start);
+  return string_nnew(&(str->buf[start]), end - start);
 }
 
 /**********************************************************************/
 
 string_t *string_repeat(const string_t *str, size_t times) {
-  size_t n =  str->len * times;
-  if( unlikely(!n)) return string_new("");
-  
+  size_t n = str->len * times;
+  if (unlikely(!n))
+    return string_new("");
+
   string_t *s = malloc(sizeof(string_t) + n);
-  if( unlikely(!s)) return NULL;
-  
+  if (unlikely(!s))
+    return NULL;
+
   s->len = n;
-  for(size_t i=0; i < times; i++)
-    memcpy(&(s->buf[i*(str->len)]), str->buf, str->len);
-  
+  for (size_t i = 0; i < times; i++)
+    memcpy(&(s->buf[i * (str->len)]), str->buf, str->len);
+
   return s;
 }
 
 /**********************************************************************/
 
-
 char *string_tocstr(const string_t *str) {
-  char *cstr = malloc(str->len +1);
-  if( unlikely(cstr==NULL)) return NULL;
+  char *cstr = malloc(str->len + 1);
+  if (unlikely(cstr == NULL))
+    return NULL;
   memcpy(cstr, str->buf, str->len);
   cstr[str->len] = '\0';
   return cstr;
@@ -181,48 +223,50 @@ char *string_tocstr(const string_t *str) {
 
 /**********************************************************************/
 
-static int string_substring_index_offset(const string_t *str, const string_t *substring, size_t offset) {
-  if(unlikely(substring->len == 0)) return offset;
-  if(unlikely(substring->len > (str->len - offset) )) return -1;
-
-  for(size_t i=offset; i<= str->len - substring->len; i++) {
-    for(size_t j=0; j < substring->len; j++) {
-      if(str->buf[i+j] != substring->buf[j]) break;
-      if( (j+1) == substring->len) return i;
+static int string_substring_index_offset(const string_t *str,
+                                         const string_t *substring,
+                                         size_t offset) {
+  if (unlikely(substring->len == 0))
+    return offset;
+  if (unlikely(substring->len > (str->len - offset)))
+    return -1;
+
+  for (size_t i = offset; i <= str->len - substring->len; i++) {
+    for (size_t j = 0; j < substring->len; j++) {
+      if (str->buf[i + j] != substring->buf[j])
+        break;
+      if ((j + 1) == substring->len)
+        return i;
     }
   }
   return -1;
 }
 
-
 int string_substring_index(const string_t *str, const string_t *substring) {
-  return string_substring_index_offset(str,substring, 0);
+  return string_substring_index_offset(str, substring, 0);
 }
 
-
 /**********************************************************************/
 
 bool string_is_substring(const string_t *str, const string_t *sub, size_t off) {
-  if(unlikely(sub->len+off > str->len)) return false;
-  if(unlikely(sub->len == 0)) return true;
+  if (unlikely(sub->len + off > str->len))
+    return false;
+  if (unlikely(sub->len == 0))
+    return true;
   return strncmp(&(str->buf[off]), sub->buf, sub->len) ? false : true;
-  
 }
 
-
-
 /**********************************************************************/
 
 string_t *string_replace_char(const string_t *str, char old, char new) {
-  string_t *s =  string_clone(str);
+  string_t *s = string_clone(str);
 
-  for(size_t i=0; i < s->len; i++) 
+  for (size_t i = 0; i < s->len; i++)
     s->buf[i] = (s->buf[i] == old) ? new : s->buf[i];
 
   return s;
 }
 
-
 /**********************************************************************/
 
 /*
@@ -230,91 +274,91 @@ string_t *string_replace_char(const string_t *str, char old, char new) {
  * suggestion by OpenAI's GPT-3.5
  */
 
-string_t *string_replace(const string_t *str, const string_t *old, const string_t *new) {
+string_t *string_replace(const string_t *str, const string_t *old,
+                         const string_t *new) {
   size_t n = 0;
   int offset = 0;
-  
-  while( (offset = string_substring_index_offset(str, old, offset)) > -1  ) {
-    offset+=old->len;
+
+  while ((offset = string_substring_index_offset(str, old, offset)) > -1) {
+    offset += old->len;
     n += 1;
   }
-  
-  if(n==0) return string_clone(str);
-  size_t len =  str->len + n * (new->len - old->len);
+
+  if (n == 0)
+    return string_clone(str);
+  size_t len = str->len + n * (new->len - old->len);
   string_t *s = malloc(sizeof(string_t) + len);
-  s->len = len;  
-  
+  s->len = len;
+
   char *t = s->buf;
   int curr = 0;
-  offset=0;
-  while(n--) {
+  offset = 0;
+  while (n--) {
     offset = string_substring_index_offset(str, old, offset);
-    memcpy(t, str->buf+curr, offset-curr);
-    t += offset-curr;
+    memcpy(t, str->buf + curr, offset - curr);
+    t += offset - curr;
 
     memcpy(t, new->buf, new->len);
     t += new->len;
     curr = offset + old->len;
-    offset+=old->len;
+    offset += old->len;
   }
-  memcpy(t, str->buf+curr, str->len-curr);
-  
-  
+  memcpy(t, str->buf + curr, str->len - curr);
+
   return s;
 }
-  
-
 
 /**********************************************************************/
 
 string_vector_t *string_split(const string_t *str, char delimiter) {
   string_vector_t *svec = string_vector_empty();
   size_t start = 0;
-  for(size_t i=0; i< string_len(str); i++)
-    if(str->buf[i]==delimiter) {
-      string_vector_add(svec, string_nnew(&(str->buf[start]), i-start));
-      start = i+1;
+  for (size_t i = 0; i < string_len(str); i++)
+    if (str->buf[i] == delimiter) {
+      string_vector_add(svec, string_nnew(&(str->buf[start]), i - start));
+      start = i + 1;
     }
-  string_vector_add(svec, string_nnew(&(str->buf[start]), string_len(str)-start));
+  string_vector_add(svec,
+                    string_nnew(&(str->buf[start]), string_len(str) - start));
   return svec;
 }
 
-
 /**********************************************************************/
 
 string_vector_t *string_ssplit(const string_t *str, string_t *delimiter) {
   string_vector_t *svec = string_vector_empty();
   int idx = string_substring_index(str, delimiter);
-  if(idx==-1) {
+  if (idx == -1) {
     string_vector_add(svec, string_clone(str));
     return svec;
   }
   string_vector_add(svec, string_nnew(str->buf, idx));
-  idx += string_len(delimiter);  
-  
-  for(size_t i=idx; i<= string_len(str)-string_len(delimiter); i++) {
-    for(size_t j=0; str->buf[i+j] == delimiter->buf[j]; j++)
-      if( (j+1) == delimiter->len-1) {
-        string_vector_add(svec, string_nnew(&(str->buf[idx]), i-idx));
+  idx += string_len(delimiter);
+
+  for (size_t i = idx; i <= string_len(str) - string_len(delimiter); i++) {
+    for (size_t j = 0; str->buf[i + j] == delimiter->buf[j]; j++)
+      if ((j + 1) == delimiter->len - 1) {
+        string_vector_add(svec, string_nnew(&(str->buf[idx]), i - idx));
         idx = i + string_len(delimiter);
-        i += string_len(delimiter);  
+        i += string_len(delimiter);
         break;
       }
   }
-  if( (size_t) idx <= string_len(str))
-    string_vector_add(svec, string_nnew(&(str->buf[idx]), string_len(str)-idx));
-    
+  if ((size_t)idx <= string_len(str))
+    string_vector_add(svec,
+                      string_nnew(&(str->buf[idx]), string_len(str) - idx));
+
   return svec;
 }
 
-
 /*************************************************************************
  *                           String Vector                               *
  *************************************************************************/
 
-string_vector_t *string_vector_empty() {
+string_vector_t *string_vector_empty(void) {
   string_vector_t *svec = malloc(sizeof(string_vector_t));
-  if(unlikely(svec==NULL)) return NULL;
+  if (unlikely(svec == NULL))
+    return NULL;
   svec->buf = malloc(CAP_DEFAULT * sizeof(string_t *));
   svec->cap = CAP_DEFAULT;
   svec->top = -1;
@@ -323,28 +367,29 @@ string_vector_t *string_vector_empty() {
 
 string_vector_t *string_vector_new(string_t *str) {
   string_vector_t *svec = string_vector_empty();
-  if(unlikely(svec==NULL)) return NULL;
+  if (unlikely(svec == NULL))
+    return NULL;
   string_vector_add(svec, str);
   return svec;
 }
-  
+
 bool string_vector_is_empty(const string_vector_t *svec) {
-    return svec->top == -1;
+  return svec->top == -1;
 }
 
-
 void string_vector_free(string_vector_t *svec) {
   free(svec->buf);
   free(svec);
 }
 
-void string_vector_deepfree(string_vector_t *svec){
-  for(int i=0;i <= svec->top; i++) free(svec->buf[i]);
+void string_vector_deepfree(string_vector_t *svec) {
+  for (int i = 0; i <= svec->top; i++)
+    free(svec->buf[i]);
   string_vector_free(svec);
 }
 
 bool string_vector_is_full(string_vector_t *svec) {
-    return (size_t) (svec->top + 1) == svec->cap; 
+  return (size_t)(svec->top + 1) == svec->cap;
 }
 
 void string_vector_resize(string_vector_t *svec) {
@@ -353,52 +398,59 @@ void string_vector_resize(string_vector_t *svec) {
 }
 
 int string_vector_find(const string_vector_t *svec, const string_t *str) {
-  for(int i= 0; i<=svec->top; i++) 
-    if (string_equal(svec->buf[i] , str)) return i;
+  for (int i = 0; i <= svec->top; i++)
+    if (string_equal(svec->buf[i], str))
+      return i;
   return -1;
 }
 
-void string_vector_add(string_vector_t *svec,  string_t *str) {
-  if (string_vector_is_full(svec)) string_vector_resize(svec);
+void string_vector_add(string_vector_t *svec, string_t *str) {
+  if (string_vector_is_full(svec))
+    string_vector_resize(svec);
   svec->top += 1;
   svec->buf[svec->top] = str;
 }
 
-
 /**********************************************************************/
 
-
 string_t *string_vector_remove(string_vector_t *svec, size_t index) {
-  if ((int)index > svec->top) return NULL;
+  if ((int)index > svec->top)
+    return NULL;
   string_t *str = svec->buf[index];
-  for(int i=index; i<svec->top; i++) svec->buf[i] = svec->buf[i+1];
-  svec->top -=1;
+  for (int i = index; i < svec->top; i++)
+    svec->buf[i] = svec->buf[i + 1];
+  svec->top -= 1;
   return str;
 }
 
-
 /**********************************************************************/
 
 bool string_vector_equal(const string_vector_t *a, const string_vector_t *b) {
-  if(a->top != b->top) return false;
-  for(int i=0;i<=a->top;i++) if(!string_equal(a->buf[i],b->buf[i])) return false;
-  return true;   
+  if (a->top != b->top)
+    return false;
+  for (int i = 0; i <= a->top; i++)
+    if (!string_equal(a->buf[i], b->buf[i]))
+      return false;
+  return true;
 }
 
 /**********************************************************************/
 
 string_vector_t *string_vector_map(strfunc_t func,
                                    const string_vector_t *svec) {
-  if(string_vector_len(svec) == 0)  return string_vector_empty();
+  if (string_vector_len(svec) == 0)
+    return string_vector_empty();
 
   string_vector_t *res = malloc(sizeof(string_vector_t));
-  if(unlikely(!res)) return NULL;
+  if (unlikely(!res))
+    return NULL;
   res->buf = malloc(svec->cap * sizeof(string_t *));
   res->cap = svec->cap;
   res->top = svec->top;
   memcpy(res->buf, svec->buf, svec->top * sizeof(string_t *));
-  
-  for(int i = 0; i<= svec->top; i++) res->buf[i] = func(svec->buf[i]);
+
+  for (int i = 0; i <= svec->top; i++)
+    res->buf[i] = func(svec->buf[i]);
 
   return res;
 }
@@ -408,32 +460,29 @@ string_vector_t *string_vector_map(strfunc_t func,
 string_vector_t *string_vector_filter(strboolfunc_t func,
                                       const string_vector_t *svec) {
   string_vector_t *res = string_vector_empty();
-  if(unlikely(!res)) return NULL;
-  for(int i = 0; i<= svec->top; i++)
-    if(func(svec->buf[i])) string_vector_add(res, string_clone(svec->buf[i])); 
-  
-  return res;     
+  if (unlikely(!res))
+    return NULL;
+  for (int i = 0; i <= svec->top; i++)
+    if (func(svec->buf[i]))
+      string_vector_add(res, string_clone(svec->buf[i]));
+
+  return res;
 }
 
 /**********************************************************************/
 
-string_t *string_vector_reduce(reducefunc_t func,
-                               const string_vector_t *svec,
+string_t *string_vector_reduce(reducefunc_t func, const string_vector_t *svec,
                                string_t *initializer) {
   string_t *val = (initializer) ? string_clone(initializer) : string_new("");
-  
-  for(int i = 0; i<= svec->top; i++) {
-    string_t *t = func(val,svec->buf[i]);
+
+  for (int i = 0; i <= svec->top; i++) {
+    string_t *t = func(val, svec->buf[i]);
     free(val);
     val = t;
   }
   return val;
 }
 
-
 /**********************************************************************/
 
-
-const char *libstring_version() {
-  return LIBSTRING_VERSION;
-}
+const char *libstring_version() { return LIBSTRING_VERSION; }
diff --git a/config/libstring.h b/config/libstring.h
index 06f533f2de570e49e89b02305fa5a1ecec375424..749a93fe3b14f395e74eb167f76a2489db1bfb2a 100644
--- a/config/libstring.h
+++ b/config/libstring.h
@@ -1,23 +1,23 @@
 #pragma once
 
+#include <stdbool.h>
 #include <stdint.h>
 #include <stdio.h>
-#include <stdbool.h>
 #include <unistd.h>
 
 #define LIBSTRING_VERSION "0.1.3"
 
 #define COLOR_DEFAULT "\033[0m"
-#define COLOR_BLACK   "\033[30m"
-#define COLOR_RED     "\033[31m"
-#define COLOR_GREEN   "\033[32m"
-#define COLOR_YELLOW  "\033[33m"
-#define COLOR_BLUE    "\033[34m"
+#define COLOR_BLACK "\033[30m"
+#define COLOR_RED "\033[31m"
+#define COLOR_GREEN "\033[32m"
+#define COLOR_YELLOW "\033[33m"
+#define COLOR_BLUE "\033[34m"
 #define COLOR_MAGENTA "\033[35m"
-#define COLOR_CYAN    "\033[36m"
-#define COLOR_WHITE   "\033[37m"
+#define COLOR_CYAN "\033[36m"
+#define COLOR_WHITE "\033[37m"
 
-enum stringcolor {BLACK, RED, GREEN, YELLOW, BLUE, MAGENTA, CYAN, WHITE};
+enum stringcolor { BLACK, RED, GREEN, YELLOW, BLUE, MAGENTA, CYAN, WHITE };
 
 typedef struct {
   size_t len;
@@ -28,7 +28,8 @@ typedef struct {
  * Creates a new colored string_t initialized with the provided character array.
  *
  * @param str A null-terminated character array to initialize the string with.
- * @param c The color to apply to the string (specified by the enum stringcolor).
+ * @param c The color to apply to the string (specified by the enum
+ * stringcolor).
  * @return A pointer to the newly allocated and colored string containing a copy
  *         of the input character array, or NULL if memory allocation failed.
  *         The returned string must be deallocated using the standard C
@@ -36,7 +37,6 @@ typedef struct {
  */
 string_t *string_colored(const char *str, enum stringcolor c);
 
-
 /**
  * Allocates a new string_t initialized with the provided character array.
  *
@@ -48,7 +48,6 @@ string_t *string_colored(const char *str, enum stringcolor c);
  **/
 string_t *string_new(const char *str);
 
-
 /**
  * Creates a new string_t object as a copy of the provided string.
  *
@@ -61,7 +60,6 @@ string_t *string_new(const char *str);
  **/
 string_t *string_clone(const string_t *str);
 
-
 /**
  * Reads up to 64 KB of data from the specified file descriptor and
  * creates a new string containing the read data.
@@ -74,7 +72,6 @@ string_t *string_clone(const string_t *str);
  **/
 string_t *string_readfd(int fd);
 
-
 /**
  * Reads a line from a file stream, with a maximum of 64 KB of data,
  * and stores it as a newly allocated string.
@@ -87,7 +84,6 @@ string_t *string_readfd(int fd);
  **/
 string_t *string_readline(FILE *stream);
 
-
 /**
  * Concatenates two strings and returns a new string containing the combined
  * contents.
@@ -101,7 +97,6 @@ string_t *string_readline(FILE *stream);
  **/
 string_t *string_concat(const string_t *s1, const string_t *s2);
 
-
 /**
  * Creates a new string by removing leading and trailing whitespace characters
  * from the provided string.
@@ -132,15 +127,14 @@ int string_compare(const string_t *s1, const string_t *s2);
  * @return True if the contents of s1 are equal to the contents of s2, false
  *         otherwise.
  **/
-bool  string_equal(const string_t *s1, const string_t *s2);
-
+bool string_equal(const string_t *s1, const string_t *s2);
 
 /**
  * Creates a new string that represents a substring of the input string.
  *
  * @param str The input string.
  * @param start The starting index of the substring.
- * @param end The ending index of the substring 
+ * @param end The ending index of the substring
  * @return A pointer to a newly allocated string containing the specified
  *         substring, or NULL if memory allocation failed or NULL if the
  *         indices are out of bounds. The returned string must be deallocated
@@ -148,7 +142,6 @@ bool  string_equal(const string_t *s1, const string_t *s2);
  **/
 string_t *string_substring(const string_t *str, size_t start, size_t end);
 
-
 /**
  * Converts a string to a null-terminated C string.
  *
@@ -160,7 +153,6 @@ string_t *string_substring(const string_t *str, size_t start, size_t end);
  **/
 char *string_tocstr(const string_t *str);
 
-
 /**
  * Finds the first occurrence of a substring within a string.
  *
@@ -169,7 +161,7 @@ char *string_tocstr(const string_t *str);
  * @return The index of the first occurrence of the substring in the input
  *         string, or -1 if not found.
  **/
-int   string_substring_index(const string_t *str, const string_t *substring);
+int string_substring_index(const string_t *str, const string_t *substring);
 
 /**
  * Checks if a substring appears in the input string at a specified offset.
@@ -182,7 +174,6 @@ int   string_substring_index(const string_t *str, const string_t *substring);
  */
 bool string_is_substring(const string_t *str, const string_t *sub, size_t off);
 
-
 /**
  * Creates a new string by repeating the input string multiple times.
  *
@@ -198,7 +189,6 @@ bool string_is_substring(const string_t *str, const string_t *sub, size_t off);
  **/
 string_t *string_repeat(const string_t *str, size_t times);
 
-
 /**
  * Creates a new string where all occurrences of the 'old' character
  * in the input string are replaced with the 'new' character.
@@ -207,26 +197,28 @@ string_t *string_repeat(const string_t *str, size_t times);
  * @param old The character to be replaced.
  * @param new The character to replace occurrences of 'old'.
  * @return A new string with replaced characters. Must be freed after use.
- * @note The returned string is allocated on the heap and must be freed by the caller.
- * @note If 'old' is not found in the input string, the function returns a copy of the input string.
+ * @note The returned string is allocated on the heap and must be freed by the
+ *caller.
+ * @note If 'old' is not found in the input string, the function returns a copy
+ *of the input string.
  **/
 string_t *string_replace_char(const string_t *str, char old, char new);
 
-
-
- /* Creates a new string where all occurrences of the 'old' substring
+/* Creates a new string where all occurrences of the 'old' substring
  * in the input string are replaced with the 'new' substring.
  *
  * @param str The input string.
  * @param old The substring to be replaced.
  * @param new The substring to replace occurrences of 'old'.
  * @return A new string with replaced substrings. Must be freed after use.
- * @note The returned string is allocated on the heap and must be freed by the caller.
- * @note If 'old' is not found in the input string, the function returns a copy of the input string.
+ * @note The returned string is allocated on the heap and must be freed by the
+ *caller.
+ * @note If 'old' is not found in the input string, the function returns a copy
+ *of the input string.
  **/
-string_t *string_replace(const string_t *str, const string_t *old, const string_t *new);
+string_t *string_replace(const string_t *str, const string_t *old,
+                         const string_t *new);
 
-  
 /**
  * Returns the character at the specified index in the string.
  *
@@ -239,7 +231,6 @@ static inline char string_get(const string_t *s, size_t index) {
   return (index < s->len) ? s->buf[index] : -1;
 }
 
-
 /**
  * Reads a line from the standard input and stores it as a newly allocated
  * string.
@@ -249,10 +240,7 @@ static inline char string_get(const string_t *s, size_t index) {
  * must be deallocated using the standard C library function `free()` when no
  * longer needed.
  **/
-static inline string_t *string_read() {
-  return string_readfd(STDIN_FILENO);
-}
-
+static inline string_t *string_read() { return string_readfd(STDIN_FILENO); }
 
 /**
  * Reads a line from the specified file stream and stores it as a newly
@@ -264,21 +252,17 @@ static inline string_t *string_read() {
  *         deallocated using the standard C library function `free()` when no
  *         longer needed.
  **/
- static inline string_t *string_readf(FILE *stream) {
+static inline string_t *string_readf(FILE *stream) {
   return string_readfd(fileno(stream));
 }
 
-
 /**
  * Checks if the given string is empty (length is 0).
  *
  * @param s The string_t object to check.
  * @return true if the string is empty, false otherwise.
  */
-static inline bool string_empty(const string_t *s) {
-  return s->len == 0;
-}
-
+static inline bool string_empty(const string_t *s) { return s->len == 0; }
 
 /**
  * Returns the length (number of characters) of the string.
@@ -286,10 +270,7 @@ static inline bool string_empty(const string_t *s) {
  * @param s The string to get the length of.
  * @return The length of the string.
  */
-static inline size_t string_len(const string_t *s) {
-  return s->len;
-}
-
+static inline size_t string_len(const string_t *s) { return s->len; }
 
 /**
  * Prints the contents of the string to the standard output.
@@ -299,7 +280,7 @@ static inline size_t string_len(const string_t *s) {
  *         occurred.
  **/
 static inline int string_print(const string_t *s) {
-  return printf("%.*s", (int) s->len, s->buf);
+  return printf("%.*s", (int)s->len, s->buf);
 }
 
 /**
@@ -311,7 +292,7 @@ static inline int string_print(const string_t *s) {
  *         occurred.
  **/
 static inline int string_printf(const string_t *s, FILE *f) {
-  return fprintf(f, "%.*s", (int) s->len, s->buf);
+  return fprintf(f, "%.*s", (int)s->len, s->buf);
 }
 
 /**
@@ -323,7 +304,7 @@ static inline int string_printf(const string_t *s, FILE *f) {
  *         occurred.
  */
 static inline int string_println(const string_t *s) {
-  return printf("%.*s\n", (int) s->len, s->buf);
+  return printf("%.*s\n", (int)s->len, s->buf);
 }
 
 /**
@@ -336,11 +317,9 @@ static inline int string_println(const string_t *s) {
  *         occurred.
  */
 static inline int string_printlnf(const string_t *s, FILE *f) {
-  return fprintf(f, "%.*s\n", (int) s->len, s->buf);
+  return fprintf(f, "%.*s\n", (int)s->len, s->buf);
 }
 
-
-
 /**********************************************************************/
 
 typedef char (*charfunc_t)(char);
@@ -360,7 +339,6 @@ typedef bool (*boolfunc_t)(char);
  **/
 string_t *string_map(charfunc_t func, const string_t *str);
 
-
 /**
  * Filters the characters of the input string using a specified predicate
  * function.
@@ -375,16 +353,14 @@ string_t *string_map(charfunc_t func, const string_t *str);
  **/
 string_t *string_filter(boolfunc_t func, const string_t *str);
 
-
 /**********************************************************************
- *                        String Vector                               * 
+ *                        String Vector                               *
  **********************************************************************/
 
-
 typedef struct st_strvec {
   size_t cap;
   int top;
-  string_t **buf;  
+  string_t **buf;
 } string_vector_t;
 
 /**
@@ -400,7 +376,6 @@ typedef struct st_strvec {
  **/
 string_vector_t *string_split(const string_t *str, char delimiter);
 
-
 /**
  * Splits the given string into a vector of substrings based on the provided
  * delimiter.
@@ -418,8 +393,6 @@ string_vector_t *string_split(const string_t *str, char delimiter);
  **/
 string_vector_t *string_ssplit(const string_t *str, string_t *delimiter);
 
-
-
 /**
  * Creates an empty string_vector.
  *
@@ -427,8 +400,7 @@ string_vector_t *string_ssplit(const string_t *str, string_t *delimiter);
  *         memory allocation failed. The returned vector must be deallocated
  *         using `string_vector_free()` when no longer needed.
  **/
-string_vector_t *string_vector_empty();
-
+string_vector_t *string_vector_empty(void);
 
 /**
  * Creates a new string_vector initialized with the provided string.
@@ -461,9 +433,8 @@ void string_vector_free(string_vector_t *svec);
  **/
 void string_vector_deepfree(string_vector_t *svec);
 
-
 /**
- * Adds a string to a string_vector 
+ * Adds a string to a string_vector
  *
  * @param svec The string_vector_t object.
  * @param str The string to add.
@@ -494,7 +465,6 @@ int string_vector_find(const string_vector_t *svec, const string_t *str);
  **/
 string_t *string_vector_remove(string_vector_t *svec, size_t index);
 
-
 /**
  * Compares two string_vector objects for equality.
  *
@@ -505,7 +475,6 @@ string_t *string_vector_remove(string_vector_t *svec, size_t index);
  **/
 bool string_vector_equal(const string_vector_t *a, const string_vector_t *b);
 
-
 /**
  * Retrieves the string at the specified index from the string vector.
  * If the index is out of bounds, NULL is returned.
@@ -517,7 +486,7 @@ bool string_vector_equal(const string_vector_t *a, const string_vector_t *b);
  */
 static inline string_t *string_vector_get(const string_vector_t *svec,
                                           size_t index) {
-  return ((int) index > svec->top) ? NULL : svec->buf[index];
+  return ((int)index > svec->top) ? NULL : svec->buf[index];
 }
 
 /**
@@ -532,10 +501,9 @@ static inline size_t string_vector_len(const string_vector_t *svec) {
 
 /**********************************************************************/
 
-typedef string_t * (*strfunc_t)(string_t *);
+typedef string_t *(*strfunc_t)(string_t *);
 typedef bool (*strboolfunc_t)(string_t *);
-typedef string_t * (*reducefunc_t)(string_t *value, string_t *element);
-
+typedef string_t *(*reducefunc_t)(string_t *value, string_t *element);
 
 /**
  * Applies a function to each string in a string vector and creates a new
@@ -552,7 +520,6 @@ typedef string_t * (*reducefunc_t)(string_t *value, string_t *element);
  **/
 string_vector_t *string_vector_map(strfunc_t func, const string_vector_t *svec);
 
-
 /**
  * Filters the strings in a string vector object based on a filtering function.
  *
@@ -568,7 +535,6 @@ string_vector_t *string_vector_map(strfunc_t func, const string_vector_t *svec);
 string_vector_t *string_vector_filter(strboolfunc_t func,
                                       const string_vector_t *svec);
 
-
 /**
  * Filters the strings in a string vector based on a filtering function.
  *
@@ -604,14 +570,12 @@ string_vector_t *string_vector_filter(strboolfunc_t func,
  *         string vector. The returned string must be deallocated
  *         using the standard C library function `free()` when no longer needed.
  */
-string_t *string_vector_reduce(reducefunc_t func,
-                               const string_vector_t *svec,
+string_t *string_vector_reduce(reducefunc_t func, const string_vector_t *svec,
                                string_t *initializer);
 
-
 /**********************************************************************/
 
-/**  
+/**
  * Returns the version string of the libstring library.
  *
  * @return A pointer to the null-terminated version string.
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000000000000000000000000000000000000..1d0fc862615d94a19522e37133ddb0d382e57af0
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,25 @@
+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1739736696,
+        "narHash": "sha256-zON2GNBkzsIyALlOCFiEBcIjI4w38GYOb+P+R4S8Jsw=",
+        "rev": "d74a2335ac9c133d6bbec9fc98d91a77f1604c1f",
+        "revCount": 754461,
+        "type": "tarball",
+        "url": "https://api.flakehub.com/f/pinned/NixOS/nixpkgs/0.1.754461%2Brev-d74a2335ac9c133d6bbec9fc98d91a77f1604c1f/01951426-5a87-7b75-8413-1a0d9ec5ff04/source.tar.gz"
+      },
+      "original": {
+        "type": "tarball",
+        "url": "https://flakehub.com/f/NixOS/nixpkgs/0.1.%2A.tar.gz"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000000000000000000000000000000000000..2cf78dd45e3b60688e51f1eb915ee4addfcd8fa2
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,35 @@
+{
+  description = "A Nix-flake-based C/C++ development environment";
+
+  inputs.nixpkgs.url = "https://flakehub.com/f/NixOS/nixpkgs/0.1.*.tar.gz";
+
+  outputs = { self, nixpkgs }:
+    let
+      supportedSystems = [ "x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin" ];
+      forEachSupportedSystem = f: nixpkgs.lib.genAttrs supportedSystems (system: f {
+        pkgs = import nixpkgs { inherit system; config.allowUnfree = true; };
+      });
+    in
+    {
+      devShells = forEachSupportedSystem ({ pkgs }: {
+        default = pkgs.mkShell.override
+          {
+            # Override stdenv in order to change compiler:
+            # stdenv = pkgs.clangStdenv;
+          }
+          {
+            packages = with pkgs; [
+              clang-tools
+	      framac
+	      clang
+	      gcc
+              cmake
+	      why3
+	      z3
+	      alt-ergo
+            ] ++ (if system == "aarch64-darwin" then [ ] else [ gdb ]);
+          };
+      });
+    };
+}
+