@@ -249,6 +249,11 @@ invariant_violated_string(
249249#define __this_function__ __func__
250250#endif
251251
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+
252257#define GET_MACRO (X1, X2, X3, X4, X5, X6, MACRO, ...) MACRO
253258
254259// This macro dispatches to the macros MACRO<n> (with 1 <= n <= 6) and calls
@@ -257,16 +262,16 @@ invariant_violated_string(
257262#define REDIRECT (MACRO, ...) \
258263 do \
259264 { \
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__)); \
270275 } while (false )
271276
272277#define INVARIANT2 (CONDITION, REASON ) \
@@ -311,7 +316,7 @@ invariant_violated_string(
311316// Short hand macros. The variants *_STRUCTURED below allow to specify a custom
312317// exception, and are equivalent to INVARIANT_STRUCTURED.
313318
314- #define INVARIANT (...) REDIRECT(INVARIANT, __VA_ARGS__)
319+ #define INVARIANT (...) EXPAND_MACRO( REDIRECT(INVARIANT, __VA_ARGS__) )
315320
316321// The condition should only contain (unmodified) inputs to the method. Inputs
317322// include arguments passed to the function, as well as member variables that
@@ -325,10 +330,10 @@ invariant_violated_string(
325330#define PRECONDITION2 (CONDITION, DIAGNOSTICS ) \
326331 INVARIANT3 (CONDITION, " Precondition" , DIAGNOSTICS)
327332
328- #define PRECONDITION (...) REDIRECT(PRECONDITION, __VA_ARGS__)
333+ #define PRECONDITION (...) EXPAND_MACRO( REDIRECT(PRECONDITION, __VA_ARGS__) )
329334
330335#define PRECONDITION_STRUCTURED (CONDITION, TYPENAME, ...) \
331- INVARIANT_STRUCTURED (CONDITION, TYPENAME, __VA_ARGS__)
336+ EXPAND_MACRO ( INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) )
332337
333338// The condition should only contain variables that will be returned /
334339// output without further modification.
@@ -342,10 +347,10 @@ invariant_violated_string(
342347#define POSTCONDITION2 (CONDITION, DIAGNOSTICS ) \
343348 INVARIANT3 (CONDITION, " Postcondition" , DIAGNOSTICS)
344349
345- #define POSTCONDITION (...) REDIRECT(POSTCONDITION, __VA_ARGS__)
350+ #define POSTCONDITION (...) EXPAND_MACRO( REDIRECT(POSTCONDITION, __VA_ARGS__) )
346351
347352#define POSTCONDITION_STRUCTURED (CONDITION, TYPENAME, ...) \
348- INVARIANT_STRUCTURED (CONDITION, TYPENAME, __VA_ARGS__)
353+ EXPAND_MACRO ( INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) )
349354
350355// The condition should only contain (unmodified) values that were
351356// changed by a previous method call.
@@ -359,15 +364,15 @@ invariant_violated_string(
359364#define CHECK_RETURN2 (CONDITION, DIAGNOSTICS ) \
360365 INVARIANT3 (CONDITION, " Check return value" , DIAGNOSTICS)
361366
362- #define CHECK_RETURN (...) REDIRECT(CHECK_RETURN, __VA_ARGS__)
367+ #define CHECK_RETURN (...) EXPAND_MACRO( REDIRECT(CHECK_RETURN, __VA_ARGS__) )
363368
364369#define CHECK_RETURN_STRUCTURED (CONDITION, TYPENAME, ...) \
365- INVARIANT_STRUCTURED (CONDITION, TYPENAME, __VA_ARGS__)
370+ EXPAND_MACRO ( INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) )
366371
367372// This should be used to mark dead code
368373#define UNREACHABLE INVARIANT2 (false , " Unreachable" )
369374#define UNREACHABLE_STRUCTURED (TYPENAME, ...) \
370- INVARIANT_STRUCTURED (false , TYPENAME, __VA_ARGS__)
375+ EXPAND_MACRO ( INVARIANT_STRUCTURED(false , TYPENAME, __VA_ARGS__) )
371376
372377// This condition should be used to document that assumptions that are
373378// made on goto_functions, goto_programs, exprts, etc. being well formed.
@@ -376,10 +381,10 @@ invariant_violated_string(
376381#define DATA_INVARIANT3 (CONDITION, REASON, DIAGNOSTICS ) \
377382 INVARIANT3 (CONDITION, REASON, DIAGNOSTICS)
378383
379- #define DATA_INVARIANT (...) REDIRECT(DATA_INVARIANT, __VA_ARGS__)
384+ #define DATA_INVARIANT (...) EXPAND_MACRO( REDIRECT(DATA_INVARIANT, __VA_ARGS__) )
380385
381386#define DATA_INVARIANT_STRUCTURED (CONDITION, TYPENAME, ...) \
382- INVARIANT_STRUCTURED (CONDITION, TYPENAME, __VA_ARGS__)
387+ EXPAND_MACRO ( INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) )
383388
384389// Legacy annotations
385390
0 commit comments