@@ -249,6 +249,11 @@ invariant_violated_string(
249
249
#define __this_function__ __func__
250
250
#endif
251
251
252
+ // We wrap macros that take __VA_ARGS__ as an argument with EXPAND_MACRO(). This
253
+ // is to account for the behaviour of msvc, which otherwise would not expand
254
+ // __VA_ARGS__ to multiple arguments in the outermost macro invocation.
255
+ #define EXPAND_MACRO (x ) x
256
+
252
257
#define GET_MACRO (X1, X2, X3, X4, X5, X6, MACRO, ...) MACRO
253
258
254
259
// This macro dispatches to the macros MACRO<n> (with 1 <= n <= 6) and calls
@@ -257,16 +262,16 @@ invariant_violated_string(
257
262
#define REDIRECT (MACRO, ...) \
258
263
do \
259
264
{ \
260
- GET_MACRO ( \
261
- __VA_ARGS__, \
262
- MACRO## 6 , \
263
- MACRO##5 , \
264
- MACRO##4 , \
265
- MACRO##3 , \
266
- MACRO##2 , \
267
- MACRO##1 , \
268
- DUMMY_MACRO_ARG) \
269
- (__VA_ARGS__); \
265
+ EXPAND_MACRO ( \
266
+ GET_MACRO ( \
267
+ __VA_ARGS__, \
268
+ MACRO##6 , \
269
+ MACRO##5 , \
270
+ MACRO##4 , \
271
+ MACRO##3 , \
272
+ MACRO##2 , \
273
+ MACRO## 1 , \
274
+ DUMMY_MACRO_ARG)(__VA_ARGS__)); \
270
275
} while (false )
271
276
272
277
#define INVARIANT2 (CONDITION, REASON ) \
@@ -311,7 +316,7 @@ invariant_violated_string(
311
316
// Short hand macros. The variants *_STRUCTURED below allow to specify a custom
312
317
// exception, and are equivalent to INVARIANT_STRUCTURED.
313
318
314
- #define INVARIANT (...) REDIRECT(INVARIANT, __VA_ARGS__)
319
+ #define INVARIANT (...) EXPAND_MACRO( REDIRECT(INVARIANT, __VA_ARGS__) )
315
320
316
321
// The condition should only contain (unmodified) inputs to the method. Inputs
317
322
// include arguments passed to the function, as well as member variables that
@@ -325,10 +330,10 @@ invariant_violated_string(
325
330
#define PRECONDITION2 (CONDITION, DIAGNOSTICS ) \
326
331
INVARIANT3 (CONDITION, " Precondition" , DIAGNOSTICS)
327
332
328
- #define PRECONDITION (...) REDIRECT(PRECONDITION, __VA_ARGS__)
333
+ #define PRECONDITION (...) EXPAND_MACRO( REDIRECT(PRECONDITION, __VA_ARGS__) )
329
334
330
- #define PRECONDITION_STRUCTURED (CONDITION, TYPENAME, ...) \
331
- INVARIANT_STRUCTURED (CONDITION, TYPENAME, __VA_ARGS__)
335
+ #define PRECONDITION_STRUCTURED (CONDITION, TYPENAME, ...) \
336
+ EXPAND_MACRO ( INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) )
332
337
333
338
// The condition should only contain variables that will be returned /
334
339
// output without further modification.
@@ -342,10 +347,10 @@ invariant_violated_string(
342
347
#define POSTCONDITION2 (CONDITION, DIAGNOSTICS ) \
343
348
INVARIANT3 (CONDITION, " Postcondition" , DIAGNOSTICS)
344
349
345
- #define POSTCONDITION (...) REDIRECT(POSTCONDITION, __VA_ARGS__)
350
+ #define POSTCONDITION (...) EXPAND_MACRO( REDIRECT(POSTCONDITION, __VA_ARGS__) )
346
351
347
- #define POSTCONDITION_STRUCTURED (CONDITION, TYPENAME, ...) \
348
- INVARIANT_STRUCTURED (CONDITION, TYPENAME, __VA_ARGS__)
352
+ #define POSTCONDITION_STRUCTURED (CONDITION, TYPENAME, ...) \
353
+ EXPAND_MACRO ( INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) )
349
354
350
355
// The condition should only contain (unmodified) values that were
351
356
// changed by a previous method call.
@@ -359,15 +364,15 @@ invariant_violated_string(
359
364
#define CHECK_RETURN2 (CONDITION, DIAGNOSTICS ) \
360
365
INVARIANT3 (CONDITION, " Check return value" , DIAGNOSTICS)
361
366
362
- #define CHECK_RETURN (...) REDIRECT(CHECK_RETURN, __VA_ARGS__)
367
+ #define CHECK_RETURN (...) EXPAND_MACRO( REDIRECT(CHECK_RETURN, __VA_ARGS__) )
363
368
364
- #define CHECK_RETURN_STRUCTURED (CONDITION, TYPENAME, ...) \
365
- INVARIANT_STRUCTURED (CONDITION, TYPENAME, __VA_ARGS__)
369
+ #define CHECK_RETURN_STRUCTURED (CONDITION, TYPENAME, ...) \
370
+ EXPAND_MACRO ( INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) )
366
371
367
372
// This should be used to mark dead code
368
373
#define UNREACHABLE INVARIANT2 (false , " Unreachable" )
369
- #define UNREACHABLE_STRUCTURED (TYPENAME, ...) \
370
- INVARIANT_STRUCTURED (false , TYPENAME, __VA_ARGS__)
374
+ #define UNREACHABLE_STRUCTURED (TYPENAME, ...) \
375
+ EXPAND_MACRO ( INVARIANT_STRUCTURED(false , TYPENAME, __VA_ARGS__) )
371
376
372
377
// This condition should be used to document that assumptions that are
373
378
// made on goto_functions, goto_programs, exprts, etc. being well formed.
@@ -376,10 +381,10 @@ invariant_violated_string(
376
381
#define DATA_INVARIANT3 (CONDITION, REASON, DIAGNOSTICS ) \
377
382
INVARIANT3 (CONDITION, REASON, DIAGNOSTICS)
378
383
379
- #define DATA_INVARIANT (...) REDIRECT(DATA_INVARIANT, __VA_ARGS__)
384
+ #define DATA_INVARIANT (...) EXPAND_MACRO( REDIRECT(DATA_INVARIANT, __VA_ARGS__) )
380
385
381
- #define DATA_INVARIANT_STRUCTURED (CONDITION, TYPENAME, ...) \
382
- INVARIANT_STRUCTURED (CONDITION, TYPENAME, __VA_ARGS__)
386
+ #define DATA_INVARIANT_STRUCTURED (CONDITION, TYPENAME, ...) \
387
+ EXPAND_MACRO ( INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) )
383
388
384
389
// Legacy annotations
385
390
0 commit comments