cprover_library.h

Go to the documentation of this file.

#pragma once
 
#include <string>
#include <vector>
#include <util/irep/irep.h>
 
class languaget;
class contextt;
class goto_functionst;
 
/* Registers the bundled internal libc headers and sources with
 * file_operations. */
void register_bundled_libc();
 
/* Returns the path the headers of the internal libc have been extracted to
 * or NULL if no library is configured (either via config.ansi_c.lib or during
 * build time). */
const std::string *internal_libc_header_dir();
 
/* Adds the internal libc to `context` by parsing and linking all C sources.
 *
 * Note that parsing the entire ESBMC standard library is a slow process.
 */
void add_bundled_library_sources(
  contextt &context,
  const languaget &c_language);
 
void add_cprover_library(
  contextt &context,
  const languaget *language = nullptr);

void record_library_symbol(const irep_idt &id);

void prune_unreferenced_library_functions(
  contextt &context,
  const goto_functionst *prelowered = nullptr);

void assert_no_pruned_calls(const goto_functionst &functions);