commit
5f7ff9984a
|
@ -103,6 +103,10 @@ Here a few minimalistic coding rules for the CPROVER source tree.
|
|||
- Prefer forward declaration to includes, but forward declare at the top of the
|
||||
header file rather than in line
|
||||
- Guard headers with `#ifndef CPROVER_DIRECTORIES_FILE_H`, etc
|
||||
- The corresponding header for a given source file should always be the *first*
|
||||
include in the source file. For example, given `foo.h` and `foo.cpp`, the
|
||||
line `#include "foo.h"` should precede all other include statements in
|
||||
`foo.cpp`.
|
||||
|
||||
# Makefiles
|
||||
- Each source file should appear on a separate line
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Abstract Interpretation
|
||||
|
||||
#include "ai.h"
|
||||
|
||||
#include <cassert>
|
||||
#include <memory>
|
||||
#include <sstream>
|
||||
|
@ -19,8 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include "is_threaded.h"
|
||||
|
||||
#include "ai.h"
|
||||
|
||||
jsont ai_domain_baset::output_json(
|
||||
const ai_baset &ai,
|
||||
const namespacet &ns) const
|
||||
|
|
|
@ -9,11 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Function Call Graphs
|
||||
|
||||
#include "call_graph.h"
|
||||
|
||||
#include <util/std_expr.h>
|
||||
#include <util/xml.h>
|
||||
|
||||
#include "call_graph.h"
|
||||
|
||||
call_grapht::call_grapht()
|
||||
{
|
||||
}
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Peter Schrammel
|
|||
/// \file
|
||||
/// Constant Propagation
|
||||
|
||||
#include "constant_propagator.h"
|
||||
|
||||
#ifdef DEBUG
|
||||
#include <iostream>
|
||||
#endif
|
||||
|
@ -17,8 +19,6 @@ Author: Peter Schrammel
|
|||
#include <util/arith_tools.h>
|
||||
#include <util/simplify_expr.h>
|
||||
|
||||
#include "constant_propagator.h"
|
||||
|
||||
exprt concatenate_array_id(
|
||||
const exprt &array, const exprt &index,
|
||||
const typet &type)
|
||||
|
|
|
@ -9,11 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Field-insensitive, location-sensitive bitvector analysis
|
||||
|
||||
#include "custom_bitvector_analysis.h"
|
||||
|
||||
#include <util/xml_expr.h>
|
||||
#include <util/simplify_expr.h>
|
||||
|
||||
#include "custom_bitvector_analysis.h"
|
||||
|
||||
#include <iostream>
|
||||
|
||||
void custom_bitvector_domaint::set_bit(
|
||||
|
|
|
@ -12,6 +12,8 @@ Date: August 2013
|
|||
/// \file
|
||||
/// Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010
|
||||
|
||||
#include "dependence_graph.h"
|
||||
|
||||
#include <cassert>
|
||||
|
||||
#include <util/json.h>
|
||||
|
@ -19,8 +21,6 @@ Date: August 2013
|
|||
|
||||
#include "goto_rw.h"
|
||||
|
||||
#include "dependence_graph.h"
|
||||
|
||||
bool dep_graph_domaint::merge(
|
||||
const dep_graph_domaint &src,
|
||||
goto_programt::const_targett from,
|
||||
|
|
|
@ -11,10 +11,10 @@ Date: March 2013
|
|||
/// \file
|
||||
/// Local variables whose address is taken
|
||||
|
||||
#include <util/std_expr.h>
|
||||
|
||||
#include "dirty.h"
|
||||
|
||||
#include <util/std_expr.h>
|
||||
|
||||
void dirtyt::build(const goto_functiont &goto_function)
|
||||
{
|
||||
forall_goto_program_instructions(it, goto_function.body)
|
||||
|
|
|
@ -9,6 +9,8 @@
|
|||
/// \file
|
||||
/// Analyses
|
||||
|
||||
#include "does_remove_const.h"
|
||||
|
||||
#include <goto-programs/goto_program.h>
|
||||
#include <util/type.h>
|
||||
#include <util/expr.h>
|
||||
|
@ -16,8 +18,6 @@
|
|||
#include <util/base_type.h>
|
||||
#include <ansi-c/c_qualifiers.h>
|
||||
|
||||
#include "does_remove_const.h"
|
||||
|
||||
/// A naive analysis to look for casts that remove const-ness from pointers.
|
||||
/// \param goto_program: the goto program to check
|
||||
/// \param ns: the namespace of the goto program (used for checking type
|
||||
|
|
|
@ -14,6 +14,8 @@
|
|||
#include <util/type.h>
|
||||
|
||||
class goto_programt;
|
||||
class namespacet;
|
||||
class exprt;
|
||||
|
||||
class does_remove_constt
|
||||
{
|
||||
|
|
|
@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Field-insensitive, location-sensitive escape analysis
|
||||
|
||||
#include <util/simplify_expr.h>
|
||||
|
||||
#include "escape_analysis.h"
|
||||
|
||||
#include <util/simplify_expr.h>
|
||||
|
||||
bool escape_domaint::is_tracked(const symbol_exprt &symbol)
|
||||
{
|
||||
const irep_idt &identifier=symbol.get_identifier();
|
||||
|
|
|
@ -10,13 +10,13 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Flow Insensitive Static Analysis
|
||||
|
||||
#include "flow_insensitive_analysis.h"
|
||||
|
||||
#include <cassert>
|
||||
|
||||
#include <util/std_expr.h>
|
||||
#include <util/std_code.h>
|
||||
|
||||
#include "flow_insensitive_analysis.h"
|
||||
|
||||
exprt flow_insensitive_abstract_domain_baset::get_guard(
|
||||
locationt from,
|
||||
locationt to) const
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// GOTO Programs
|
||||
|
||||
#include "goto_check.h"
|
||||
|
||||
#include <algorithm>
|
||||
|
||||
#include <util/simplify_expr.h>
|
||||
|
@ -27,7 +29,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/options.h>
|
||||
|
||||
#include "local_bitvector_analysis.h"
|
||||
#include "goto_check.h"
|
||||
|
||||
class goto_checkt
|
||||
{
|
||||
|
|
|
@ -8,6 +8,7 @@ Date: April 2010
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "goto_rw.h"
|
||||
|
||||
#include <limits>
|
||||
#include <algorithm>
|
||||
|
@ -24,8 +25,6 @@ Date: April 2010
|
|||
|
||||
#include <pointer-analysis/goto_program_dereference.h>
|
||||
|
||||
#include "goto_rw.h"
|
||||
|
||||
range_domain_baset::~range_domain_baset()
|
||||
{
|
||||
}
|
||||
|
|
|
@ -9,10 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Interval Analysis
|
||||
|
||||
#include "interval_analysis.h"
|
||||
|
||||
#include <util/find_symbols.h>
|
||||
|
||||
#include "interval_domain.h"
|
||||
#include "interval_analysis.h"
|
||||
|
||||
void instrument_intervals(
|
||||
const ait<interval_domaint> &interval_analysis,
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Interval Domain
|
||||
|
||||
#include "interval_domain.h"
|
||||
|
||||
#ifdef DEBUG
|
||||
#include <iostream>
|
||||
#endif
|
||||
|
@ -17,8 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/std_expr.h>
|
||||
#include <util/arith_tools.h>
|
||||
|
||||
#include "interval_domain.h"
|
||||
|
||||
void interval_domaint::output(
|
||||
std::ostream &out,
|
||||
const ai_baset &ai,
|
||||
|
|
|
@ -9,13 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Invariant Propagation
|
||||
|
||||
#include "invariant_propagation.h"
|
||||
|
||||
#include <util/simplify_expr.h>
|
||||
#include <util/base_type.h>
|
||||
#include <util/symbol_table.h>
|
||||
#include <util/std_expr.h>
|
||||
|
||||
#include "invariant_propagation.h"
|
||||
|
||||
void invariant_propagationt::make_all_true()
|
||||
{
|
||||
for(auto &state : state_map)
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Invariant Set
|
||||
|
||||
#include "invariant_set.h"
|
||||
|
||||
#include <iostream>
|
||||
|
||||
#include <util/symbol_table.h>
|
||||
|
@ -22,8 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/c_types.h>
|
||||
#include <langapi/language_util.h>
|
||||
|
||||
#include "invariant_set.h"
|
||||
|
||||
void inv_object_storet::output(std::ostream &out) const
|
||||
{
|
||||
for(unsigned i=0; i<entries.size(); i++)
|
||||
|
|
|
@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Invariant Set Domain
|
||||
|
||||
#include <util/simplify_expr.h>
|
||||
|
||||
#include "invariant_set_domain.h"
|
||||
|
||||
#include <util/simplify_expr.h>
|
||||
|
||||
void invariant_set_domaint::transform(
|
||||
locationt from_l,
|
||||
locationt to_l,
|
||||
|
|
|
@ -11,9 +11,10 @@ Date: October 2012
|
|||
/// \file
|
||||
/// Over-approximate Concurrency for Threaded Goto Programs
|
||||
|
||||
#include "ai.h"
|
||||
#include "is_threaded.h"
|
||||
|
||||
#include "ai.h"
|
||||
|
||||
class is_threaded_domaint:public ai_domain_baset
|
||||
{
|
||||
public:
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Field-insensitive, location-sensitive may-alias analysis
|
||||
|
||||
#include "local_bitvector_analysis.h"
|
||||
|
||||
#include <iterator>
|
||||
#include <algorithm>
|
||||
|
||||
|
@ -19,8 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/c_types.h>
|
||||
#include <langapi/language_util.h>
|
||||
|
||||
#include "local_bitvector_analysis.h"
|
||||
|
||||
void local_bitvector_analysist::flagst::print(std::ostream &out) const
|
||||
{
|
||||
if(is_unknown())
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// CFG for One Function
|
||||
|
||||
#include "local_cfg.h"
|
||||
|
||||
#if 0
|
||||
#include <iterator>
|
||||
#include <algorithm>
|
||||
|
@ -22,8 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#endif
|
||||
|
||||
#include "local_cfg.h"
|
||||
|
||||
void local_cfgt::build(const goto_programt &goto_program)
|
||||
{
|
||||
nodes.resize(goto_program.instructions.size());
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Field-insensitive, location-sensitive may-alias analysis
|
||||
|
||||
#include "local_may_alias.h"
|
||||
|
||||
#include <iterator>
|
||||
#include <algorithm>
|
||||
|
||||
|
@ -19,8 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/c_types.h>
|
||||
#include <langapi/language_util.h>
|
||||
|
||||
#include "local_may_alias.h"
|
||||
|
||||
/// \return return 'true' iff changed
|
||||
bool local_may_aliast::loc_infot::merge(const loc_infot &src)
|
||||
{
|
||||
|
|
|
@ -11,10 +11,10 @@ Date: March 2013
|
|||
/// \file
|
||||
/// Local variables
|
||||
|
||||
#include <util/std_expr.h>
|
||||
|
||||
#include "locals.h"
|
||||
|
||||
#include <util/std_expr.h>
|
||||
|
||||
void localst::build(const goto_functiont &goto_function)
|
||||
{
|
||||
forall_goto_program_instructions(it, goto_function.body)
|
||||
|
|
|
@ -9,10 +9,10 @@ Author: Georg Weissenbacher, georg@weissenbacher.name
|
|||
/// \file
|
||||
/// Dominators
|
||||
|
||||
#include <iostream>
|
||||
|
||||
#include "natural_loops.h"
|
||||
|
||||
#include <iostream>
|
||||
|
||||
void show_natural_loops(const goto_functionst &goto_functions)
|
||||
{
|
||||
forall_goto_functions(it, goto_functions)
|
||||
|
|
|
@ -13,6 +13,8 @@ Date: February 2013
|
|||
/// Range-based reaching definitions analysis (following Field- Sensitive
|
||||
/// Program Dependence Analysis, Litvak et al., FSE 2010)
|
||||
|
||||
#include "reaching_definitions.h"
|
||||
|
||||
#include <util/pointer_offset_size.h>
|
||||
#include <util/prefix.h>
|
||||
|
||||
|
@ -21,8 +23,6 @@ Date: February 2013
|
|||
#include "is_threaded.h"
|
||||
#include "dirty.h"
|
||||
|
||||
#include "reaching_definitions.h"
|
||||
|
||||
void rd_range_domaint::populate_cache(const irep_idt &identifier) const
|
||||
{
|
||||
assert(bv_container);
|
||||
|
|
|
@ -9,11 +9,11 @@ Author: Peter Schrammel
|
|||
/// \file
|
||||
/// Modified expression replacement for constant propagator
|
||||
|
||||
#include "replace_symbol_ext.h"
|
||||
|
||||
#include <util/std_types.h>
|
||||
#include <util/std_expr.h>
|
||||
|
||||
#include "replace_symbol_ext.h"
|
||||
|
||||
/// does not replace object in address_of expressions
|
||||
bool replace_symbol_extt::replace(exprt &dest) const
|
||||
{
|
||||
|
|
|
@ -9,6 +9,9 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Value Set Propagation
|
||||
|
||||
#define USE_DEPRECATED_STATIC_ANALYSIS_H
|
||||
#include "static_analysis.h"
|
||||
|
||||
#include <cassert>
|
||||
#include <memory>
|
||||
|
||||
|
@ -17,9 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include "is_threaded.h"
|
||||
|
||||
#define USE_DEPRECATED_STATIC_ANALYSIS_H
|
||||
#include "static_analysis.h"
|
||||
|
||||
exprt static_analysis_baset::get_guard(
|
||||
locationt from,
|
||||
locationt to)
|
||||
|
|
|
@ -11,11 +11,11 @@ Date: January 2010
|
|||
/// \file
|
||||
/// Detection for Uninitialized Local Variables
|
||||
|
||||
#include "uninitialized_domain.h"
|
||||
|
||||
#include <util/std_expr.h>
|
||||
#include <util/std_code.h>
|
||||
|
||||
#include "uninitialized_domain.h"
|
||||
|
||||
void uninitialized_domaint::transform(
|
||||
locationt from,
|
||||
locationt to,
|
||||
|
|
|
@ -9,11 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// ANSI-C Language Type Checking
|
||||
|
||||
#include "anonymous_member.h"
|
||||
|
||||
#include <util/std_types.h>
|
||||
#include <util/std_expr.h>
|
||||
|
||||
#include "anonymous_member.h"
|
||||
|
||||
static exprt make_member_expr(
|
||||
const exprt &struct_union,
|
||||
const struct_union_typet::componentt &component,
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// SpecC Language Conversion
|
||||
|
||||
#include "ansi_c_convert_type.h"
|
||||
|
||||
#include <cassert>
|
||||
|
||||
#include <util/c_types.h>
|
||||
|
@ -18,8 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/arith_tools.h>
|
||||
#include <util/std_types.h>
|
||||
|
||||
#include "ansi_c_convert_type.h"
|
||||
|
||||
void ansi_c_convert_typet::read(const typet &type)
|
||||
{
|
||||
clear();
|
||||
|
|
|
@ -9,14 +9,14 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// ANSI-C Language Type Checking
|
||||
|
||||
#include "ansi_c_declaration.h"
|
||||
|
||||
#include <ostream>
|
||||
#include <cassert>
|
||||
|
||||
#include <util/config.h>
|
||||
#include <util/std_types.h>
|
||||
|
||||
#include "ansi_c_declaration.h"
|
||||
|
||||
void ansi_c_declaratort::build(irept &src)
|
||||
{
|
||||
typet *p=static_cast<typet *>(&src);
|
||||
|
|
|
@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "ansi_c_entry_point.h"
|
||||
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
|
@ -24,7 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <goto-programs/goto_functions.h>
|
||||
#include <linking/static_lifetime_init.h>
|
||||
|
||||
#include "ansi_c_entry_point.h"
|
||||
#include "c_nondet_symbol_factory.h"
|
||||
|
||||
exprt::operandst build_function_environment(
|
||||
|
|
|
@ -6,11 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "ansi_c_internal_additions.h"
|
||||
|
||||
#include <util/config.h>
|
||||
|
||||
#include "ansi_c_internal_additions.h"
|
||||
|
||||
const char gcc_builtin_headers_generic[]=
|
||||
"# 1 \"gcc_builtin_headers_generic.h\"\n"
|
||||
#include "gcc_builtin_headers_generic.inc"
|
||||
|
|
|
@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "ansi_c_language.h"
|
||||
|
||||
#include <cstring>
|
||||
#include <sstream>
|
||||
|
@ -18,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <linking/remove_internal_symbols.h>
|
||||
|
||||
#include "ansi_c_entry_point.h"
|
||||
#include "ansi_c_language.h"
|
||||
#include "ansi_c_typecheck.h"
|
||||
#include "ansi_c_parser.h"
|
||||
#include "expr2c.h"
|
||||
|
|
|
@ -6,11 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "ansi_c_parse_tree.h"
|
||||
|
||||
#include <ostream>
|
||||
|
||||
#include "ansi_c_parse_tree.h"
|
||||
|
||||
void ansi_c_parse_treet::swap(ansi_c_parse_treet &ansi_c_parse_tree)
|
||||
{
|
||||
ansi_c_parse_tree.items.swap(items);
|
||||
|
|
|
@ -6,10 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "ansi_c_parser.h"
|
||||
|
||||
#include <iostream>
|
||||
|
||||
#include "ansi_c_parser.h"
|
||||
#include "c_storage_spec.h"
|
||||
|
||||
ansi_c_parsert ansi_c_parser;
|
||||
|
|
|
@ -6,11 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "ansi_c_scope.h"
|
||||
|
||||
#include <ostream>
|
||||
|
||||
#include "ansi_c_scope.h"
|
||||
|
||||
void ansi_c_scopet::print(std::ostream &out) const
|
||||
{
|
||||
out << "Prefix: " << prefix << "\n";
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// ANSI-C Misc Utilities
|
||||
|
||||
#include "c_misc.h"
|
||||
|
||||
#include <cstdio>
|
||||
|
||||
#ifdef _WIN32
|
||||
|
@ -17,8 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#endif
|
||||
#endif
|
||||
|
||||
#include "c_misc.h"
|
||||
|
||||
static void MetaChar(std::string &out, char c, bool inString)
|
||||
{
|
||||
switch(c)
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: DiffBlue Limited. All rights reserved.
|
|||
/// \file
|
||||
/// C Nondet Symbol Factory
|
||||
|
||||
#include "c_nondet_symbol_factory.h"
|
||||
|
||||
#include <set>
|
||||
#include <sstream>
|
||||
|
||||
|
@ -28,8 +30,6 @@ Author: DiffBlue Limited. All rights reserved.
|
|||
|
||||
#include <goto-programs/goto_functions.h>
|
||||
|
||||
#include "c_nondet_symbol_factory.h"
|
||||
|
||||
/// Create a new temporary static symbol
|
||||
/// \param symbol_table: The symbol table to create the symbol in
|
||||
/// \param loc: The location to assign to the symbol
|
||||
|
|
|
@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "c_preprocess.h"
|
||||
|
||||
#include <cstdio>
|
||||
#include <cstdlib>
|
||||
|
@ -31,8 +32,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/std_types.h>
|
||||
#include <util/prefix.h>
|
||||
|
||||
#include "c_preprocess.h"
|
||||
|
||||
#define GCC_DEFINES_16 \
|
||||
" -D__INT_MAX__=32767"\
|
||||
" -D__CHAR_BIT__=8"\
|
||||
|
|
|
@ -6,11 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "c_qualifiers.h"
|
||||
|
||||
#include <ostream>
|
||||
|
||||
#include "c_qualifiers.h"
|
||||
|
||||
std::string c_qualifierst::as_string() const
|
||||
{
|
||||
std::string qualifiers;
|
||||
|
|
|
@ -9,13 +9,14 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Conversion of sizeof Expressions
|
||||
|
||||
#include <util/c_types.h>
|
||||
#include "c_sizeof.h"
|
||||
|
||||
#include <util/config.h>
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/simplify_expr.h>
|
||||
#include <util/std_expr.h>
|
||||
#include <util/c_types.h>
|
||||
|
||||
#include "c_sizeof.h"
|
||||
#include "c_typecast.h"
|
||||
|
||||
exprt c_sizeoft::sizeof_rec(const typet &type)
|
||||
|
|
|
@ -6,11 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "c_storage_spec.h"
|
||||
|
||||
#include <util/expr.h>
|
||||
|
||||
#include "c_storage_spec.h"
|
||||
|
||||
void c_storage_spect::read(const typet &type)
|
||||
{
|
||||
if(type.id()==ID_merged_type ||
|
||||
|
|
|
@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "c_typecast.h"
|
||||
|
||||
#include <algorithm>
|
||||
|
||||
|
@ -20,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/symbol.h>
|
||||
#include <util/simplify_expr.h>
|
||||
|
||||
#include "c_typecast.h"
|
||||
#include "c_qualifiers.h"
|
||||
|
||||
bool c_implicit_typecast(
|
||||
|
|
|
@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// ANSI-C Conversion / Type Checking
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
|
||||
#include "c_typecheck_base.h"
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
|
||||
void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
|
||||
{
|
||||
const code_typet::parameterst ¶meters=
|
||||
|
|
|
@ -9,11 +9,12 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// ANSI-C Conversion / Type Checking
|
||||
|
||||
#include "c_typecheck_base.h"
|
||||
|
||||
#include <util/std_types.h>
|
||||
#include <util/prefix.h>
|
||||
#include <util/config.h>
|
||||
|
||||
#include "c_typecheck_base.h"
|
||||
#include "expr2c.h"
|
||||
#include "type2name.h"
|
||||
#include "c_storage_spec.h"
|
||||
|
|
|
@ -9,11 +9,12 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// C Language Type Checking
|
||||
|
||||
#include "c_typecheck_base.h"
|
||||
|
||||
#include <util/config.h>
|
||||
#include <linking/zero_initializer.h>
|
||||
|
||||
#include "ansi_c_declaration.h"
|
||||
#include "c_typecheck_base.h"
|
||||
|
||||
void c_typecheck_baset::start_typecheck_code()
|
||||
{
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// ANSI-C Language Type Checking
|
||||
|
||||
#include "c_typecheck_base.h"
|
||||
|
||||
#include <cassert>
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
|
@ -24,7 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/pointer_predicates.h>
|
||||
|
||||
#include "c_typecast.h"
|
||||
#include "c_typecheck_base.h"
|
||||
#include "c_sizeof.h"
|
||||
#include "c_qualifiers.h"
|
||||
#include "string_constant.h"
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// ANSI-C Conversion / Type Checking
|
||||
|
||||
#include "c_typecheck_base.h"
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/c_types.h>
|
||||
#include <util/type_eq.h>
|
||||
|
@ -19,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include <linking/zero_initializer.h>
|
||||
|
||||
#include "c_typecheck_base.h"
|
||||
#include "string_constant.h"
|
||||
#include "anonymous_member.h"
|
||||
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include "c_typecheck_base.h"
|
||||
|
||||
#include <unordered_set>
|
||||
|
||||
#include <util/c_types.h>
|
||||
|
@ -18,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/std_types.h>
|
||||
#include <util/pointer_offset_size.h>
|
||||
|
||||
#include "c_typecheck_base.h"
|
||||
#include "c_sizeof.h"
|
||||
#include "c_qualifiers.h"
|
||||
#include "ansi_c_declaration.h"
|
||||
|
|
|
@ -6,9 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "c_typecheck_base.h"
|
||||
|
||||
#include "c_typecast.h"
|
||||
#include "c_typecheck_base.h"
|
||||
|
||||
void c_typecheck_baset::implicit_typecast(
|
||||
exprt &expr,
|
||||
|
|
|
@ -6,12 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "cprover_library.h"
|
||||
|
||||
#include <sstream>
|
||||
|
||||
#include <util/config.h>
|
||||
|
||||
#include "cprover_library.h"
|
||||
#include "ansi_c_language.h"
|
||||
|
||||
struct cprover_library_entryt
|
||||
|
|
|
@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// ANSI-C Language Type Checking
|
||||
|
||||
#include <ostream>
|
||||
|
||||
#include "designator.h"
|
||||
|
||||
#include <ostream>
|
||||
|
||||
void designatort::print(std::ostream &out) const
|
||||
{
|
||||
for(index_listt::const_iterator it=index_list.begin();
|
||||
|
|
|
@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "expr2c.h"
|
||||
|
||||
#include <cassert>
|
||||
#include <cctype>
|
||||
|
@ -38,7 +39,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include "c_misc.h"
|
||||
#include "c_qualifiers.h"
|
||||
#include "expr2c.h"
|
||||
#include "expr2c_class.h"
|
||||
|
||||
/*
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// C Language Conversion
|
||||
|
||||
#include "convert_character_literal.h"
|
||||
|
||||
#include <cassert>
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
|
@ -16,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/std_expr.h>
|
||||
|
||||
#include "unescape_string.h"
|
||||
#include "convert_character_literal.h"
|
||||
|
||||
exprt convert_character_literal(
|
||||
const std::string &src,
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// C++ Language Conversion
|
||||
|
||||
#include "convert_float_literal.h"
|
||||
|
||||
#include <cassert>
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
|
@ -20,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/string2int.h>
|
||||
|
||||
#include "parse_float.h"
|
||||
#include "convert_float_literal.h"
|
||||
|
||||
exprt convert_float_literal(const std::string &src)
|
||||
{
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// C++ Language Conversion
|
||||
|
||||
#include "convert_integer_literal.h"
|
||||
|
||||
#include <cassert>
|
||||
#include <cctype>
|
||||
|
||||
|
@ -18,8 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/std_expr.h>
|
||||
#include <util/string2int.h>
|
||||
|
||||
#include "convert_integer_literal.h"
|
||||
|
||||
exprt convert_integer_literal(const std::string &src)
|
||||
{
|
||||
bool is_unsigned=false, is_imaginary=false;
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// C/C++ Language Conversion
|
||||
|
||||
#include "convert_string_literal.h"
|
||||
|
||||
#include <cassert>
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
|
@ -18,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include "../string_constant.h"
|
||||
|
||||
#include "unescape_string.h"
|
||||
#include "convert_string_literal.h"
|
||||
|
||||
std::basic_string<unsigned int> convert_one_string_literal(
|
||||
const std::string &src)
|
||||
|
|
|
@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Conversion of Expressions
|
||||
|
||||
#include <cctype>
|
||||
|
||||
#include "parse_float.h"
|
||||
|
||||
#include <cctype>
|
||||
|
||||
void parse_float(
|
||||
const std::string &src,
|
||||
mp_integer &significand,
|
||||
|
|
|
@ -9,13 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// ANSI-C Language Conversion
|
||||
|
||||
#include "unescape_string.h"
|
||||
|
||||
#include <cassert>
|
||||
#include <cctype>
|
||||
|
||||
#include <util/unicode.h>
|
||||
|
||||
#include "unescape_string.h"
|
||||
|
||||
static void append_universal_char(
|
||||
unsigned int value,
|
||||
std::string &dest)
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include "padding.h"
|
||||
|
||||
#include <algorithm>
|
||||
|
||||
#include <util/config.h>
|
||||
|
@ -16,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/simplify_expr.h>
|
||||
#include <util/arith_tools.h>
|
||||
|
||||
#include "padding.h"
|
||||
|
||||
mp_integer alignment(const typet &type, const namespacet &ns)
|
||||
{
|
||||
// we need to consider a number of different cases:
|
||||
|
|
|
@ -9,13 +9,14 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// ANSI-C Language Conversion
|
||||
|
||||
#include "preprocessor_line.h"
|
||||
|
||||
#include <cctype>
|
||||
|
||||
#include <util/string2int.h>
|
||||
#include <util/parser.h>
|
||||
|
||||
#include "literals/unescape_string.h"
|
||||
#include "preprocessor_line.h"
|
||||
|
||||
void preprocessor_line(
|
||||
const char *text,
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// printf Formatting
|
||||
|
||||
#include "printf_formatter.h"
|
||||
|
||||
#include <cassert>
|
||||
#include <sstream>
|
||||
|
||||
|
@ -16,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/format_constant.h>
|
||||
#include <util/simplify_expr.h>
|
||||
|
||||
#include "printf_formatter.h"
|
||||
|
||||
const exprt printf_formattert::make_type(
|
||||
const exprt &src, const typet &dest)
|
||||
{
|
||||
|
|
|
@ -6,13 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "string_constant.h"
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/c_types.h>
|
||||
#include <util/std_expr.h>
|
||||
|
||||
#include "string_constant.h"
|
||||
|
||||
string_constantt::string_constantt():
|
||||
exprt(ID_string_constant)
|
||||
{
|
||||
|
|
|
@ -9,14 +9,14 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// Type Naming for C
|
||||
|
||||
#include "type2name.h"
|
||||
|
||||
#include <util/std_types.h>
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/namespace.h>
|
||||
#include <util/symbol.h>
|
||||
#include <util/symbol_table.h>
|
||||
|
||||
#include "type2name.h"
|
||||
|
||||
typedef std::unordered_map<irep_idt, std::pair<size_t, bool>, irep_id_hash>
|
||||
symbol_numbert;
|
||||
|
||||
|
|
|
@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
|
||||
#include <util/type.h>
|
||||
|
||||
class namespacet;
|
||||
|
||||
std::string type2name(const typet &type);
|
||||
std::string type2name(const typet &type, const namespacet &ns);
|
||||
|
||||
|
|
|
@ -6,11 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "assembler_parser.h"
|
||||
|
||||
#include <iostream>
|
||||
|
||||
#include "assembler_parser.h"
|
||||
|
||||
assembler_parsert assembler_parser;
|
||||
|
||||
extern char *yyassemblertext;
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Symbolic Execution of ANSI-C
|
||||
|
||||
#include "all_properties_class.h"
|
||||
|
||||
#include <iostream>
|
||||
|
||||
#include <util/time_stopping.h>
|
||||
|
@ -24,8 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include "bv_cbmc.h"
|
||||
|
||||
#include "all_properties_class.h"
|
||||
|
||||
void bmc_all_propertiest::goal_covered(const cover_goalst::goalt &)
|
||||
{
|
||||
for(auto &g : goal_map)
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Symbolic Execution of ANSI-C
|
||||
|
||||
#include "bmc.h"
|
||||
|
||||
#include <fstream>
|
||||
#include <iostream>
|
||||
#include <memory>
|
||||
|
@ -40,7 +42,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include "counterexample_beautification.h"
|
||||
#include "fault_localization.h"
|
||||
#include "bmc.h"
|
||||
|
||||
void bmct::do_unwind_module()
|
||||
{
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Test-Suite Generation with BMC
|
||||
|
||||
#include "bmc.h"
|
||||
|
||||
#include <iostream>
|
||||
|
||||
#include <util/time_stopping.h>
|
||||
|
@ -24,7 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <goto-programs/xml_goto_trace.h>
|
||||
#include <goto-programs/json_goto_trace.h>
|
||||
|
||||
#include "bmc.h"
|
||||
#include "bv_cbmc.h"
|
||||
|
||||
class bmc_covert:
|
||||
|
|
|
@ -6,12 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "bv_cbmc.h"
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/replace_expr.h>
|
||||
|
||||
#include "bv_cbmc.h"
|
||||
|
||||
bvt bv_cbmct::convert_waitfor(const exprt &expr)
|
||||
{
|
||||
if(expr.operands().size()!=4)
|
||||
|
|
|
@ -9,13 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Writing DIMACS Files
|
||||
|
||||
#include "cbmc_dimacs.h"
|
||||
|
||||
#include <fstream>
|
||||
#include <iostream>
|
||||
|
||||
#include <solvers/sat/dimacs_cnf.h>
|
||||
|
||||
#include "cbmc_dimacs.h"
|
||||
|
||||
bool cbmc_dimacst::write_dimacs(const std::string &filename)
|
||||
{
|
||||
if(filename.empty() || filename=="-")
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Language Registration
|
||||
|
||||
#include "cbmc_parse_options.h"
|
||||
|
||||
#include <langapi/mode.h>
|
||||
|
||||
#include <ansi-c/ansi_c_language.h>
|
||||
|
@ -19,8 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <jsil/jsil_language.h>
|
||||
#endif
|
||||
|
||||
#include "cbmc_parse_options.h"
|
||||
|
||||
void cbmc_parse_optionst::register_languages()
|
||||
{
|
||||
register_language(new_ansi_c_language);
|
||||
|
|
|
@ -17,14 +17,14 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
*/
|
||||
|
||||
#include "cbmc_parse_options.h"
|
||||
|
||||
#include <util/unicode.h>
|
||||
|
||||
#ifdef IREP_HASH_STATS
|
||||
#include <iostream>
|
||||
#endif
|
||||
|
||||
#include "cbmc_parse_options.h"
|
||||
|
||||
#ifdef IREP_HASH_STATS
|
||||
extern unsigned long long irep_hash_cnt;
|
||||
extern unsigned long long irep_cmp_cnt;
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// CBMC Command Line Option Processing
|
||||
|
||||
#include "cbmc_parse_options.h"
|
||||
|
||||
#include <fstream>
|
||||
#include <cstdlib> // exit()
|
||||
#include <iostream>
|
||||
|
@ -58,7 +60,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <langapi/mode.h>
|
||||
|
||||
#include "cbmc_solvers.h"
|
||||
#include "cbmc_parse_options.h"
|
||||
#include "bmc.h"
|
||||
#include "version.h"
|
||||
#include "xml_interface.h"
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Solvers for VCs Generated by Symbolic Execution of ANSI-C
|
||||
|
||||
#include "cbmc_solvers.h"
|
||||
|
||||
#include <memory>
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
|
@ -23,7 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <solvers/prop/aig_prop.h>
|
||||
#include <solvers/sat/dimacs_cnf.h>
|
||||
|
||||
#include "cbmc_solvers.h"
|
||||
#include "bv_cbmc.h"
|
||||
#include "cbmc_dimacs.h"
|
||||
#include "counterexample_beautification.h"
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Counterexample Beautification using Incremental SAT
|
||||
|
||||
#include "counterexample_beautification.h"
|
||||
|
||||
#include <util/threeval.h>
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/symbol.h>
|
||||
|
@ -17,8 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <solvers/prop/minimize.h>
|
||||
#include <solvers/prop/literal_expr.h>
|
||||
|
||||
#include "counterexample_beautification.h"
|
||||
|
||||
void counterexample_beautificationt::get_minimization_list(
|
||||
prop_convt &prop_conv,
|
||||
const symex_target_equationt &equation,
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Peter Schrammel
|
|||
/// \file
|
||||
/// Fault Localization
|
||||
|
||||
#include "fault_localization.h"
|
||||
|
||||
#include <util/threeval.h>
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/symbol.h>
|
||||
|
@ -21,7 +23,6 @@ Author: Peter Schrammel
|
|||
|
||||
#include <goto-symex/build_goto_trace.h>
|
||||
|
||||
#include "fault_localization.h"
|
||||
#include "counterexample_beautification.h"
|
||||
|
||||
void fault_localizationt::freeze_guards()
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Symbolic Execution of ANSI-C
|
||||
|
||||
#include "bmc.h"
|
||||
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
|
||||
|
@ -21,8 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/json.h>
|
||||
#include <util/json_expr.h>
|
||||
|
||||
#include "bmc.h"
|
||||
|
||||
void bmct::show_vcc_plain(std::ostream &out)
|
||||
{
|
||||
out << "\n" << "VERIFICATION CONDITIONS:" << "\n" << "\n";
|
||||
|
|
|
@ -9,13 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Bounded Model Checking for ANSI-C
|
||||
|
||||
#include "symex_bmc.h"
|
||||
|
||||
#include <limits>
|
||||
|
||||
#include <util/source_location.h>
|
||||
#include <util/simplify_expr.h>
|
||||
|
||||
#include "symex_bmc.h"
|
||||
|
||||
symex_bmct::symex_bmct(
|
||||
const namespacet &_ns,
|
||||
symbol_tablet &_new_symbol_table,
|
||||
|
|
|
@ -11,6 +11,8 @@ Date: March 2016
|
|||
/// \file
|
||||
/// Record and print code coverage of symbolic execution
|
||||
|
||||
#include "symex_coverage.h"
|
||||
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <sstream>
|
||||
|
@ -24,8 +26,6 @@ Date: March 2016
|
|||
#include <goto-programs/goto_functions.h>
|
||||
#include <goto-programs/remove_returns.h>
|
||||
|
||||
#include "symex_coverage.h"
|
||||
|
||||
class coverage_recordt
|
||||
{
|
||||
public:
|
||||
|
|
|
@ -9,14 +9,14 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// XML Interface
|
||||
|
||||
#include "xml_interface.h"
|
||||
|
||||
#include <iostream>
|
||||
|
||||
#include <util/message.h>
|
||||
|
||||
#include <xmllang/xml_parser.h>
|
||||
|
||||
#include "xml_interface.h"
|
||||
|
||||
/// XML User Interface
|
||||
void xml_interfacet::get_xml_options(cmdlinet &cmdline)
|
||||
{
|
||||
|
|
|
@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Symex Main Module
|
||||
|
||||
#include <util/unicode.h>
|
||||
|
||||
#include "clobber_parse_options.h"
|
||||
|
||||
#include <util/unicode.h>
|
||||
|
||||
#ifdef _MSC_VER
|
||||
int wmain(int argc, const wchar_t **argv_wide)
|
||||
{
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
/// \file
|
||||
/// Symex Command Line Options Processing
|
||||
|
||||
#include "clobber_parse_options.h"
|
||||
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <cstdlib>
|
||||
|
@ -37,7 +39,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include <cbmc/version.h>
|
||||
|
||||
#include "clobber_parse_options.h"
|
||||
// #include "clobber_instrumenter.h"
|
||||
|
||||
clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv):
|
||||
|
|
|
@ -9,12 +9,13 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include "cpp_typecheck.h"
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/std_types.h>
|
||||
|
||||
#include <util/c_types.h>
|
||||
|
||||
#include "cpp_typecheck.h"
|
||||
#include "cpp_util.h"
|
||||
|
||||
/// \param object: non-typechecked object
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Conversion
|
||||
|
||||
#include "cpp_convert_type.h"
|
||||
|
||||
#include <cassert>
|
||||
|
||||
#include <util/config.h>
|
||||
|
@ -17,7 +19,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
|
||||
#include <util/c_types.h>
|
||||
|
||||
#include "cpp_convert_type.h"
|
||||
#include "cpp_declaration.h"
|
||||
#include "cpp_name.h"
|
||||
|
||||
|
|
|
@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include <ostream>
|
||||
|
||||
#include "cpp_declaration.h"
|
||||
|
||||
#include <ostream>
|
||||
|
||||
void cpp_declarationt::output(std::ostream &out) const
|
||||
{
|
||||
out << "is_template: " << is_template() << "\n";
|
||||
|
|
|
@ -9,11 +9,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include "cpp_declarator.h"
|
||||
|
||||
#include <ostream>
|
||||
#include <cassert>
|
||||
|
||||
#include "cpp_declarator.h"
|
||||
|
||||
void cpp_declaratort::output(std::ostream &out) const
|
||||
{
|
||||
out << " name: " << name().pretty() << "\n";
|
||||
|
|
|
@ -9,13 +9,14 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include "cpp_declarator_converter.h"
|
||||
|
||||
#include <util/source_location.h>
|
||||
#include <util/std_types.h>
|
||||
|
||||
#include <util/c_types.h>
|
||||
|
||||
#include "cpp_type2name.h"
|
||||
#include "cpp_declarator_converter.h"
|
||||
#include "cpp_typecheck.h"
|
||||
|
||||
cpp_declarator_convertert::cpp_declarator_convertert(
|
||||
|
|
|
@ -9,12 +9,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include "cpp_typecheck.h"
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
|
||||
#include <util/c_types.h>
|
||||
|
||||
#include "cpp_typecheck.h"
|
||||
|
||||
/// \return typechecked code
|
||||
codet cpp_typecheckt::cpp_destructor(
|
||||
const source_locationt &source_location,
|
||||
|
|
|
@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include <util/c_types.h>
|
||||
|
||||
#include "cpp_enum_type.h"
|
||||
|
||||
#include <util/c_types.h>
|
||||
|
||||
cpp_enum_typet::cpp_enum_typet():typet(ID_c_enum)
|
||||
{
|
||||
}
|
||||
|
|
|
@ -9,9 +9,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include "cpp_id.h"
|
||||
|
||||
#include <ostream>
|
||||
|
||||
#include "cpp_id.h"
|
||||
#include "cpp_scope.h"
|
||||
|
||||
cpp_idt::cpp_idt():
|
||||
|
|
|
@ -9,13 +9,14 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include "cpp_typecheck.h"
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/simplify_expr.h>
|
||||
|
||||
#include <util/c_types.h>
|
||||
|
||||
#include "cpp_type2name.h"
|
||||
#include "cpp_typecheck.h"
|
||||
|
||||
std::string cpp_typecheckt::template_suffix(
|
||||
const cpp_template_args_tct &template_args)
|
||||
|
|
|
@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "cpp_internal_additions.h"
|
||||
|
||||
#include <ostream>
|
||||
|
||||
|
@ -13,8 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include <ansi-c/ansi_c_internal_additions.h>
|
||||
|
||||
#include "cpp_internal_additions.h"
|
||||
|
||||
std::string c2cpp(const std::string &s)
|
||||
{
|
||||
std::string result;
|
||||
|
|
|
@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Module
|
||||
|
||||
#include "cpp_language.h"
|
||||
|
||||
#include <cstring>
|
||||
#include <sstream>
|
||||
#include <fstream>
|
||||
|
@ -23,7 +25,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
#include <ansi-c/c_preprocess.h>
|
||||
|
||||
#include "cpp_internal_additions.h"
|
||||
#include "cpp_language.h"
|
||||
#include "expr2cpp.h"
|
||||
#include "cpp_parser.h"
|
||||
#include "cpp_typecheck.h"
|
||||
|
|
|
@ -9,11 +9,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include "cpp_name.h"
|
||||
|
||||
#include <cassert>
|
||||
#include <sstream>
|
||||
|
||||
#include "cpp_name.h"
|
||||
|
||||
irep_idt cpp_namet::get_base_name() const
|
||||
{
|
||||
const subt &sub=get_sub();
|
||||
|
|
|
@ -9,9 +9,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include "cpp_namespace_spec.h"
|
||||
|
||||
#include <ostream>
|
||||
|
||||
#include "cpp_namespace_spec.h"
|
||||
#include "cpp_item.h"
|
||||
|
||||
void cpp_namespace_spect::output(std::ostream &out) const
|
||||
|
|
|
@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Parser
|
||||
|
||||
#include <util/config.h>
|
||||
|
||||
#include "cpp_parser.h"
|
||||
|
||||
#include <util/config.h>
|
||||
|
||||
cpp_parsert cpp_parser;
|
||||
|
||||
bool cpp_parse();
|
||||
|
|
|
@ -9,9 +9,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include "cpp_typecheck.h"
|
||||
#include "cpp_scope.h"
|
||||
|
||||
#include "cpp_typecheck.h"
|
||||
|
||||
std::ostream &operator << (std::ostream &out, cpp_scopet::lookup_kindt kind)
|
||||
{
|
||||
switch(kind)
|
||||
|
|
|
@ -9,11 +9,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
|
|||
/// \file
|
||||
/// C++ Language Type Checking
|
||||
|
||||
#include <ostream>
|
||||
|
||||
|
||||
#include "cpp_scopes.h"
|
||||
|
||||
#include <ostream>
|
||||
|
||||
cpp_scopet &cpp_scopest::new_block_scope()
|
||||
{
|
||||
unsigned prefix=++current_scope().compound_counter;
|
||||
|
|
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue