From fc52fd9ac8a1a8fc76efd1e0f04048d42fc83b77 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Wed, 31 May 2023 23:29:08 +0900
Subject: [PATCH] inline arrow_step: IT WORKS WITH FRAMAC YAY!
---
include/arrow.c | 8 +-------
include/arrow.h | 8 +++++++-
include/arrow_noalloc.c | 8 +-------
include/arrow_spec.c | 12 ++----------
include/arrow_spec.h | 12 ++++++++++--
5 files changed, 21 insertions(+), 27 deletions(-)
diff --git a/include/arrow.c b/include/arrow.c
index 7cfb2e86..0801b045 100644
--- a/include/arrow.c
+++ b/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);
diff --git a/include/arrow.h b/include/arrow.h
index e0799784..20cbdc08 100644
--- a/include/arrow.h
+++ b/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
diff --git a/include/arrow_noalloc.c b/include/arrow_noalloc.c
index 2331679f..edb15c57 100644
--- a/include/arrow_noalloc.c
+++ b/include/arrow_noalloc.c
@@ -1,9 +1,3 @@
#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);
diff --git a/include/arrow_spec.c b/include/arrow_spec.c
index 1e363823..64c8fe63 100644
--- a/include/arrow_spec.c
+++ b/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) {
diff --git a/include/arrow_spec.h b/include/arrow_spec.h
index 78ef4bf0..06b717c1 100644
--- a/include/arrow_spec.h
+++ b/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
/@
--
GitLab