ld_converter Class Reference

#include <ld_converter.h>

Public Member Functions
	ld_converter (contextt &context, const LdIR &ir)
void	convert ()
	Build the symbol table, ld::scan_loop, and __ESBMC_main skeleton.
void	prepend_static_init ()
	Prepend static-lifetime initialisation assignments to __ESBMC_main.
void	enable_fault_injection (bool enabled)
	Fault-injection mode: negate contact polarities / degrade coil assignments.

Constructor & Destructor Documentation

ld_converter()

ld_converter::ld_converter	(	contextt &	context,
		const LdIR &	ir )

Member Function Documentation

convert()

void ld_converter::convert

(

)

Build the symbol table, ld::scan_loop, and __ESBMC_main skeleton.

Throws std::runtime_error on internal errors.

enable_fault_injection()

void ld_converter::enable_fault_injection ( bool enabled )

inline

Fault-injection mode: negate contact polarities / degrade coil assignments.

Used by WP1 validation to plant known semantic errors.

prepend_static_init()

void ld_converter::prepend_static_init

(

)

Prepend static-lifetime initialisation assignments to __ESBMC_main.

Call this after all symbols (including those from property_encoder) have been added to the context.

---

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

• src/ld-frontend/ir_gen/ld_converter.h
• src/ld-frontend/ir_gen/ld_converter.cpp