cprover_libc_sources.cpp File Reference

#include <c2goto/cprover_library.h>
#include <util/config/config.h>
#include <util/lang/language.h>
#include <clang-c-frontend/AST/vfs_paths.h>
#include <util/base/filesystem.h>
#include <util/message/message.h>
#include <libc.h>
#include <libm.h>
#include <libmusl.h>
#include <libmuslhdr.h>
#include <libcpp.h>
#include <headers/libc_hdr.h>

Include dependency graph for cprover_libc_sources.cpp:

Macros
#define	ESBMC_FLAIL(body, size, ...)
#define	ESBMC_FLAIL(body, size, ...)
#define	ESBMC_FLAIL(body, size, ...)
#define	_LIBM_H
#define	_ENDIAN_H
#define	__NEED_uint16_t
#define	__NEED_uint32_t
#define	__NEED_uint64_t
#define	__PDP_ENDIAN   3412
#define	BIG_ENDIAN   __BIG_ENDIAN
#define	LITTLE_ENDIAN   __LITTLE_ENDIAN
#define	PDP_ENDIAN   __PDP_ENDIAN
#define	BYTE_ORDER   __BYTE_ORDER
#define	htobe16(x)
#define	be16toh(x)
#define	htobe32(x)
#define	be32toh(x)
#define	htobe64(x)
#define	be64toh(x)
#define	htole16(x)
#define	le16toh(x)
#define	htole32(x)
#define	le32toh(x)
#define	htole64(x)
#define	le64toh(x)
#define	WANT_ROUNDING   1
#define	WANT_SNAN   0
#define	issignalingf_inline(x)
#define	issignaling_inline(x)
#define	predict_true(x)
#define	predict_false(x)
#define	_UNUSED(expr)
#define	FORCE_EVAL(x)
#define	asuint(f)
#define	asfloat(i)
#define	asuint64(f)
#define	asdouble(i)
#define	EXTRACT_WORDS(hi, lo, d)
#define	GET_HIGH_WORD(hi, d)
#define	GET_LOW_WORD(lo, d)
#define	INSERT_WORDS(d, hi, lo)
#define	SET_HIGH_WORD(d, hi)
#define	SET_LOW_WORD(d, lo)
#define	GET_FLOAT_WORD(w, d)
#define	SET_FLOAT_WORD(d, w)
#define	ESBMC_FLAIL(body, size, ...)
#define	ESBMC_FLAIL(body, size, ...)
#define	ESBMC_FLAIL(body, size, ...)
#define	ESBMC_FLAIL(body, size, ...)
#define	ESBMC_FLAIL(body, size, ...)

Functions
void	register_bundled_libc ()
const std::string *	internal_libc_header_dir ()
static std::string	get_filename_from_path (const std::string &path)
void	add_bundled_library_sources (contextt &context, const languaget &c_language)

Variables
static const std::string	vfs_prefix = clang_vfs_root() + "/libc"
static const std::string	vfs_headers = vfs_prefix + "/headers"
static const std::string	vfs_library = vfs_prefix + "/library"
static const std::string	vfs_libm = vfs_library + "/libm"
static const std::string	vfs_musl = vfs_libm + "/musl"
static const std::string	vfs_cpp = vfs_library + "/cpp"
static const std::string	vfs_python = vfs_library + "/python"
static const std::string	vfs_solidity = vfs_library + "/solidity"

Macro Definition Documentation

__NEED_uint16_t

#define __NEED_uint16_t

__NEED_uint32_t

#define __NEED_uint32_t

__NEED_uint64_t

#define __NEED_uint64_t

__PDP_ENDIAN

#define __PDP_ENDIAN   3412

_ENDIAN_H

#define _ENDIAN_H

_LIBM_H

#define _LIBM_H

_UNUSED

#define _UNUSED

(

expr

)

Value:

do { (void)(expr); } while (0)

asdouble

#define asdouble

(

i

)

Value:

((union{uint64_t _i; double _f;}){i})._f

asfloat

#define asfloat

(

i

)

Value:

((union{uint32_t _i; float _f;}){i})._f

asuint

#define asuint

(

f

)

Value:

((union{float _f; uint32_t _i;}){f})._i

asuint64

#define asuint64

(

f

)

Value:

((union{double _f; uint64_t _i;}){f})._i

be16toh

#define be16toh

(

x

)

Value:

__bswap16(x)

be32toh

#define be32toh

(

x

)

Value:

__bswap32(x)

be64toh

#define be64toh

(

x

)

Value:

__bswap64(x)

BIG_ENDIAN

#define BIG_ENDIAN   __BIG_ENDIAN

BYTE_ORDER

#define BYTE_ORDER   __BYTE_ORDER

ESBMC_FLAIL [1/8]

#define ESBMC_FLAIL	(		body,
			size,
			... )

Value:

parse(vfs_libm + "/" #__VA_ARGS__);

ESBMC_FLAIL [2/8]

#define ESBMC_FLAIL	(		body,
			size,
			... )

Value:

parse(vfs_library + "/" #__VA_ARGS__);

ESBMC_FLAIL [3/8]

#define ESBMC_FLAIL	(		body,
			size,
			... )

Value:

  file_operations::filesystemt::get().add_bundled(                             \
    vfs_cpp + "/" #__VA_ARGS__, body, size);

ESBMC_FLAIL [4/8]

#define ESBMC_FLAIL	(		body,
			size,
			... )

