cprover_library.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANSI_C_CPROVER_LIBRARY_H
#define CPROVER_ANSI_C_CPROVER_LIBRARY_H
 
#include <set>
 
#include <util/irep.h>
 
class message_handlert;
class symbol_table_baset;
 
struct cprover_library_entryt
{
  const char *function;
  const char *model;
};
 
std::string get_cprover_library_text(
  const std::set<irep_idt> &functions,
  const symbol_table_baset &,
  const struct cprover_library_entryt[],
  const std::string &prologue,
  const bool force_load = false);

void add_library(
  const std::string &src,
  symbol_table_baset &,
  message_handlert &,
  const std::set<irep_idt> &keep = {});
 
void cprover_c_library_factory(
  const std::set<irep_idt> &functions,
  const symbol_table_baset &,
  symbol_table_baset &,
  message_handlert &);

void cprover_c_library_factory_force_load(
  const std::set<irep_idt> &functions,
  symbol_table_baset &symbol_table,
  message_handlert &message_handler);
 
#endif // CPROVER_ANSI_C_CPROVER_LIBRARY_H