inline arrow_step: IT WORKS WITH FRAMAC YAY!

include/arrow.c

@@ -13,10 +13,4 @@ void _arrow_dealloc (struct _arrow_mem * _alloc) {
   free (_alloc);
 }
 
-_Bool _arrow_step(struct _arrow_mem *self) {
-  if (self->_reg._first) {
-    self->_reg._first = 0;
-    return 1;
-  }
-  return 0;
-}
+extern inline _Bool _arrow_step(struct _arrow_mem *self);

include/arrow.h

@@ -26,6 +26,12 @@ extern void _arrow_dealloc (struct _arrow_mem *);
 
 #define _arrow_reset(self) {(self)->_reg._first = 1;}
 
-_Bool _arrow_step(struct _arrow_mem *self);
+inline _Bool _arrow_step(struct _arrow_mem *self) {
+  if (self->_reg._first) {
+    self->_reg._first = 0;
+    return 1;
+  }
+  return 0;
+}
 
 #endif

include/arrow_noalloc.c

 #include "arrow.h"
 
-_Bool _arrow_step(struct _arrow_mem *self) {
-  if (self->_reg._first) {
-    self->_reg._first = 0;
-    return 1;
-  }
-  return 0;
-}
+extern inline _Bool _arrow_step(struct _arrow_mem *self);

include/arrow_spec.c

@@ -13,16 +13,8 @@ void _arrow_dealloc (struct _arrow_mem * _alloc) {
   free (_alloc);
 }
 
-_Bool _arrow_step(struct _arrow_mem *self)
-       /*@ ghost (struct _arrow_mem_ghost \ghost *mem) */
-{
-  if (self->_reg._first) {
-    self->_reg._first = 0;
-    //@ ghost mem->_reg._first = 0;
-    return 1;
-  }
-  return 0;
-}
+extern inline _Bool _arrow_step(struct _arrow_mem *self)
+       /*@ ghost (struct _arrow_mem_ghost \ghost *mem) */;
 
 /*@ ghost
   _Bool _arrow_step_ghost(struct _arrow_mem_ghost \ghost *mem) {

include/arrow_spec.h

@@ -64,8 +64,16 @@ extern void _arrow_dealloc (struct _arrow_mem *);
   ensures !\old(mem->_reg._first) ==> *mem == \old(*mem);
   assigns mem->_reg._first, self->_reg._first;
 */
-_Bool _arrow_step(struct _arrow_mem *self)
-       /*@ ghost (struct _arrow_mem_ghost \ghost *mem) */;
+inline _Bool _arrow_step(struct _arrow_mem *self)
+       /*@ ghost (struct _arrow_mem_ghost \ghost *mem) */
+{
+  if (self->_reg._first) {
+    self->_reg._first = 0;
+    //@ ghost mem->_reg._first = 0;
+    return 1;
+  }
+  return 0;
+}
 
 /*@ ghost
   /@