@@ -43,7 +43,7 @@ typedef struct {
4343#ifndef GGL_DISABLE_MACRO_TYPE_CHECKING
4444/// Create buffer literal from a byte array.
4545#define GGL_BUF (...) \
46- _Generic((&(__VA_ARGS__)), uint8_t(*)[]: GGL_BUF_UNCHECKED(__VA_ARGS__))
46+ _Generic((&(__VA_ARGS__)), uint8_t (*)[]: GGL_BUF_UNCHECKED(__VA_ARGS__))
4747#else
4848#define GGL_BUF GGL_BUF_UNCHECKED
4949#endif
@@ -101,28 +101,26 @@ bool ggl_buffer_contains(GglBuffer buf, GglBuffer substring, size_t *start);
101101/// The result is the overlap between the start to end range and the input
102102/// bounds.
103103CONST
104- GglBuffer ggl_buffer_substr (GglBuffer buf , size_t start , size_t end )
105- CBMC_CONTRACT (
106- requires (cbmc_buffer_restrict (& buf )),
107- requires (start < end ),
108- ensures (cbmc_implies (
109- (buf .data == NULL ),
110- (cbmc_return .data == NULL ) && (cbmc_return .len == 0 )
111- )),
112- ensures (cbmc_implies (
113- (buf .data != NULL ),
114- (cbmc_ptr_in_range (buf .data , cbmc_return .data , buf .data + buf .len )),
115- ((cbmc_return .data - buf .data ) <= (buf .len - cbmc_return .len ))
116- )),
117- ensures (cbmc_implies (
118- (buf .data != NULL ) && (start <= buf .len ),
119- (cbmc_return .data == buf .data + start )
120- )),
121- ensures (cbmc_implies (
122- (buf .data != NULL ) && (end <= buf .len ),
123- (cbmc_return .len == end - start )
124- )),
125- );
104+ GglBuffer
105+ ggl_buffer_substr (GglBuffer buf , size_t start , size_t end ) CBMC_CONTRACT (
106+ requires (cbmc_buffer_restrict (& buf )),
107+ requires (start < end ),
108+ ensures (cbmc_implies (
109+ (buf .data == NULL ), (cbmc_return .data == NULL ) && (cbmc_return .len == 0 )
110+ )),
111+ ensures (cbmc_implies (
112+ (buf .data != NULL ),
113+ (cbmc_ptr_in_range (buf .data , cbmc_return .data , buf .data + buf .len )),
114+ ((cbmc_return .data - buf .data ) <= (buf .len - cbmc_return .len ))
115+ )),
116+ ensures (cbmc_implies (
117+ (buf .data != NULL ) && (start <= buf .len ),
118+ (cbmc_return .data == buf .data + start )
119+ )),
120+ ensures (cbmc_implies (
121+ (buf .data != NULL ) && (end <= buf .len ), (cbmc_return .len == end - start )
122+ )),
123+ );
126124
127125/// Parse an integer from a string
128126ACCESS (write_only , 2 )
0 commit comments