Merge pull request #858 from tautschnig/dump-c-typedef
Fix dump-c output involving typedef names
This commit is contained in:
Daniel Kroening
GitHub
commit
c7ce527327
|
|
@ -8,6 +8,8 @@
|
|||
* GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions
|
||||
* GOTO-INSTRUMENT: New option --undefined-function-is-assume-false
|
||||
* GOTO-INSTRUMENT: New option --remove-function-body
|
||||
* GOTO-INSTRUMENT: New option --use-all-headers, changed --use-system-headers to
|
||||
--no-system-headers
|
||||
|
||||
|
||||
5.7
|
||||
|
|
|
|||
|
|
@ -0,0 +1,19 @@
|
|||
#include<stdarg.h>
|
||||
#include<stdlib.h>
|
||||
|
||||
void bb_verror_msg(const char *s, va_list p, const char *strerr) {
|
||||
}
|
||||
|
||||
void bb_error_msg(const char *s, ...)
|
||||
{
|
||||
va_list p;
|
||||
va_start(p, s);
|
||||
bb_verror_msg(s, p, NULL);
|
||||
va_end(p);
|
||||
}
|
||||
|
||||
int main() {
|
||||
bb_error_msg("FOOO");
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
--dump-c
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
va_list
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
@ -0,0 +1,69 @@
|
|||
typedef long int off_t;
|
||||
typedef signed char smallint;
|
||||
|
||||
typedef struct chain_s {
|
||||
struct node_s *first;
|
||||
struct node_s *last;
|
||||
const char *programname;
|
||||
} chain;
|
||||
|
||||
typedef struct func_s {
|
||||
struct chain_s body;
|
||||
} func;
|
||||
|
||||
typedef struct node_s {
|
||||
struct node_s *n;
|
||||
} node;
|
||||
|
||||
typedef struct dumper_t_x {
|
||||
node n;
|
||||
off_t dump_skip;
|
||||
signed int dump_length;
|
||||
smallint dump_vflag;
|
||||
} dumper_t;
|
||||
|
||||
typedef struct FS_x {
|
||||
struct FS *nextfs;
|
||||
signed int bcnt;
|
||||
} FS;
|
||||
|
||||
dumper_t * alloc_dumper(void) {
|
||||
return (void*) 0;
|
||||
}
|
||||
|
||||
typedef unsigned int uint32_t;
|
||||
|
||||
const uint32_t xx[2];
|
||||
|
||||
typedef struct node_s2 {
|
||||
uint32_t info;
|
||||
} node2;
|
||||
|
||||
typedef struct {
|
||||
int x;
|
||||
} anon_name;
|
||||
|
||||
typedef struct node_s3 {
|
||||
union {
|
||||
struct node_s *n;
|
||||
func *f;
|
||||
} r;
|
||||
} node3;
|
||||
|
||||
typedef int x_int;
|
||||
typedef int y_int;
|
||||
typedef x_int *p_int;
|
||||
|
||||
int main() {
|
||||
node n;
|
||||
chain c;
|
||||
dumper_t a;
|
||||
dumper_t b[3];
|
||||
node2* sn;
|
||||
anon_name d;
|
||||
node3* s3;
|
||||
y_int y;
|
||||
p_int p;
|
||||
alloc_dumper();
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -0,0 +1,10 @@
|
|||
CORE
|
||||
main.c
|
||||
--dump-c
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
--
|
||||
^warning: ignoring
|
||||
--
|
||||
This test should be run via chain.sh, which will try to recompile the dumped C
|
||||
code. Missing/incomplete typedef output would cause a failure.
|
||||
|
|
@ -0,0 +1,16 @@
|
|||
typedef struct
|
||||
{
|
||||
char bogus;
|
||||
} bb_mbstate_t;
|
||||
|
||||
int bb_wcrtomb(char *s, char wc, bb_mbstate_t *ps);
|
||||
|
||||
int bb_wcrtomb(char *s, char wc, bb_mbstate_t *ps)
|
||||
{
|
||||
return 1;
|
||||
}
|
||||
|
||||
int main() {
|
||||
bb_wcrtomb("foo", 'Z', (void*)1);
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -0,0 +1,10 @@
|
|||
CORE
|
||||
main.c
|
||||
--dump-c
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
--
|
||||
^warning: ignoring
|
||||
--
|
||||
This test should be run via chain.sh, which will try to recompile the dumped C
|
||||
code. Missing/incomplete typedef output would cause a failure.
|
||||
|
|
@ -0,0 +1,30 @@
|
|||
extern void* memset(void *, int, unsigned long);
|
||||
|
||||
typedef void (*__sighandler_t) (int);
|
||||
|
||||
typedef __sighandler_t sighandler_t;
|
||||
|
||||
typedef struct siginfo {
|
||||
int si_signo;
|
||||
} siginfo_t;
|
||||
|
||||
struct sigaction {
|
||||
union {
|
||||
__sighandler_t _sa_handler;
|
||||
void (*_sa_sigaction)(int, struct siginfo *, void *);
|
||||
} _u;
|
||||
};
|
||||
|
||||
#define sa_sigaction _u._sa_sigaction
|
||||
#define sa_handler _u._sa_handler
|
||||
|
||||
static void askpass_timeout(signed int ignore) {
|
||||
;
|
||||
}
|
||||
|
||||
int main() {
|
||||
struct sigaction sa, oldsa;
|
||||
memset(&sa, 0, sizeof(sa));
|
||||
sa.sa_handler = askpass_timeout;
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -0,0 +1,10 @@
|
|||
CORE
|
||||
main.c
|
||||
--dump-c
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
--
|
||||
^warning: ignoring
|
||||
--
|
||||
This test should be run via chain.sh, which will try to recompile the dumped C
|
||||
code. Missing/incomplete typedef output would cause a failure.
|
||||
|
|
@ -0,0 +1,23 @@
|
|||
#ifndef _WIN32
|
||||
|
||||
#include <signal.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
void sig_block(int sig)
|
||||
{
|
||||
sigset_t ss;
|
||||
sigemptyset(&ss);
|
||||
sigaddset(&ss, sig);
|
||||
sigprocmask(SIG_BLOCK, &ss, NULL);
|
||||
}
|
||||
|
||||
int main() {
|
||||
sig_block(0);
|
||||
return 0;
|
||||
}
|
||||
#else
|
||||
int main()
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
#endif
|
||||
|
|
@ -0,0 +1,10 @@
|
|||
CORE
|
||||
main.c
|
||||
--dump-c
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
--
|
||||
^warning: ignoring
|
||||
--
|
||||
This test should be run via chain.sh, which will try to recompile the dumped C
|
||||
code. Missing/incomplete typedef output would cause a failure.
|
||||
|
|
@ -558,6 +558,14 @@ std::string expr2ct::convert_rec(
|
|||
|
||||
c_qualifierst ret_qualifiers;
|
||||
ret_qualifiers.read(code_type.return_type());
|
||||
// _Noreturn should go with the return type
|
||||
if(new_qualifiers.is_noreturn)
|
||||
{
|
||||
ret_qualifiers.is_noreturn=true;
|
||||
new_qualifiers.is_noreturn=false;
|
||||
q=new_qualifiers.as_string();
|
||||
}
|
||||
|
||||
const typet &return_type=code_type.return_type();
|
||||
|
||||
// return type may be a function pointer or array
|
||||
|
|
@ -1833,10 +1841,12 @@ std::string expr2ct::convert_constant(
|
|||
|
||||
if(dest!="" && isdigit(dest[dest.size()-1]))
|
||||
{
|
||||
if(dest.find('.')==std::string::npos)
|
||||
dest+=".0";
|
||||
|
||||
// ANSI-C: double is default; float/long-double require annotation
|
||||
if(src.type()==float_type())
|
||||
dest+='f';
|
||||
else if(src.type()==double_type())
|
||||
dest+=""; // ANSI-C: double is default
|
||||
else if(src.type()==long_double_type())
|
||||
dest+='l';
|
||||
}
|
||||
|
|
@ -3522,7 +3532,11 @@ std::string expr2ct::convert_with_precedence(
|
|||
return convert_function(src, "isinf", precedence=16);
|
||||
|
||||
else if(src.id()==ID_bswap)
|
||||
return convert_function(src, "bswap", precedence=16);
|
||||
return convert_function(
|
||||
src,
|
||||
"__builtin_bswap"+
|
||||
integer2string(pointer_offset_bits(src.op0().type(), ns)),
|
||||
precedence=16);
|
||||
|
||||
else if(src.id()==ID_isnormal)
|
||||
return convert_function(src, "isnormal", precedence=16);
|
||||
|
|
|
|||
|
|
@ -146,7 +146,7 @@ int clobber_parse_optionst::doit()
|
|||
if(!out)
|
||||
throw std::string("failed to create file simulator.c");
|
||||
|
||||
dump_c(goto_functions, true, ns, out);
|
||||
dump_c(goto_functions, true, false, ns, out);
|
||||
|
||||
status() << "instrumentation complete; compile and execute simulator.c"
|
||||
<< eom;
|
||||
|
|
|
|||
|
|
@ -714,6 +714,7 @@ void compilet::convert_symbols(goto_functionst &dest)
|
|||
|
||||
if(s_it->second.type.id()==ID_code &&
|
||||
!s_it->second.is_macro &&
|
||||
!s_it->second.is_type &&
|
||||
s_it->second.value.id()!="compiled" &&
|
||||
s_it->second.value.is_not_nil())
|
||||
{
|
||||
|
|
|
|||
|
|
@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <cctype>
|
||||
|
||||
#include <util/config.h>
|
||||
#include <util/invariant.h>
|
||||
#include <util/prefix.h>
|
||||
#include <util/suffix.h>
|
||||
#include <util/find_symbols.h>
|
||||
|
|
@ -38,6 +39,7 @@ void dump_ct::operator()(std::ostream &os)
|
|||
std::stringstream func_decl_stream;
|
||||
std::stringstream compound_body_stream;
|
||||
std::stringstream global_var_stream;
|
||||
std::stringstream global_decl_stream;
|
||||
std::stringstream func_body_stream;
|
||||
local_static_declst local_static_decls;
|
||||
|
||||
|
|
@ -92,17 +94,20 @@ void dump_ct::operator()(std::ostream &os)
|
|||
symbolt &symbol=it->second;
|
||||
bool tag_added=false;
|
||||
|
||||
// TODO we could get rid of some of the ID_anonymous by looking up
|
||||
// the origin symbol types in typedef_types and adjusting any other
|
||||
// uses of ID_tag
|
||||
if((symbol.type.id()==ID_union || symbol.type.id()==ID_struct) &&
|
||||
symbol.type.get(ID_tag).empty())
|
||||
{
|
||||
assert(symbol.is_type);
|
||||
PRECONDITION(symbol.is_type);
|
||||
symbol.type.set(ID_tag, ID_anonymous);
|
||||
tag_added=true;
|
||||
}
|
||||
else if(symbol.type.id()==ID_c_enum &&
|
||||
symbol.type.find(ID_tag).get(ID_C_base_name).empty())
|
||||
{
|
||||
assert(symbol.is_type);
|
||||
PRECONDITION(symbol.is_type);
|
||||
symbol.type.add(ID_tag).set(ID_C_base_name, ID_anonymous);
|
||||
tag_added=true;
|
||||
}
|
||||
|
|
@ -141,14 +146,17 @@ void dump_ct::operator()(std::ostream &os)
|
|||
symbol.type.set(ID_tag, new_tag);
|
||||
}
|
||||
|
||||
// we don't want to dump in full all definitions
|
||||
if(!tag_added && ignore(symbol))
|
||||
// we don't want to dump in full all definitions; in particular
|
||||
// do not dump anonymous types that are defined in system headers
|
||||
if((!tag_added || symbol.is_type) && ignore(symbol))
|
||||
continue;
|
||||
|
||||
if(!symbols_sorted.insert(name_str).second)
|
||||
assert(false);
|
||||
bool inserted=symbols_sorted.insert(name_str).second;
|
||||
CHECK_RETURN(inserted);
|
||||
}
|
||||
|
||||
gather_global_typedefs();
|
||||
|
||||
// collect all declarations we might need, include local static variables
|
||||
bool skip_function_main=false;
|
||||
for(std::set<std::string>::const_iterator
|
||||
|
|
@ -167,13 +175,17 @@ void dump_ct::operator()(std::ostream &os)
|
|||
type_id==ID_incomplete_union ||
|
||||
type_id==ID_c_enum))
|
||||
{
|
||||
os << "// " << symbol.name << '\n';
|
||||
os << "// " << symbol.location << '\n';
|
||||
if(!ignore(symbol))
|
||||
{
|
||||
global_decl_stream << "// " << symbol.name << '\n';
|
||||
global_decl_stream << "// " << symbol.location << '\n';
|
||||
|
||||
if(type_id==ID_c_enum)
|
||||
convert_compound_enum(symbol.type, os);
|
||||
else
|
||||
os << type_to_string(symbol_typet(symbol.name)) << ";\n\n";
|
||||
if(type_id==ID_c_enum)
|
||||
convert_compound_enum(symbol.type, global_decl_stream);
|
||||
else
|
||||
global_decl_stream << type_to_string(symbol_typet(symbol.name))
|
||||
<< ";\n\n";
|
||||
}
|
||||
}
|
||||
else if(symbol.is_static_lifetime && symbol.type.id()!=ID_code)
|
||||
convert_global_variable(
|
||||
|
|
@ -201,7 +213,8 @@ void dump_ct::operator()(std::ostream &os)
|
|||
{
|
||||
const symbolt &symbol=ns.lookup(*it);
|
||||
|
||||
if(symbol.type.id()!=ID_code)
|
||||
if(symbol.type.id()!=ID_code ||
|
||||
symbol.is_type)
|
||||
continue;
|
||||
|
||||
convert_function_declaration(
|
||||
|
|
@ -230,6 +243,8 @@ void dump_ct::operator()(std::ostream &os)
|
|||
compound_body_stream);
|
||||
}
|
||||
|
||||
// Dump the code to the target stream;
|
||||
// the statements before to this point collect the code to dump!
|
||||
for(std::set<std::string>::const_iterator
|
||||
it=system_headers.begin();
|
||||
it!=system_headers.end();
|
||||
|
|
@ -261,6 +276,11 @@ void dump_ct::operator()(std::ostream &os)
|
|||
<< "#endif\n\n";
|
||||
}
|
||||
|
||||
if(!global_decl_stream.str().empty())
|
||||
os << global_decl_stream.str() << '\n';
|
||||
|
||||
dump_typedefs(os);
|
||||
|
||||
if(!func_decl_stream.str().empty())
|
||||
os << func_decl_stream.str() << '\n';
|
||||
if(!compound_body_stream.str().empty())
|
||||
|
|
@ -295,7 +315,7 @@ void dump_ct::convert_compound(
|
|||
{
|
||||
const symbolt &symbol=
|
||||
ns.lookup(to_symbol_type(type).get_identifier());
|
||||
assert(symbol.is_type);
|
||||
DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol");
|
||||
|
||||
if(!ignore(symbol))
|
||||
convert_compound(symbol.type, unresolved, recursive, os);
|
||||
|
|
@ -304,7 +324,7 @@ void dump_ct::convert_compound(
|
|||
{
|
||||
const symbolt &symbol=
|
||||
ns.lookup(to_c_enum_tag_type(type).get_identifier());
|
||||
assert(symbol.is_type);
|
||||
DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol");
|
||||
|
||||
if(!ignore(symbol))
|
||||
convert_compound(symbol.type, unresolved, recursive, os);
|
||||
|
|
@ -349,11 +369,14 @@ void dump_ct::convert_compound(
|
|||
if(!converted_compound.insert(name).second)
|
||||
return;
|
||||
|
||||
// make sure typedef names used in the declaration are available
|
||||
collect_typedefs(type, true);
|
||||
|
||||
const irept &bases = type.find(ID_bases);
|
||||
std::stringstream base_decls;
|
||||
forall_irep(parent_it, bases.get_sub())
|
||||
{
|
||||
assert(false);
|
||||
UNREACHABLE;
|
||||
/*
|
||||
assert(parent_it->id() == ID_base);
|
||||
assert(parent_it->get(ID_type) == ID_symbol);
|
||||
|
|
@ -407,8 +430,13 @@ void dump_ct::convert_compound(
|
|||
while(non_array_type->id()==ID_array)
|
||||
non_array_type=&(ns.follow(non_array_type->subtype()));
|
||||
|
||||
if(recursive && non_array_type->id()!=ID_pointer)
|
||||
convert_compound(comp.type(), comp.type(), recursive, os);
|
||||
if(recursive)
|
||||
{
|
||||
if(non_array_type->id()!=ID_pointer)
|
||||
convert_compound(comp.type(), comp.type(), recursive, os);
|
||||
else
|
||||
collect_typedefs(comp.type(), true);
|
||||
}
|
||||
|
||||
irep_idt comp_name=comp.get_name();
|
||||
|
||||
|
|
@ -419,7 +447,7 @@ void dump_ct::convert_compound(
|
|||
// namespace
|
||||
std::string fake_unique_name="NO/SUCH/NS::"+id2string(comp_name);
|
||||
std::string s=make_decl(fake_unique_name, comp.type());
|
||||
assert(s.find("NO/SUCH/NS")==std::string::npos);
|
||||
POSTCONDITION(s.find("NO/SUCH/NS")==std::string::npos);
|
||||
|
||||
if(comp_type.id()==ID_c_bit_field &&
|
||||
to_c_bit_field_type(comp_type).get_width()==0)
|
||||
|
|
@ -457,15 +485,31 @@ void dump_ct::convert_compound(
|
|||
struct_body << s;
|
||||
}
|
||||
else
|
||||
assert(false);
|
||||
UNREACHABLE;
|
||||
|
||||
struct_body << ";\n";
|
||||
}
|
||||
|
||||
os << type_to_string(unresolved);
|
||||
typet unresolved_clean=unresolved;
|
||||
typedef_typest::const_iterator td_entry=
|
||||
typedef_types.find(unresolved);
|
||||
irep_idt typedef_str;
|
||||
if(td_entry!=typedef_types.end())
|
||||
{
|
||||
unresolved_clean.remove(ID_C_typedef);
|
||||
typedef_str=td_entry->second;
|
||||
std::pair<typedef_mapt::iterator, bool> td_map_entry=
|
||||
typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
|
||||
PRECONDITION(!td_map_entry.second);
|
||||
if(!td_map_entry.first->second.early)
|
||||
td_map_entry.first->second.type_decl_str="";
|
||||
os << "typedef ";
|
||||
}
|
||||
|
||||
os << type_to_string(unresolved_clean);
|
||||
if(!base_decls.str().empty())
|
||||
{
|
||||
assert(language->id()=="cpp");
|
||||
PRECONDITION(language->id()=="cpp");
|
||||
os << ": " << base_decls.str();
|
||||
}
|
||||
os << '\n';
|
||||
|
|
@ -489,14 +533,16 @@ void dump_ct::convert_compound(
|
|||
os << " __attribute__ ((__transparent_union__))";
|
||||
if(type.get_bool(ID_C_packed))
|
||||
os << " __attribute__ ((__packed__))";
|
||||
os << ";\n";
|
||||
if(!typedef_str.empty())
|
||||
os << " " << typedef_str;
|
||||
os << ";\n\n";
|
||||
}
|
||||
|
||||
void dump_ct::convert_compound_enum(
|
||||
const typet &type,
|
||||
std::ostream &os)
|
||||
{
|
||||
assert(type.id()==ID_c_enum);
|
||||
PRECONDITION(type.id()==ID_c_enum);
|
||||
|
||||
const irept &tag=type.find(ID_tag);
|
||||
const irep_idt &name=tag.get(ID_C_base_name);
|
||||
|
|
@ -597,7 +643,10 @@ void dump_ct::init_system_library_map()
|
|||
"pthread_rwlock_unlock", "pthread_rwlock_wrlock",
|
||||
"pthread_rwlockattr_destroy", "pthread_rwlockattr_getpshared",
|
||||
"pthread_rwlockattr_init", "pthread_rwlockattr_setpshared",
|
||||
"pthread_self", "pthread_setspecific"
|
||||
"pthread_self", "pthread_setspecific",
|
||||
/* non-public struct types */
|
||||
"tag-__pthread_internal_list", "tag-__pthread_mutex_s",
|
||||
"pthread_mutex_t"
|
||||
};
|
||||
ADD_TO_SYSTEM_LIBRARY(pthread_syms, "pthread.h");
|
||||
|
||||
|
|
@ -622,7 +671,7 @@ void dump_ct::init_system_library_map()
|
|||
"mkstemp", "mktemp", "perror", "printf", "putc", "putchar",
|
||||
"puts", "putw", "putwc", "putwchar", "remove", "rewind", "scanf",
|
||||
"setbuf", "setbuffer", "setlinebuf", "setvbuf", "snprintf",
|
||||
"sprintf", "sscanf", "strerror", "swprintf", "sys_errlist",
|
||||
"sprintf", "sscanf", "swprintf", "sys_errlist",
|
||||
"sys_nerr", "tempnam", "tmpfile", "tmpnam", "ungetc", "ungetwc",
|
||||
"vasprintf", "vfprintf", "vfscanf", "vfwprintf", "vprintf",
|
||||
"vscanf", "vsnprintf", "vsprintf", "vsscanf", "vswprintf",
|
||||
|
|
@ -658,9 +707,9 @@ void dump_ct::init_system_library_map()
|
|||
const char* time_syms[]=
|
||||
{
|
||||
"asctime", "asctime_r", "ctime", "ctime_r", "difftime", "gmtime",
|
||||
"gmtime_r", "localtime", "localtime_r", "mktime",
|
||||
"gmtime_r", "localtime", "localtime_r", "mktime", "strftime",
|
||||
/* non-public struct types */
|
||||
"tag-timespec", "tag-timeval"
|
||||
"tag-timespec", "tag-timeval", "tag-tm"
|
||||
};
|
||||
ADD_TO_SYSTEM_LIBRARY(time_syms, "time.h");
|
||||
|
||||
|
|
@ -681,21 +730,27 @@ void dump_ct::init_system_library_map()
|
|||
// sys/select.h
|
||||
const char* sys_select_syms[]=
|
||||
{
|
||||
"select"
|
||||
"select",
|
||||
/* non-public struct types */
|
||||
"fd_set"
|
||||
};
|
||||
ADD_TO_SYSTEM_LIBRARY(sys_select_syms, "sys/select.h");
|
||||
|
||||
// sys/socket.h
|
||||
const char* sys_socket_syms[]=
|
||||
{
|
||||
"accept", "bind", "connect"
|
||||
"accept", "bind", "connect",
|
||||
/* non-public struct types */
|
||||
"tag-sockaddr"
|
||||
};
|
||||
ADD_TO_SYSTEM_LIBRARY(sys_socket_syms, "sys/socket.h");
|
||||
|
||||
// sys/stat.h
|
||||
const char* sys_stat_syms[]=
|
||||
{
|
||||
"fstat", "lstat", "stat"
|
||||
"fstat", "lstat", "stat",
|
||||
/* non-public struct types */
|
||||
"tag-stat"
|
||||
};
|
||||
ADD_TO_SYSTEM_LIBRARY(sys_stat_syms, "sys/stat.h");
|
||||
|
||||
|
|
@ -715,6 +770,38 @@ void dump_ct::init_system_library_map()
|
|||
ADD_TO_SYSTEM_LIBRARY(sys_wait_syms, "sys/wait.h");
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: dump_ct::ignore
|
||||
|
||||
Inputs: type input to check whether it should not be dumped
|
||||
|
||||
Outputs: true, iff the type should not be printed
|
||||
|
||||
Purpose: Ignore selected types as they are covered via system headers
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
bool dump_ct::ignore(const typet &type)
|
||||
{
|
||||
symbolt symbol;
|
||||
symbol.type=type;
|
||||
|
||||
return ignore(symbol);
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: dump_ct::ignore
|
||||
|
||||
Inputs: type input to check whether it should not be dumped
|
||||
|
||||
Outputs: true, iff the symbol should not be printed
|
||||
|
||||
Purpose: Ignore selected symbols as they are covered via system headers
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
bool dump_ct::ignore(const symbolt &symbol)
|
||||
{
|
||||
const std::string &name_str=id2string(symbol.name);
|
||||
|
|
@ -729,15 +816,13 @@ bool dump_ct::ignore(const symbolt &symbol)
|
|||
name_str=="envp_size'")
|
||||
return true;
|
||||
|
||||
if(has_suffix(name_str, "$object"))
|
||||
return true;
|
||||
|
||||
const std::string &file_str=id2string(symbol.location.get_file());
|
||||
|
||||
// don't dump internal GCC builtins
|
||||
if((file_str=="gcc_builtin_headers_alpha.h" ||
|
||||
file_str=="gcc_builtin_headers_arm.h" ||
|
||||
file_str=="gcc_builtin_headers_ia32.h" ||
|
||||
file_str=="gcc_builtin_headers_mips.h" ||
|
||||
file_str=="gcc_builtin_headers_power.h" ||
|
||||
file_str=="gcc_builtin_headers_generic.h") &&
|
||||
if(has_prefix(file_str, "gcc_builtin_headers_") &&
|
||||
has_prefix(name_str, "__builtin_"))
|
||||
return true;
|
||||
|
||||
|
|
@ -749,9 +834,6 @@ bool dump_ct::ignore(const symbolt &symbol)
|
|||
return true;
|
||||
}
|
||||
|
||||
if(name_str.find("$link")!=std::string::npos)
|
||||
return false;
|
||||
|
||||
system_library_mapt::const_iterator it=
|
||||
system_library_map.find(symbol.name);
|
||||
|
||||
|
|
@ -761,6 +843,19 @@ bool dump_ct::ignore(const symbolt &symbol)
|
|||
return true;
|
||||
}
|
||||
|
||||
if(use_all_headers &&
|
||||
has_prefix(file_str, "/usr/include/"))
|
||||
{
|
||||
if(file_str.find("/bits/")==std::string::npos)
|
||||
{
|
||||
// Do not include transitive includes of system headers!
|
||||
std::string::size_type prefix_len=std::string("/usr/include/").size();
|
||||
system_headers.insert(file_str.substr(prefix_len));
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
@ -789,6 +884,10 @@ void dump_ct::cleanup_decl(
|
|||
|
||||
tmp.add_instruction(END_FUNCTION);
|
||||
|
||||
std::unordered_set<irep_idt, irep_id_hash> typedef_names;
|
||||
for(const auto &td : typedef_map)
|
||||
typedef_names.insert(td.first);
|
||||
|
||||
code_blockt b;
|
||||
goto_program2codet p2s(
|
||||
irep_idt(),
|
||||
|
|
@ -797,13 +896,268 @@ void dump_ct::cleanup_decl(
|
|||
b,
|
||||
local_static,
|
||||
local_type_decls,
|
||||
typedef_names,
|
||||
system_headers);
|
||||
p2s();
|
||||
|
||||
assert(b.operands().size()==1);
|
||||
POSTCONDITION(b.operands().size()==1);
|
||||
decl.swap(b.op0());
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: dump_ct::collect_typedefs
|
||||
|
||||
Inputs:
|
||||
type Type to inspect for ID_C_typedef entry
|
||||
early Set to true to enforce that typedef is dumped before any
|
||||
function declarations or struct definitions
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose: Find any typedef names contained in the input type and store
|
||||
their declaration strings in typedef_map for eventual output.
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
void dump_ct::collect_typedefs(const typet &type, bool early)
|
||||
{
|
||||
std::unordered_set<irep_idt, irep_id_hash> deps;
|
||||
collect_typedefs_rec(type, early, deps);
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: dump_ct::collect_typedefs_rec
|
||||
|
||||
Inputs:
|
||||
type Type to inspect for ID_C_typedef entry
|
||||
early Set to true to enforce that typedef is dumped before any
|
||||
function declarations or struct definitions
|
||||
dependencies Typedefs used in the declaration of a given typedef
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose: Find any typedef names contained in the input type and store
|
||||
their declaration strings in typedef_map for eventual output.
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
void dump_ct::collect_typedefs_rec(
|
||||
const typet &type,
|
||||
bool early,
|
||||
std::unordered_set<irep_idt, irep_id_hash> &dependencies)
|
||||
{
|
||||
if(ignore(type))
|
||||
return;
|
||||
|
||||
std::unordered_set<irep_idt, irep_id_hash> local_deps;
|
||||
|
||||
if(type.id()==ID_code)
|
||||
{
|
||||
const code_typet &code_type=to_code_type(type);
|
||||
|
||||
collect_typedefs_rec(code_type.return_type(), early, local_deps);
|
||||
for(const auto ¶m : code_type.parameters())
|
||||
collect_typedefs_rec(param.type(), early, local_deps);
|
||||
}
|
||||
else if(type.id()==ID_pointer || type.id()==ID_array)
|
||||
{
|
||||
collect_typedefs_rec(type.subtype(), early, local_deps);
|
||||
}
|
||||
else if(type.id()==ID_symbol)
|
||||
{
|
||||
const symbolt &symbol=
|
||||
ns.lookup(to_symbol_type(type).get_identifier());
|
||||
collect_typedefs_rec(symbol.type, early, local_deps);
|
||||
}
|
||||
|
||||
const irep_idt &typedef_str=type.get(ID_C_typedef);
|
||||
|
||||
if(!typedef_str.empty())
|
||||
{
|
||||
std::pair<typedef_mapt::iterator, bool> entry=
|
||||
typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
|
||||
|
||||
if(entry.second ||
|
||||
(early && entry.first->second.type_decl_str.empty()))
|
||||
{
|
||||
if(typedef_str=="__gnuc_va_list" || typedef_str == "va_list")
|
||||
{
|
||||
system_headers.insert("stdarg.h");
|
||||
early=false;
|
||||
}
|
||||
else
|
||||
{
|
||||
typet t=type;
|
||||
t.remove(ID_C_typedef);
|
||||
|
||||
std::ostringstream oss;
|
||||
oss << "typedef " << make_decl(typedef_str, t) << ';';
|
||||
|
||||
entry.first->second.type_decl_str=oss.str();
|
||||
entry.first->second.dependencies=local_deps;
|
||||
}
|
||||
}
|
||||
|
||||
if(early)
|
||||
{
|
||||
entry.first->second.early=true;
|
||||
|
||||
for(const auto &d : local_deps)
|
||||
{
|
||||
auto td_entry=typedef_map.find(d);
|
||||
PRECONDITION(td_entry!=typedef_map.end());
|
||||
td_entry->second.early=true;
|
||||
}
|
||||
}
|
||||
|
||||
dependencies.insert(typedef_str);
|
||||
}
|
||||
|
||||
dependencies.insert(local_deps.begin(), local_deps.end());
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: dump_ct::gather_global_typedefs
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose: find all global typdefs in the symbol table and store them
|
||||
in typedef_types
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
void dump_ct::gather_global_typedefs()
|
||||
{
|
||||
// sort the symbols first to ensure deterministic replacement in
|
||||
// typedef_types below as there could be redundant declarations
|
||||
// typedef int x;
|
||||
// typedef int y;
|
||||
std::map<std::string, symbolt> symbols_sorted;
|
||||
for(const auto &symbol_entry : copied_symbol_table.symbols)
|
||||
symbols_sorted.insert(
|
||||
{id2string(symbol_entry.first), symbol_entry.second});
|
||||
|
||||
for(const auto &symbol_entry : symbols_sorted)
|
||||
{
|
||||
const symbolt &symbol=symbol_entry.second;
|
||||
|
||||
if(symbol.is_macro && symbol.is_type &&
|
||||
symbol.location.get_function().empty())
|
||||
{
|
||||
const irep_idt &typedef_str=symbol.type.get(ID_C_typedef);
|
||||
PRECONDITION(!typedef_str.empty());
|
||||
typedef_types[symbol.type]=typedef_str;
|
||||
if(ignore(symbol))
|
||||
typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
|
||||
else
|
||||
collect_typedefs(symbol.type, false);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: dump_ct::dump_typedefs
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs: os output stream
|
||||
|
||||
Purpose: print all typedefs that are not covered via
|
||||
typedef struct xyz { ... } name;
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
void dump_ct::dump_typedefs(std::ostream &os) const
|
||||
{
|
||||
// we need to compute a topological sort; we do so by picking all
|
||||
// typedefs the dependencies of which have been emitted into to_insert
|
||||
std::vector<typedef_infot> typedefs_sorted;
|
||||
typedefs_sorted.reserve(typedef_map.size());
|
||||
|
||||
// elements in to_insert are lexicographically sorted and ready for
|
||||
// output
|
||||
std::map<std::string, typedef_infot> to_insert;
|
||||
|
||||
typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
|
||||
id_sett typedefs_done;
|
||||
std::unordered_map<irep_idt, id_sett, irep_id_hash>
|
||||
forward_deps, reverse_deps;
|
||||
|
||||
for(const auto &td : typedef_map)
|
||||
if(!td.second.type_decl_str.empty())
|
||||
{
|
||||
if(td.second.dependencies.empty())
|
||||
// those can be dumped immediately
|
||||
to_insert.insert({id2string(td.first), td.second});
|
||||
else
|
||||
{
|
||||
// delay them until dependencies are dumped
|
||||
forward_deps.insert({td.first, td.second.dependencies});
|
||||
for(const auto &d : td.second.dependencies)
|
||||
reverse_deps[d].insert(td.first);
|
||||
}
|
||||
}
|
||||
|
||||
while(!to_insert.empty())
|
||||
{
|
||||
// the topologically next element (lexicographically ranked first
|
||||
// among all the dependencies of which have been dumped)
|
||||
typedef_infot t=to_insert.begin()->second;
|
||||
to_insert.erase(to_insert.begin());
|
||||
// move to the output queue
|
||||
typedefs_sorted.push_back(t);
|
||||
|
||||
// find any depending typedefs that are now valid, or at least
|
||||
// reduce the remaining dependencies
|
||||
auto r_it=reverse_deps.find(t.typedef_name);
|
||||
if(r_it==reverse_deps.end())
|
||||
continue;
|
||||
|
||||
// reduce remaining dependencies
|
||||
id_sett &r_deps=r_it->second;
|
||||
for(id_sett::iterator it=r_deps.begin(); it!=r_deps.end(); ) // no ++it
|
||||
{
|
||||
auto f_it=forward_deps.find(*it);
|
||||
if(f_it==forward_deps.end()) // might be done already
|
||||
{
|
||||
it=r_deps.erase(it);
|
||||
continue;
|
||||
}
|
||||
|
||||
// update dependencies
|
||||
id_sett &f_deps=f_it->second;
|
||||
PRECONDITION(!f_deps.empty());
|
||||
PRECONDITION(f_deps.find(t.typedef_name)!=f_deps.end());
|
||||
f_deps.erase(t.typedef_name);
|
||||
|
||||
if(f_deps.empty()) // all depenencies done now!
|
||||
{
|
||||
const auto td_entry=typedef_map.find(*it);
|
||||
PRECONDITION(td_entry!=typedef_map.end());
|
||||
to_insert.insert({id2string(*it), td_entry->second});
|
||||
forward_deps.erase(*it);
|
||||
it=r_deps.erase(it);
|
||||
}
|
||||
else
|
||||
++it;
|
||||
}
|
||||
}
|
||||
|
||||
POSTCONDITION(forward_deps.empty());
|
||||
|
||||
for(const auto &td : typedefs_sorted)
|
||||
os << td.type_decl_str << '\n';
|
||||
|
||||
if(!typedefs_sorted.empty())
|
||||
os << '\n';
|
||||
}
|
||||
|
||||
void dump_ct::convert_global_variable(
|
||||
const symbolt &symbol,
|
||||
std::ostream &os,
|
||||
|
|
@ -837,8 +1191,10 @@ void dump_ct::convert_global_variable(
|
|||
it=syms.begin();
|
||||
it!=syms.end();
|
||||
++it)
|
||||
if(!symbols_sorted.insert(id2string(*it)).second)
|
||||
assert(false);
|
||||
{
|
||||
bool inserted=symbols_sorted.insert(id2string(*it)).second;
|
||||
CHECK_RETURN(inserted);
|
||||
}
|
||||
|
||||
for(std::set<std::string>::const_iterator
|
||||
it=symbols_sorted.begin();
|
||||
|
|
@ -862,7 +1218,7 @@ void dump_ct::convert_global_variable(
|
|||
|
||||
std::list<irep_idt> empty_static, empty_types;
|
||||
cleanup_decl(d, empty_static, empty_types);
|
||||
assert(empty_static.empty());
|
||||
CHECK_RETURN(empty_static.empty());
|
||||
os << expr_to_string(d) << '\n';
|
||||
}
|
||||
}
|
||||
|
|
@ -888,6 +1244,10 @@ void dump_ct::convert_function_declaration(
|
|||
code_blockt b;
|
||||
std::list<irep_idt> type_decls, local_static;
|
||||
|
||||
std::unordered_set<irep_idt, irep_id_hash> typedef_names;
|
||||
for(const auto &td : typedef_map)
|
||||
typedef_names.insert(td.first);
|
||||
|
||||
goto_program2codet p2s(
|
||||
symbol.name,
|
||||
func_entry->second.body,
|
||||
|
|
@ -895,6 +1255,7 @@ void dump_ct::convert_function_declaration(
|
|||
b,
|
||||
local_static,
|
||||
type_decls,
|
||||
typedef_names,
|
||||
system_headers);
|
||||
p2s();
|
||||
|
||||
|
|
@ -933,6 +1294,10 @@ void dump_ct::convert_function_declaration(
|
|||
os_decl << "// " << symbol.location << '\n';
|
||||
os_decl << make_decl(symbol.name, symbol.type) << ";\n";
|
||||
}
|
||||
|
||||
// make sure typedef names used in the function declaration are
|
||||
// available
|
||||
collect_typedefs(symbol.type, true);
|
||||
}
|
||||
|
||||
static bool find_block_position_rec(
|
||||
|
|
@ -1029,7 +1394,7 @@ void dump_ct::insert_local_static_decls(
|
|||
{
|
||||
local_static_declst::const_iterator d_it=
|
||||
local_static_decls.find(*it);
|
||||
assert(d_it!=local_static_decls.end());
|
||||
PRECONDITION(d_it!=local_static_decls.end());
|
||||
|
||||
code_declt d=d_it->second;
|
||||
std::list<irep_idt> redundant;
|
||||
|
|
@ -1042,7 +1407,7 @@ void dump_ct::insert_local_static_decls(
|
|||
// within an if(false) { ... } block
|
||||
if(find_block_position_rec(*it, b, dest_ptr, before))
|
||||
{
|
||||
assert(dest_ptr!=0);
|
||||
CHECK_RETURN(dest_ptr!=0);
|
||||
dest_ptr->operands().insert(before, d);
|
||||
}
|
||||
}
|
||||
|
|
@ -1079,7 +1444,7 @@ void dump_ct::insert_local_type_decls(
|
|||
// has been removed by cleanup operations
|
||||
if(find_block_position_rec(*it, b, dest_ptr, before))
|
||||
{
|
||||
assert(dest_ptr!=0);
|
||||
CHECK_RETURN(dest_ptr!=0);
|
||||
dest_ptr->operands().insert(before, skip);
|
||||
}
|
||||
}
|
||||
|
|
@ -1103,7 +1468,7 @@ void dump_ct::cleanup_expr(exprt &expr)
|
|||
exprt::operandst old_ops;
|
||||
old_ops.swap(expr.operands());
|
||||
|
||||
assert(old_components.size()==old_ops.size());
|
||||
PRECONDITION(old_components.size()==old_ops.size());
|
||||
exprt::operandst::iterator o_it=old_ops.begin();
|
||||
for(struct_union_typet::componentst::const_iterator
|
||||
it=old_components.begin();
|
||||
|
|
@ -1145,7 +1510,7 @@ void dump_ct::cleanup_expr(exprt &expr)
|
|||
const struct_union_typet::componentt &comp=
|
||||
u_type_f.get_component(u.get_component_name());
|
||||
const typet &u_op_type=comp.type();
|
||||
assert(u_op_type.id()==ID_pointer);
|
||||
PRECONDITION(u_op_type.id()==ID_pointer);
|
||||
|
||||
typecast_exprt tc(u.op(), u_op_type);
|
||||
expr.swap(tc);
|
||||
|
|
@ -1253,8 +1618,9 @@ void dump_ct::cleanup_type(typet &type)
|
|||
if(type.id()==ID_array)
|
||||
cleanup_expr(to_array_type(type).size());
|
||||
|
||||
assert((type.id()!=ID_union && type.id()!=ID_struct) ||
|
||||
!type.get(ID_tag).empty());
|
||||
POSTCONDITION(
|
||||
(type.id()!=ID_union && type.id()!=ID_struct) ||
|
||||
!type.get(ID_tag).empty());
|
||||
}
|
||||
|
||||
std::string dump_ct::type_to_string(const typet &type)
|
||||
|
|
@ -1278,19 +1644,23 @@ std::string dump_ct::expr_to_string(const exprt &expr)
|
|||
void dump_c(
|
||||
const goto_functionst &src,
|
||||
const bool use_system_headers,
|
||||
const bool use_all_headers,
|
||||
const namespacet &ns,
|
||||
std::ostream &out)
|
||||
{
|
||||
dump_ct goto2c(src, use_system_headers, ns, new_ansi_c_language);
|
||||
dump_ct goto2c(
|
||||
src, use_system_headers, use_all_headers, ns, new_ansi_c_language);
|
||||
out << goto2c;
|
||||
}
|
||||
|
||||
void dump_cpp(
|
||||
const goto_functionst &src,
|
||||
const bool use_system_headers,
|
||||
const bool use_all_headers,
|
||||
const namespacet &ns,
|
||||
std::ostream &out)
|
||||
{
|
||||
dump_ct goto2cpp(src, use_system_headers, ns, new_cpp_language);
|
||||
dump_ct goto2cpp(
|
||||
src, use_system_headers, use_all_headers, ns, new_cpp_language);
|
||||
out << goto2cpp;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -17,12 +17,14 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
void dump_c(
|
||||
const goto_functionst &src,
|
||||
const bool use_system_headers,
|
||||
const bool use_all_headers,
|
||||
const namespacet &ns,
|
||||
std::ostream &out);
|
||||
|
||||
void dump_cpp(
|
||||
const goto_functionst &src,
|
||||
const bool use_system_headers,
|
||||
const bool use_all_headers,
|
||||
const namespacet &ns,
|
||||
std::ostream &out);
|
||||
|
||||
|
|
|
|||
|
|
@ -25,12 +25,14 @@ public:
|
|||
dump_ct(
|
||||
const goto_functionst &_goto_functions,
|
||||
const bool use_system_headers,
|
||||
const bool use_all_headers,
|
||||
const namespacet &_ns,
|
||||
language_factoryt factory):
|
||||
goto_functions(_goto_functions),
|
||||
copied_symbol_table(_ns.get_symbol_table()),
|
||||
ns(copied_symbol_table),
|
||||
language(factory())
|
||||
language(factory()),
|
||||
use_all_headers(use_all_headers)
|
||||
{
|
||||
if(use_system_headers)
|
||||
init_system_library_map();
|
||||
|
|
@ -48,6 +50,7 @@ protected:
|
|||
symbol_tablet copied_symbol_table;
|
||||
const namespacet ns;
|
||||
languaget *language;
|
||||
const bool use_all_headers;
|
||||
|
||||
typedef std::unordered_set<irep_idt, irep_id_hash> convertedt;
|
||||
convertedt converted_compound, converted_global, converted_enum;
|
||||
|
|
@ -62,12 +65,32 @@ protected:
|
|||
declared_enum_constants_mapt;
|
||||
declared_enum_constants_mapt declared_enum_constants;
|
||||
|
||||
struct typedef_infot
|
||||
{
|
||||
irep_idt typedef_name;
|
||||
std::string type_decl_str;
|
||||
bool early;
|
||||
std::unordered_set<irep_idt, irep_id_hash> dependencies;
|
||||
|
||||
explicit typedef_infot(const irep_idt &name):
|
||||
typedef_name(name),
|
||||
type_decl_str(""),
|
||||
early(false)
|
||||
{
|
||||
}
|
||||
};
|
||||
typedef std::map<irep_idt, typedef_infot> typedef_mapt;
|
||||
typedef_mapt typedef_map;
|
||||
typedef std::unordered_map<typet, irep_idt, irep_hash> typedef_typest;
|
||||
typedef_typest typedef_types;
|
||||
|
||||
void init_system_library_map();
|
||||
|
||||
std::string type_to_string(const typet &type);
|
||||
std::string expr_to_string(const exprt &expr);
|
||||
|
||||
bool ignore(const symbolt &symbol);
|
||||
bool ignore(const typet &type);
|
||||
|
||||
static std::string indent(const unsigned n)
|
||||
{
|
||||
|
|
@ -88,6 +111,14 @@ protected:
|
|||
return d_str.substr(0, d_str.size()-1);
|
||||
}
|
||||
|
||||
void collect_typedefs(const typet &type, bool early);
|
||||
void collect_typedefs_rec(
|
||||
const typet &type,
|
||||
bool early,
|
||||
std::unordered_set<irep_idt, irep_id_hash> &dependencies);
|
||||
void gather_global_typedefs();
|
||||
void dump_typedefs(std::ostream &os) const;
|
||||
|
||||
void convert_compound_declaration(
|
||||
const symbolt &symbol,
|
||||
std::ostream &os_body);
|
||||
|
|
|
|||
|
|
@ -621,7 +621,8 @@ int goto_instrument_parse_optionst::doit()
|
|||
if(cmdline.isset("dump-c") || cmdline.isset("dump-cpp"))
|
||||
{
|
||||
const bool is_cpp=cmdline.isset("dump-cpp");
|
||||
const bool h=cmdline.isset("use-system-headers");
|
||||
const bool h_libc=!cmdline.isset("no-system-headers");
|
||||
const bool h_all=cmdline.isset("use-all-headers");
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
// restore RETURN instructions in case remove_returns had been
|
||||
|
|
@ -640,10 +641,11 @@ int goto_instrument_parse_optionst::doit()
|
|||
error() << "failed to write to `" << cmdline.args[1] << "'";
|
||||
return 10;
|
||||
}
|
||||
(is_cpp ? dump_cpp : dump_c)(goto_functions, h, ns, out);
|
||||
(is_cpp ? dump_cpp : dump_c)(goto_functions, h_libc, h_all, ns, out);
|
||||
}
|
||||
else
|
||||
(is_cpp ? dump_cpp : dump_c)(goto_functions, h, ns, std::cout);
|
||||
(is_cpp ? dump_cpp : dump_c)(
|
||||
goto_functions, h_libc, h_all, ns, std::cout);
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -1540,7 +1542,8 @@ void goto_instrument_parse_optionst::help()
|
|||
" --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
|
||||
"\n"
|
||||
"Other options:\n"
|
||||
" --use-system-headers with --dump-c/--dump-cpp: generate C source with includes\n" // NOLINT(*)
|
||||
" --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
|
||||
" --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
|
||||
" --version show version and exit\n"
|
||||
" --xml-ui use XML-formatted output\n"
|
||||
" --json-ui use JSON-formatted output\n"
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
"(all)" \
|
||||
"(document-claims-latex)(document-claims-html)" \
|
||||
"(document-properties-latex)(document-properties-html)" \
|
||||
"(dump-c)(dump-cpp)(use-system-headers)(dot)(xml)" \
|
||||
"(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \
|
||||
OPT_GOTO_CHECK \
|
||||
/* no-X-check are deprecated and ignored */ \
|
||||
"(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
|
||||
|
|
|
|||
|
|
@ -110,14 +110,23 @@ void goto_program2codet::scan_for_varargs()
|
|||
forall_goto_program_instructions(target, goto_program)
|
||||
if(target->is_assign())
|
||||
{
|
||||
const exprt &l=to_code_assign(target->code).lhs();
|
||||
const exprt &r=to_code_assign(target->code).rhs();
|
||||
|
||||
// find va_arg_next
|
||||
if(r.id()==ID_side_effect &&
|
||||
to_side_effect_expr(r).get_statement()==ID_gcc_builtin_va_arg_next)
|
||||
{
|
||||
assert(r.has_operands());
|
||||
va_list_expr.insert(r.op0());
|
||||
}
|
||||
// try our modelling of va_start
|
||||
else if(l.type().id()==ID_pointer &&
|
||||
l.type().get(ID_C_typedef)=="va_list" &&
|
||||
l.id()==ID_symbol &&
|
||||
r.id()==ID_typecast &&
|
||||
to_typecast_expr(r).op().id()==ID_address_of)
|
||||
va_list_expr.insert(l);
|
||||
}
|
||||
|
||||
if(!va_list_expr.empty())
|
||||
|
|
@ -556,7 +565,7 @@ goto_programt::const_targett goto_program2codet::convert_goto(
|
|||
else if(!target->guard.is_true())
|
||||
return convert_goto_switch(target, upper_bound, dest);
|
||||
else if(!loop_last_stack.empty())
|
||||
return convert_goto_break_continue(target, dest);
|
||||
return convert_goto_break_continue(target, upper_bound, dest);
|
||||
else
|
||||
return convert_goto_goto(target, dest);
|
||||
}
|
||||
|
|
@ -794,7 +803,14 @@ bool goto_program2codet::set_block_end_points(
|
|||
|
||||
// ignore dead instructions for the following checks
|
||||
if(n.dominators.empty())
|
||||
{
|
||||
// simplification may have figured out that a case is unreachable
|
||||
// this is possibly getting too weird, abort to be safe
|
||||
if(case_end==it->case_start)
|
||||
return true;
|
||||
|
||||
continue;
|
||||
}
|
||||
|
||||
// find the last instruction dominated by the case start
|
||||
if(n.dominators.find(it->case_start)==n.dominators.end())
|
||||
|
|
@ -1098,7 +1114,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
|
|||
upper_bound->location_number < end_if->location_number))
|
||||
{
|
||||
if(!loop_last_stack.empty())
|
||||
return convert_goto_break_continue(target, dest);
|
||||
return convert_goto_break_continue(target, upper_bound, dest);
|
||||
else
|
||||
return convert_goto_goto(target, dest);
|
||||
}
|
||||
|
|
@ -1131,6 +1147,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
|
|||
|
||||
goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
|
||||
goto_programt::const_targett target,
|
||||
goto_programt::const_targett upper_bound,
|
||||
codet &dest)
|
||||
{
|
||||
assert(!loop_last_stack.empty());
|
||||
|
|
@ -1140,7 +1157,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
|
|||
// 1: ...
|
||||
goto_programt::const_targett next=target;
|
||||
for(++next;
|
||||
next!=goto_program.instructions.end();
|
||||
next!=upper_bound && next!=goto_program.instructions.end();
|
||||
++next)
|
||||
{
|
||||
cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
|
||||
|
|
@ -1496,6 +1513,11 @@ void goto_program2codet::cleanup_code(
|
|||
|
||||
add_local_types(code.op0().type());
|
||||
|
||||
const irep_idt &typedef_str=code.op0().type().get(ID_C_typedef);
|
||||
if(!typedef_str.empty() &&
|
||||
typedef_names.find(typedef_str)==typedef_names.end())
|
||||
code.op0().type().remove(ID_C_typedef);
|
||||
|
||||
return;
|
||||
}
|
||||
else if(code.get_statement()==ID_function_call)
|
||||
|
|
@ -1851,6 +1873,11 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
|
|||
|
||||
add_local_types(t);
|
||||
expr=typecast_exprt(expr, t);
|
||||
|
||||
const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
|
||||
if(!typedef_str.empty() &&
|
||||
typedef_names.find(typedef_str)==typedef_names.end())
|
||||
expr.type().remove(ID_C_typedef);
|
||||
}
|
||||
else if(expr.id()==ID_array ||
|
||||
expr.id()==ID_vector)
|
||||
|
|
@ -1863,6 +1890,11 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
|
|||
|
||||
expr.make_typecast(t);
|
||||
add_local_types(t);
|
||||
|
||||
const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
|
||||
if(!typedef_str.empty() &&
|
||||
typedef_names.find(typedef_str)==typedef_names.end())
|
||||
expr.type().remove(ID_C_typedef);
|
||||
}
|
||||
else if(expr.id()==ID_side_effect)
|
||||
{
|
||||
|
|
@ -1978,6 +2010,11 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
|
|||
{
|
||||
add_local_types(expr.type());
|
||||
|
||||
const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
|
||||
if(!typedef_str.empty() &&
|
||||
typedef_names.find(typedef_str)==typedef_names.end())
|
||||
expr.type().remove(ID_C_typedef);
|
||||
|
||||
assert(expr.type().id()!=ID_union &&
|
||||
expr.type().id()!=ID_struct);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -52,6 +52,7 @@ public:
|
|||
code_blockt &_dest,
|
||||
id_listt &_local_static,
|
||||
id_listt &_type_names,
|
||||
const id_sett &_typedef_names,
|
||||
std::set<std::string> &_system_headers):
|
||||
func_name(identifier),
|
||||
goto_program(_goto_program),
|
||||
|
|
@ -60,6 +61,7 @@ public:
|
|||
toplevel_block(_dest),
|
||||
local_static(_local_static),
|
||||
type_names(_type_names),
|
||||
typedef_names(_typedef_names),
|
||||
system_headers(_system_headers)
|
||||
{
|
||||
assert(local_static.empty());
|
||||
|
|
@ -81,6 +83,7 @@ protected:
|
|||
code_blockt &toplevel_block;
|
||||
id_listt &local_static;
|
||||
id_listt &type_names;
|
||||
const id_sett &typedef_names;
|
||||
std::set<std::string> &system_headers;
|
||||
std::unordered_set<exprt, irep_hash> va_list_expr;
|
||||
|
||||
|
|
@ -196,6 +199,7 @@ protected:
|
|||
|
||||
goto_programt::const_targett convert_goto_break_continue(
|
||||
goto_programt::const_targett target,
|
||||
goto_programt::const_targett upper_bound,
|
||||
codet &dest);
|
||||
|
||||
goto_programt::const_targett convert_goto_goto(
|
||||
|
|
|
|||
|
|
@ -302,7 +302,7 @@ static bool link_functions(
|
|||
rename_symbolt macro_application;
|
||||
|
||||
forall_symbols(it, dest_symbol_table.symbols)
|
||||
if(it->second.is_macro)
|
||||
if(it->second.is_macro && !it->second.is_type)
|
||||
{
|
||||
const symbolt &symbol=it->second;
|
||||
|
||||
|
|
|
|||
|
|
@ -124,6 +124,10 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
|
|||
|
||||
forall_subtypes(it, src)
|
||||
find_symbols(kind, *it, dest);
|
||||
|
||||
const irep_idt &typedef_name=src.get(ID_C_typedef);
|
||||
if(!typedef_name.empty())
|
||||
dest.insert(typedef_name);
|
||||
}
|
||||
|
||||
if(src.id()==ID_struct ||
|
||||
|
|
|
|||
Loading…
Reference in New Issue