cbmc_irep_readert Class Reference

Low-level reader for the CBMC goto-binary format (version 6). More...

#include <read_cbmc_goto_object.h>

Public Member Functions
	cbmc_irep_readert (std::istream &in)
unsigned	read_word ()
	CBMC encodes words as little-endian 7-bit varints (continuation bit 0x80).
std::string	read_string ()
	Reads a NUL-terminated string with backslash escaping (same as ESBMC).
irep_idt	read_string_ref ()
	Reads a word-tagged, cached string reference.
void	read_reference (irept &dest)
	Reads a word-tagged, cached irep reference (with S/N/C children).
bool	failed () const
	True once a malformed encoding was hit.

Detailed Description

Low-level reader for the CBMC goto-binary format (version 6).

Mirrors irep_serializationt but uses CBMC's 7-bit varint word encoding instead of ESBMC's big-endian 32-bit words. The S/N/C reference grammar and the string/irep reference caching are identical to ESBMC's reader.

Constructor & Destructor Documentation

cbmc_irep_readert()

cbmc_irep_readert::cbmc_irep_readert ( std::istream & in )

inlineexplicit

Member Function Documentation

failed()

bool cbmc_irep_readert::failed ( ) const

inline

True once a malformed encoding was hit.

The reader then abandons the rest of the parse cleanly (subsequent reads no-op) instead of aborting the process, so a corrupt CBMC binary is a recoverable error rather than a crash (roadmap §4.7). parse_cbmc_goto surfaces this as its bool return.

read_reference()

void cbmc_irep_readert::read_reference

(

irept &

dest

)

Reads a word-tagged, cached irep reference (with S/N/C children).

read_string()

std::string cbmc_irep_readert::read_string

(

)

Reads a NUL-terminated string with backslash escaping (same as ESBMC).

read_string_ref()

irep_idt cbmc_irep_readert::read_string_ref

(

)

Reads a word-tagged, cached string reference.

read_word()

unsigned cbmc_irep_readert::read_word

(

)

CBMC encodes words as little-endian 7-bit varints (continuation bit 0x80).

---

The documentation for this class was generated from the following files:

• src/goto-programs/read_cbmc_goto_object.h
• src/goto-programs/read_cbmc_goto_object.cpp