CBMC
dfcc_contract_clauses_codegent Class Reference

Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that build write sets or havoc write sets. More...

#include <dfcc_contract_clauses_codegen.h>

+ Collaboration diagram for dfcc_contract_clauses_codegent:

Public Member Functions

 dfcc_contract_clauses_codegent (goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library)
 
void gen_spec_assigns_instructions (const irep_idt &language_mode, const exprt::operandst &assigns_clause, goto_programt &dest)
 Generates instructions encoding the assigns_clause targets and adds them to dest. More...
 
void gen_spec_frees_instructions (const irep_idt &language_mode, const exprt::operandst &frees_clause, goto_programt &dest)
 Generates instructions encoding the frees_clause targets and adds them to dest. More...
 

Protected Member Functions

void encode_assignable_target_group (const irep_idt &language_mode, const conditional_target_group_exprt &group, goto_programt &dest)
 Generates GOTO instructions to build the representation of the given conditional target group. More...
 
void encode_assignable_target (const irep_idt &language_mode, const exprt &target, goto_programt &dest)
 Generates GOTO instructions to build the representation of the given assignable target. More...
 
void encode_freeable_target_group (const irep_idt &language_mode, const conditional_target_group_exprt &group, goto_programt &dest)
 Generates GOTO instructions to build the representation of the given conditional target group. More...
 
void encode_freeable_target (const irep_idt &language_mode, const exprt &target, goto_programt &dest)
 Generates GOTO instructions to build the representation of the given freeable target. More...
 
void inline_and_check_warnings (goto_programt &goto_program)
 Inlines all calls in the given program and checks that the only missing functions or functions without bodies are built-in functions, and that no other warnings happened. More...
 

Protected Attributes

goto_modeltgoto_model
 
message_handlertmessage_handler
 
messaget log
 
dfcc_librarytlibrary
 
namespacet ns
 

Detailed Description

Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that build write sets or havoc write sets.

Definition at line 35 of file dfcc_contract_clauses_codegen.h.

Constructor & Destructor Documentation

◆ dfcc_contract_clauses_codegent()

dfcc_contract_clauses_codegent::dfcc_contract_clauses_codegent ( goto_modelt goto_model,
message_handlert message_handler,
dfcc_libraryt library 
)
Parameters
goto_modelGOTO model being transformed
message_handlerUsed debug/warning/error messages
libraryThe contracts instrumentation library

Definition at line 31 of file dfcc_contract_clauses_codegen.cpp.

Member Function Documentation

◆ encode_assignable_target()

void dfcc_contract_clauses_codegent::encode_assignable_target ( const irep_idt language_mode,
const exprt target,
goto_programt dest 
)
protected

Generates GOTO instructions to build the representation of the given assignable target.

Definition at line 125 of file dfcc_contract_clauses_codegen.cpp.

◆ encode_assignable_target_group()

void dfcc_contract_clauses_codegent::encode_assignable_target_group ( const irep_idt language_mode,
const conditional_target_group_exprt group,
goto_programt dest 
)
protected

Generates GOTO instructions to build the representation of the given conditional target group.

Definition at line 98 of file dfcc_contract_clauses_codegen.cpp.

◆ encode_freeable_target()

void dfcc_contract_clauses_codegent::encode_freeable_target ( const irep_idt language_mode,
const exprt target,
goto_programt dest 
)
protected

Generates GOTO instructions to build the representation of the given freeable target.

Definition at line 214 of file dfcc_contract_clauses_codegen.cpp.

◆ encode_freeable_target_group()

void dfcc_contract_clauses_codegent::encode_freeable_target_group ( const irep_idt language_mode,
const conditional_target_group_exprt group,
goto_programt dest 
)
protected

Generates GOTO instructions to build the representation of the given conditional target group.

Definition at line 187 of file dfcc_contract_clauses_codegen.cpp.

◆ gen_spec_assigns_instructions()

void dfcc_contract_clauses_codegent::gen_spec_assigns_instructions ( const irep_idt language_mode,
const exprt::operandst assigns_clause,
goto_programt dest 
)

Generates instructions encoding the assigns_clause targets and adds them to dest.

Assumes that all targets in the clause are represented as plain expressions (i.e. an lambdas expressions introduced for function contract targets may are already instanciated).

Parameters
language_modeMode to use for fresh symbols
assigns_clauseSequence of targets to encode
destDestination program

Definition at line 43 of file dfcc_contract_clauses_codegen.cpp.

◆ gen_spec_frees_instructions()

void dfcc_contract_clauses_codegent::gen_spec_frees_instructions ( const irep_idt language_mode,
const exprt::operandst frees_clause,
goto_programt dest 
)

Generates instructions encoding the frees_clause targets and adds them to dest.

Assumes that all targets in the clause are represented as plain expressions (i.e. an lambdas expressions introduced for function contract targets may are already instanciated).

Parameters
language_modeMode to use for fresh symbols
frees_clauseSequence of targets to encode
destDestination program

Definition at line 71 of file dfcc_contract_clauses_codegen.cpp.

◆ inline_and_check_warnings()

void dfcc_contract_clauses_codegent::inline_and_check_warnings ( goto_programt goto_program)
protected

Inlines all calls in the given program and checks that the only missing functions or functions without bodies are built-in functions, and that no other warnings happened.

Definition at line 260 of file dfcc_contract_clauses_codegen.cpp.

Member Data Documentation

◆ goto_model

goto_modelt& dfcc_contract_clauses_codegent::goto_model
protected

Definition at line 77 of file dfcc_contract_clauses_codegen.h.

◆ library

dfcc_libraryt& dfcc_contract_clauses_codegent::library
protected

Definition at line 80 of file dfcc_contract_clauses_codegen.h.

◆ log

messaget dfcc_contract_clauses_codegent::log
protected

Definition at line 79 of file dfcc_contract_clauses_codegen.h.

◆ message_handler

message_handlert& dfcc_contract_clauses_codegent::message_handler
protected

Definition at line 78 of file dfcc_contract_clauses_codegen.h.

◆ ns

namespacet dfcc_contract_clauses_codegent::ns
protected

Definition at line 81 of file dfcc_contract_clauses_codegen.h.


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