Skip to content
BitVecMustPush

BitVecMustPush

Description

Aborting variant of BitVecPush. See that macro for parameter semantics and success-state effects.

Success

Returns to the caller. The underlying BitVecPush call succeeded; see BitVecPush for the post-state.

Failure

Does not return - aborts via LOG_FATAL / SysAbort when the underlying BitVecPush call returns false.

Usage example (Cross-references)

Usage examples (Cross-references)
        do {                                                                                                               \
            if (!BitVecPush((bv), (value))) {                                                                              \
                LOG_FATAL("BitVecMustPush failed");                                                                        \
            }                                                                                                              \
        } while (0)
Last updated on