read_cbmc_goto_object.h File Reference

#include <istream>
#include <map>
#include <string>
#include <vector>
#include <util/irep/irep.h>

Include dependency graph for read_cbmc_goto_object.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	cbmc_irep_readert
	Low-level reader for the CBMC goto-binary format (version 6). More...
struct	cbmc_symbolt
	Intermediate, pre-adaptation parse of a CBMC symbol (mirrors cbmc.rs CBMCSymbol). More...
struct	cbmc_instructiont
	Intermediate parse of a CBMC instruction (mirrors cbmc.rs CBMCInstruction). More...
struct	cbmc_functiont
struct	cbmc_parse_resultt

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').
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.
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

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.