Value:

  file_operations::filesystemt::get().add_bundled(                             \
    vfs_musl + "/" #__VA_ARGS__, body, size);

ESBMC_FLAIL [5/8]

#define ESBMC_FLAIL	(		body,
			size,
			... )

Value:

  file_operations::filesystemt::get().add_bundled(                             \
    vfs_musl + "/" #__VA_ARGS__, body, size);

ESBMC_FLAIL [6/8]

#define ESBMC_FLAIL	(		body,
			size,
			... )

Value:

  file_operations::filesystemt::get().add_bundled(                             \
    vfs_libm + "/" #__VA_ARGS__, body, size);

ESBMC_FLAIL [7/8]

#define ESBMC_FLAIL	(		body,
			size,
			... )

Value:

  file_operations::filesystemt::get().add_bundled(                             \
    vfs_library + "/" #__VA_ARGS__, body, size);

ESBMC_FLAIL [8/8]

#define ESBMC_FLAIL	(		body,
			size,
			... )

Value:

  file_operations::filesystemt::get().add_bundled(                             \
    vfs_headers + "/" #__VA_ARGS__, body, size);

EXTRACT_WORDS

#define EXTRACT_WORDS	(		hi,
			lo,
			d )

Value:

do {                                              \
  uint64_t __u = asuint64(d);                     \
  (hi) = __u >> 32;                               \
  (lo) = (uint32_t)__u;                           \
} while (0)

FORCE_EVAL

#define FORCE_EVAL

(

x

)

Value:

    do {                        \
    if (sizeof(x) == sizeof(float)) {         \
        fp_force_evalf(x);                \
    } else if (sizeof(x) == sizeof(double)) { \
        fp_force_eval(x);                 \
    } else {                                  \
        fp_force_evall(x);                \
    }                                         \
} while(0)

GET_FLOAT_WORD

#define GET_FLOAT_WORD	(		w,
			d )

Value:

do {                                              \
  (w) = asuint(d);                                \
} while (0)

GET_HIGH_WORD

#define GET_HIGH_WORD	(		hi,
			d )

Value:

do {                                              \
  (hi) = asuint64(d) >> 32;                       \
} while (0)

GET_LOW_WORD

#define GET_LOW_WORD	(		lo,
			d )

Value:

do {                                              \
  (lo) = (uint32_t)asuint64(d);                   \
} while (0)

htobe16

#define htobe16

(

x

)

Value:

__bswap16(x)

htobe32

#define htobe32

(

x

)

Value:

__bswap32(x)

htobe64

#define htobe64

(

x

)

Value:

__bswap64(x)

htole16

#define htole16

(

x

)

Value:

(uint16_t)(x)

htole32

#define htole32

(

x

)

Value:

(uint32_t)(x)

htole64

#define htole64

(

x

)

Value:

(uint64_t)(x)

INSERT_WORDS

#define INSERT_WORDS	(		d,
			hi,
			lo )

Value:

do {                                              \
  (d) = asdouble(((uint64_t)(hi)<<32) | (uint32_t)(lo)); \
} while (0)

issignaling_inline

#define issignaling_inline

(

x

)

Value:

0

issignalingf_inline

#define issignalingf_inline

(

x

)

Value:

0

le16toh

#define le16toh

(

x

)

Value:

(uint16_t)(x)

le32toh

#define le32toh

(

x

)

Value:

(uint32_t)(x)

le64toh

#define le64toh

(

x

)

Value:

(uint64_t)(x)

LITTLE_ENDIAN

#define LITTLE_ENDIAN   __LITTLE_ENDIAN

PDP_ENDIAN

#define PDP_ENDIAN   __PDP_ENDIAN

predict_false

#define predict_false

(

x

)

Value:

(x)

predict_true

#define predict_true

(

x

)

Value:

(x)

SET_FLOAT_WORD

#define SET_FLOAT_WORD	(		d,
			w )

Value:

do {                                              \
  (d) = asfloat(w);                               \
} while (0)

SET_HIGH_WORD

#define SET_HIGH_WORD	(		d,
			hi )

Value:

  INSERT_WORDS(d, hi, (uint32_t)asuint64(d))

SET_LOW_WORD

#define SET_LOW_WORD	(		d,
			lo )

Value:

  INSERT_WORDS(d, asuint64(d)>>32, lo)

WANT_ROUNDING

#define WANT_ROUNDING   1

WANT_SNAN

#define WANT_SNAN   0

Function Documentation

add_bundled_library_sources()

void add_bundled_library_sources	(	contextt &	context,
		const languaget &	c_language )

get_filename_from_path()

std::string get_filename_from_path ( const std::string & path )

static

internal_libc_header_dir()

const std::string * internal_libc_header_dir

(

)

register_bundled_libc()

void register_bundled_libc

(

)

Variable Documentation

vfs_cpp

const std::string vfs_cpp = vfs_library + "/cpp"

static

vfs_headers

const std::string vfs_headers = vfs_prefix + "/headers"

static

vfs_libm

const std::string vfs_libm = vfs_library + "/libm"

static

vfs_library

const std::string vfs_library = vfs_prefix + "/library"

static

vfs_musl

const std::string vfs_musl = vfs_libm + "/musl"

static

vfs_prefix

const std::string vfs_prefix = clang_vfs_root() + "/libc"

static

vfs_python

const std::string vfs_python = vfs_library + "/python"

static

vfs_solidity

const std::string vfs_solidity = vfs_library + "/solidity"

static