CBMC: /home/runner/work/cbmc/cbmc/src/cprover/state_encoding.cpp File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Functions | Variables

state_encoding.cpp File Reference

#include "state_encoding.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/mathematical_expr.h>
#include <util/pointer_expr.h>
#include <util/prefix.h>
#include <util/simplify_expr.h>
#include <util/std_code.h>
#include <goto-programs/goto_model.h>
#include "equality_propagation.h"
#include "instrument_contracts.h"
#include "sentinel_dll.h"
#include "solver.h"
#include "state.h"
#include "state_encoding_targets.h"
#include "variable_encoding.h"
#include <algorithm>
#include <iostream>

+ Include dependency graph for state_encoding.cpp:

Go to the source code of this file.

Classes

class state_encodingt

Functions

static exprt simplifying_not (exprt src)

void state_encoding (const goto_modelt &goto_model, bool program_is_inlined, std::optional< irep_idt > contract, encoding_targett &dest)

void state_encoding (const goto_modelt &goto_model, state_encoding_formatt state_encoding_format, bool program_is_inlined, std::optional< irep_idt > contract, std::ostream &out)

void variable_encoding (const goto_modelt &goto_model, state_encoding_formatt state_encoding_format, std::ostream &out)

solver_resultt state_encoding_solver (const goto_modelt &goto_model, bool program_is_inlined, std::optional< irep_idt > contract, const solver_optionst &solver_options)

Variables

std::set< irep_idt > no_body_warnings

Function Documentation

◆ simplifying_not()

static exprt simplifying_not ( exprt src )

static

Definition at line 630 of file state_encoding.cpp.

◆ state_encoding() [1/2]

void state_encoding ( const goto_modelt & goto_model,

bool program_is_inlined,

std::optional< irep_idt > contract,

encoding_targett & dest

)

Definition at line 1116 of file state_encoding.cpp.

◆ state_encoding() [2/2]

void state_encoding ( const goto_modelt & goto_model,

state_encoding_formatt state_encoding_format,

bool program_is_inlined,

std::optional< irep_idt > contract,

std::ostream & out

)

Definition at line 1178 of file state_encoding.cpp.

◆ state_encoding_solver()

solver_resultt state_encoding_solver ( const goto_modelt & goto_model,

bool program_is_inlined,

std::optional< irep_idt > contract,

const solver_optionst & solver_options

)

Definition at line 1236 of file state_encoding.cpp.

◆ variable_encoding()

void variable_encoding ( const goto_modelt & goto_model,

state_encoding_formatt state_encoding_format,

std::ostream & out

)

Definition at line 1204 of file state_encoding.cpp.

Variable Documentation

◆ no_body_warnings

std::set<irep_idt> no_body_warnings

Definition at line 645 of file state_encoding.cpp.