overflow_checkst Struct Reference

What goto_check will instrument on the guards this pass emits. More...

#include <goto_invariant_synthesis.h>

Public Attributes
bool	signed_arith = false
	–overflow-check: signed arithmetic is instrumented.
bool	unsigned_arith = false
	–unsigned-overflow-check: unsigned arithmetic is instrumented too (goto_check.cpp, enable_unsigned_overflow_check).

Detailed Description

What goto_check will instrument on the guards this pass emits.

It checks every instruction guard, including the synthesised ones, so a closed form emitted at a type it watches draws overflow claims on arithmetic the user never wrote.

Member Data Documentation

signed_arith

bool overflow_checkst::signed_arith = false

–overflow-check: signed arithmetic is instrumented.

unsigned_arith

bool overflow_checkst::unsigned_arith = false

–unsigned-overflow-check: unsigned arithmetic is instrumented too (goto_check.cpp, enable_unsigned_overflow_check).

Under it no integer type is safe to emit the closed form at, so synthesis declines outright.

---

The documentation for this struct was generated from the following file:

• src/goto-programs/goto_invariant_synthesis.h