CBMC
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()

static 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()

static 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.