Symbolic Execution of ANSI-C. More...

#include "bmc.h"
#include <chrono>
#include <iostream>
#include <util/exception_utils.h>
#include <util/exit_codes.h>
#include <langapi/language_util.h>
#include <goto-programs/graphml_witness.h>
#include <goto-programs/json_goto_trace.h>
#include <goto-programs/xml_goto_trace.h>
#include <goto-symex/build_goto_trace.h>
#include <goto-symex/memory_model_pso.h>
#include <goto-symex/show_program.h>
#include <goto-symex/show_vcc.h>
#include <goto-symex/slice.h>
#include <goto-symex/slice_by_trace.h>
#include <linking/static_lifetime_init.h>
#include <goto-checker/solver_factory.h>
#include "counterexample_beautification.h"
#include "fault_localization.h"

Include dependency graph for bmc.cpp:

Go to the source code of this file.

Detailed Description

Symbolic Execution of ANSI-C.

Definition in file bmc.cpp.