ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
bigint.cpp File Reference
#include <big-int/allocainc.h>
#include <big-int/bigint.hh>
#include <cctype>
#include <climits>
#include <cstdio>
#include <cstdlib>
#include <cstring>
Include dependency graph for bigint.cpp:

Macros

#define error(x)

Typedefs

typedef BigInt::llong_t llong_t
typedef BigInt::ullong_t ullong_t
typedef BigInt::onedig_t onedig_t
typedef BigInt::twodig_t twodig_t

Functions

unsigned adjust_size (unsigned size)
int digit_cmp (onedig_t const *a, onedig_t const *b, unsigned n)
static onedig_t digit_add (onedig_t const *d1, unsigned l1, onedig_t const *d2, unsigned l2, onedig_t *r)
static void digit_sub (onedig_t const *d1, unsigned l1, onedig_t const *d2, unsigned l2, onedig_t *r)
static onedig_t digit_mul (onedig_t *b, unsigned l, onedig_t d)
static void digit_mul (onedig_t const *a, unsigned la, onedig_t const *b, unsigned lb, onedig_t *r)
static onedig_t digit_div (onedig_t *b, unsigned l, onedig_t d)
onedig_t guess_q (onedig_t const *r, onedig_t const *y)
static onedig_t multiply_and_subtract (onedig_t *r, onedig_t const *y, unsigned l, onedig_t q)
static void add_back (onedig_t *r, onedig_t const *y, unsigned l)
static void digit_div (onedig_t *r, const onedig_t *y, unsigned yl, onedig_t *q, unsigned ql)
void digit_set (ullong_t ul, onedig_t d[small], unsigned &l)

Variables

static const unsigned small = BigInt::small
static const int single_bits = sizeof(onedig_t) * CHAR_BIT
static const twodig_t base = twodig_t(1) << single_bits
static const twodig_t single_max = base - 1

Macro Definition Documentation

◆ error

#define error ( x)
Value:
fprintf(stderr, "%s\n", x); \
abort()
int fprintf(FILE *__ESBMC_restrict stream, const char *__ESBMC_restrict format,...)
FILE * stderr

Typedef Documentation

◆ llong_t

◆ onedig_t

◆ twodig_t

◆ ullong_t

Function Documentation

◆ add_back()

void add_back ( onedig_t * r,
onedig_t const * y,
unsigned l )
static

◆ adjust_size()

unsigned adjust_size ( unsigned size)
inline

◆ digit_add()

onedig_t digit_add ( onedig_t const * d1,
unsigned l1,
onedig_t const * d2,
unsigned l2,
onedig_t * r )
static

◆ digit_cmp()

int digit_cmp ( onedig_t const * a,
onedig_t const * b,
unsigned n )
inline

◆ digit_div() [1/2]

onedig_t digit_div ( onedig_t * b,
unsigned l,
onedig_t d )
static

◆ digit_div() [2/2]

void digit_div ( onedig_t * r,
const onedig_t * y,
unsigned yl,
onedig_t * q,
unsigned ql )
static

◆ digit_mul() [1/2]

onedig_t digit_mul ( onedig_t * b,
unsigned l,
onedig_t d )
static

◆ digit_mul() [2/2]

void digit_mul ( onedig_t const * a,
unsigned la,
onedig_t const * b,
unsigned lb,
onedig_t * r )
static

◆ digit_set()

void digit_set ( ullong_t ul,
onedig_t d[small],
unsigned & l )
inline

◆ digit_sub()

void digit_sub ( onedig_t const * d1,
unsigned l1,
onedig_t const * d2,
unsigned l2,
onedig_t * r )
static

◆ guess_q()

onedig_t guess_q ( onedig_t const * r,
onedig_t const * y )
inline

◆ multiply_and_subtract()

onedig_t multiply_and_subtract ( onedig_t * r,
onedig_t const * y,
unsigned l,
onedig_t q )
static

Variable Documentation

◆ base

const twodig_t base = twodig_t(1) << single_bits
static

◆ single_bits

const int single_bits = sizeof(onedig_t) * CHAR_BIT
static

◆ single_max

const twodig_t single_max = base - 1
static

◆ small

const unsigned small = BigInt::small
static