#include <goto-programs/read_cbmc_goto_object.h>
#include <goto-programs/cbmc_adapter.h>
#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_program_irep.h>
#include <util/lang/c_types.h>
#include <util/config/config.h>
#include <util/expr/expr_util.h>
#include <util/irep/migrate.h>
#include <util/message/message.h>
#include <util/irep/std_expr.h>
#include <util/symtab/symbol.h>
#include <cassert>
#include <cstdint>
#include <cstdlib>
#include <utility>

Include dependency graph for read_cbmc_goto_object.cpp:

Functions
bool	is_cbmc_goto_magic (const unsigned char header[4])
	True if the 4-byte header is the CBMC goto-binary magic (0x7f 'G' 'B' 'F').
static bool	implausible_count (std::istream &in, unsigned count, const char *what)
bool	parse_cbmc_goto (std::istream &in, const std::string &filename, cbmc_parse_resultt &result)
	Parses a CBMC goto-binary stream (header 0x7f 'G' 'B' 'F', version 6) into the intermediate, still-CBMC-convention structures above.
static void	set_object_alignment (symbolt &symbol)
bool	read_cbmc_goto_object (std::istream &in, const std::string &filename, contextt &context, goto_functionst &goto_functions)
	Reads a CBMC goto-binary, adapts it to ESBMC irep conventions, and populates the symbol table and goto functions — the CBMC-format counterpart of read_bin_goto_object.

Function Documentation

◆ implausible_count()

bool implausible_count	(	std::istream &	in,
		unsigned	count,
		const char *	what )

static

◆ is_cbmc_goto_magic()

bool is_cbmc_goto_magic ( const unsigned char header[4] )

True if the 4-byte header is the CBMC goto-binary magic (0x7f 'G' 'B' 'F').

ESBMC's own goto-binary format starts with 'G' 'B' 'F' (no leading 0x7f).

◆ parse_cbmc_goto()

bool parse_cbmc_goto	(	std::istream &	in,
		const std::string &	filename,
		cbmc_parse_resultt &	result )

Parses a CBMC goto-binary stream (header 0x7f 'G' 'B' 'F', version 6) into the intermediate, still-CBMC-convention structures above.

Returns true on error. Mirrors cbmc.rs process_cbmc_file.

◆ read_cbmc_goto_object()

bool read_cbmc_goto_object	(	std::istream &	in,
		const std::string &	filename,
		contextt &	context,
		goto_functionst &	goto_functions )

Reads a CBMC goto-binary, adapts it to ESBMC irep conventions, and populates the symbol table and goto functions — the CBMC-format counterpart of read_bin_goto_object.

Returns true on error.

◆ set_object_alignment()

void set_object_alignment ( symbolt & symbol )