From ae24d843609c0fb4c65b4b369c88243adcbe4079 Mon Sep 17 00:00:00 2001 From: Reini Urban Date: Fri, 19 Nov 2021 19:47:06 +0100 Subject: [PATCH] WIP play with ACSL contracts --- ctl/algorithm.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/ctl/algorithm.h b/ctl/algorithm.h index 054f5319..d6691097 100644 --- a/ctl/algorithm.h +++ b/ctl/algorithm.h @@ -40,6 +40,12 @@ static inline I JOIN(A, find_if)(A *self, int _match(T *)) } // C++11 +/*@ + requires valid: \valid_read(self + (0..self->size-1)); + assigns \nothing; + ensures result: 0 <= \result <= self->size; + ensures result: \result == FindNotEqual(self, self->size, v); +*/ static inline I JOIN(A, find_if_not)(A *self, int _match(T *)) { foreach (A, self, i)