WIP play with ACSL contracts

rurban · rurban · commit 33b515b0c147 · 2024-02-16T21:02:41.000+01:00
diff --git 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)

Original file line number	Diff line number	Diff line change
`@@ -40,6 +40,12 @@ static inline I JOIN(A, find_if)(A self, int _match(T ))`
`40`	`40`	`}`
`41`	`41`
`42`	`42`	`// C++11`
	`43`	`+/*@`
	`44`	`+ requires valid: \valid_read(self + (0..self->size-1));`
	`45`	`+ assigns \nothing;`
	`46`	`+ ensures result: 0 <= \result <= self->size;`
	`47`	`+ ensures result: \result == FindNotEqual(self, self->size, v);`
	`48`	`+*/`
`43`	`49`	`static inline I JOIN(A, find_if_not)(A self, int _match(T ))`
`44`	`50`	`{`
`45`	`51`	`foreach (A, self, i)`