cprover
Loading...
Searching...
No Matches
boolbv_overflow.cpp File Reference
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/bitvector_types.h>
#include <util/invariant.h>
#include "boolbv.h"
Include dependency graph for boolbv_overflow.cpp:

Go to the source code of this file.

Functions

static bvt mult_overflow_result (propt &prop, const bvt &bv0, const bvt &bv1, bv_utilst::representationt rep)
static bvt shl_overflow_result (propt &prop, const bvt &bv0, const bvt &bv1, bv_utilst::representationt rep0, bv_utilst::representationt rep1)

Function Documentation

◆ mult_overflow_result()

bvt mult_overflow_result ( propt & prop,
const bvt & bv0,
const bvt & bv1,
bv_utilst::representationt rep )
static

Definition at line 16 of file boolbv_overflow.cpp.

◆ shl_overflow_result()

bvt shl_overflow_result ( propt & prop,
const bvt & bv0,
const bvt & bv1,
bv_utilst::representationt rep0,
bv_utilst::representationt rep1 )
static

Definition at line 53 of file boolbv_overflow.cpp.