This commit is contained in:
Patrick Pelissier committed 2017-02-21 21:57:19 +01:00
1 parent 85c9693413
commit 0f0cc0680d
1 file changed
+1
+1
View File
@@ -39,6 +39,7 @@
// This macro defines the contract of a string.
// Note: A ==> B is represented as not(A) or B
// Note: use of strlen can slowdown a lot the program in some program.
#define STRING_CONTRACT(v) \
M_ASSUME (v != NULL); \
M_ASSUME (v->ptr != NULL || (v->size == 0 && v->alloc == 0)); \