CBMC: /home/runner/work/cbmc/cbmc/src/cpp/cprover_library.cpp Source File

17 static std::string get_cprover_library_text(

18 const std::set<irep_idt> &functions,

19 const symbol_table_baset &symbol_table)

20{

21 std::ostringstream library_text;

22

23 library_text << "#line 1 \"<builtin-library>\"\n"

24 << "#undef inline\n";

25

26 // cprover_library.inc may not have been generated when running Doxygen, thus

27 // make Doxygen skip this part

29 const struct cprover_library_entryt cprover_library[] =

30#include "cprover_library.inc" // IWYU pragma: keep

31 ; // NOLINT(whitespace/semicolon)

33

34 return get_cprover_library_text(

35 functions, symbol_table, cprover_library, library_text.str());

36}

38 void cprover_cpp_library_factory(

39 const std::set<irep_idt> &functions,

40 const symbol_table_baset &symbol_table,

41 symbol_table_baset &dest_symbol_table,

42 message_handlert &message_handler)

43{

44 if(config.ansi_c.lib == configt::ansi_ct::libt::LIB_NONE)

45 return;

46

47 const std::string library_text =

48 get_cprover_library_text(functions, symbol_table);

49

50 add_library(library_text, dest_symbol_table, message_handler);

51}

get_cprover_library_text

static std::string get_cprover_library_text(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, const bool force_load)

Definition cprover_library.cpp:19

add_library

void add_library(const std::string &src, symbol_table_baset &symbol_table, message_handlert &message_handler, const std::set< irep_idt > &keep)

Parses and typechecks the given src and adds its contents to the symbol table.

Definition cprover_library.cpp:121

cprover_library.h

config

configt config

Definition config.cpp:25

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

configt::ansi_c

struct configt::ansi_ct ansi_c

message_handlert

Definition message.h:27

symbol_table_baset

The symbol table base class interface.

Definition symbol_table_base.h:23

config.h

cprover_cpp_library_factory

void cprover_cpp_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)

Definition cprover_library.cpp:38

cprover_library.h

configt::ansi_ct::libt::LIB_NONE

@ LIB_NONE

cprover_library_entryt

Definition cprover_library.h:21