cbmc_adapter.cpp File Reference

#include <goto-programs/cbmc_adapter.h>
#include <util/lang/c_types.h>
#include <util/message/message.h>
#include <algorithm>
#include <cstdlib>
#include <map>
#include <string>
#include <unordered_map>
#include <unordered_set>

Include dependency graph for cbmc_adapter.cpp:

Functions
unsigned	map_cbmc_instruction_type (unsigned cbmc_type)
	Maps a CBMC goto-program instruction-type value onto the matching ESBMC goto_program_instruction_typet value.
cbmc_adapted_resultt	adapt_cbmc_to_esbmc (cbmc_parse_resultt parsed)
	Rewrites CBMC irep conventions into ESBMC's.

Function Documentation

adapt_cbmc_to_esbmc()

cbmc_adapted_resultt adapt_cbmc_to_esbmc

(

cbmc_parse_resultt

parsed

)

Rewrites CBMC irep conventions into ESBMC's.

Faithful port of goto-transcoder's adapter.rs (ESBMCParseResult::from(CBMCParseResult)).

map_cbmc_instruction_type()

unsigned map_cbmc_instruction_type

(

unsigned

cbmc_type

)

Maps a CBMC goto-program instruction-type value onto the matching ESBMC goto_program_instruction_typet value.

CBMC and ESBMC share the goto_program_instruction_typet numbering for every kind that reaches a finished straight-line/control-flow binary, so those map by identity. The kinds that diverge are handled explicitly:

• START_THREAD (6) / END_THREAD (7): CBMC encodes concurrency as instruction types, whereas ESBMC models it with __ESBMC_spawn_thread intrinsic calls and has no instruction-type counterpart.
• INCOMPLETE_GOTO (19): an unresolved goto that should not survive into a finished binary; ESBMC reuses 19 as a removed-enumerator gap. These divergent kinds are rejected with a named diagnostic (the function aborts) rather than being silently mis-cast in symex. cbmc_type is a raw CBMC instruction-type value; the return value is the ESBMC enumerator.