void cfg_dominators_templatet::operator()(P &program)
{
@@ -84,36 +65,14 @@ void cfg_dominators_templatet
::operator()(P &program)
fixedpoint(program);
}
-/*******************************************************************\
-
-Function: cfg_dominators_templatet::initialise
-
- Inputs:
-
- Outputs:
-
- Purpose: Initialises the elements of the fixed point analysis
-
-\*******************************************************************/
-
+/// Initialises the elements of the fixed point analysis
template
void cfg_dominators_templatet::initialise(P &program)
{
cfg(program);
}
-/*******************************************************************\
-
-Function: cfg_dominators_templatet::fixedpoint
-
- Inputs:
-
- Outputs:
-
- Purpose: Computes the MOP for the dominator analysis
-
-\*******************************************************************/
-
+/// Computes the MOP for the dominator analysis
template
void cfg_dominators_templatet::fixedpoint(P &program)
{
@@ -205,19 +164,9 @@ void cfg_dominators_templatet
::fixedpoint(P &program)
}
}
-/*******************************************************************\
-
-Function: dominators_pretty_print_node
-
- Inputs: `node` to print and stream `out` to pretty-print it to
-
- Outputs:
-
- Purpose: Pretty-print a single node in the dominator tree.
- Supply a specialisation if operator<< is not sufficient.
-
-\*******************************************************************/
-
+/// Pretty-print a single node in the dominator tree. Supply a specialisation if
+/// operator<< is not sufficient.
+/// \par parameters: `node` to print and stream `out` to pretty-print it to
template
void dominators_pretty_print_node(const T &node, std::ostream &out)
{
@@ -231,18 +180,7 @@ inline void dominators_pretty_print_node(
out << target->code.pretty();
}
-/*******************************************************************\
-
-Function: cfg_dominators_templatet::output
-
- Inputs:
-
- Outputs:
-
- Purpose: Print the result of the dominator computation
-
-\*******************************************************************/
-
+/// Print the result of the dominator computation
template
void cfg_dominators_templatet::output(std::ostream &out) const
{
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 6735d558cc3..15cda33e864 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -6,6 +6,9 @@ Author: Peter Schrammel
\*******************************************************************/
+/// \file
+/// Constant Propagation
+
#ifdef DEBUG
#include
#endif
@@ -16,18 +19,6 @@ Author: Peter Schrammel
#include "constant_propagator.h"
-/*******************************************************************\
-
-Function: concatenate_array_id
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt concatenate_array_id(
const exprt &array, const exprt &index,
const typet &type)
@@ -47,18 +38,6 @@ exprt concatenate_array_id(
return new_expr;
}
-/*******************************************************************\
-
-Function: concatenate_array_id
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt concatenate_array_id(
const exprt &array, const mp_integer &index,
const typet &type)
@@ -71,18 +50,6 @@ exprt concatenate_array_id(
return new_expr;
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::assign_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void constant_propagator_domaint::assign_rec(
valuest &values,
const exprt &lhs, const exprt &rhs,
@@ -93,7 +60,7 @@ void constant_propagator_domaint::assign_rec(
#ifdef DEBUG
std::cout << "assign: " << from_expr(ns, "", lhs)
- << " := " << from_type(ns, "", rhs_type) << std::endl;
+ << " := " << from_type(ns, "", rhs_type) << '\n';
#endif
if(lhs.id()==ID_symbol && rhs.id()==ID_if)
@@ -154,18 +121,6 @@ void constant_propagator_domaint::assign_rec(
#endif
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::transform
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void constant_propagator_domaint::transform(
locationt from,
locationt to,
@@ -255,18 +210,7 @@ void constant_propagator_domaint::transform(
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::two_way_propagate_rec
-
- Inputs:
-
- Outputs:
-
- Purpose: handles equalities and conjunctions containing equalities
-
-\*******************************************************************/
-
+/// handles equalities and conjunctions containing equalities
bool constant_propagator_domaint::two_way_propagate_rec(
const exprt &expr,
const namespacet &ns)
@@ -308,18 +252,6 @@ bool constant_propagator_domaint::two_way_propagate_rec(
return change;
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::assign
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void constant_propagator_domaint::assign(
valuest &dest,
const symbol_exprt &lhs,
@@ -331,17 +263,19 @@ void constant_propagator_domaint::assign(
dest.set_to(lhs, rhs);
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::is_array_constant
-
- Inputs:
-
- Outputs:
-
- Purpose:
+/// Simplify the condition given context-sensitive knowledge from the abstract
+/// state.
+/// \par parameters: The condition to simplify and its namespace.
+/// \return The simplified condition.
+bool constant_propagator_domaint::ai_simplify(
+ exprt &condition,
+ const namespacet &ns) const
+{
+ bool b=values.replace_const.replace(condition);
+ b&=simplify(condition, ns);
-\*******************************************************************/
+ return b;
+}
bool constant_propagator_domaint::valuest::is_array_constant(const exprt &expr) const
{
@@ -355,18 +289,6 @@ bool constant_propagator_domaint::valuest::is_array_constant(const exprt &expr)
return true;
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::valuest::is_constant
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
{
if(expr.id()==ID_side_effect &&
@@ -395,18 +317,6 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
return true;
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::valuest::is_constant_address_of
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool constant_propagator_domaint::valuest::is_constant_address_of(
const exprt &expr) const
{
@@ -426,18 +336,7 @@ bool constant_propagator_domaint::valuest::is_constant_address_of(
return true;
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::valuest::set_to_top
-
- Inputs:
-
- Outputs:
-
- Purpose: Do not call this when iterating over replace_const.expr_map!
-
-\*******************************************************************/
-
+/// Do not call this when iterating over replace_const.expr_map!
bool constant_propagator_domaint::valuest::set_to_top(const irep_idt &id)
{
bool result = false;
@@ -455,18 +354,6 @@ bool constant_propagator_domaint::valuest::set_to_top(const irep_idt &id)
return result;
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::valuest::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void constant_propagator_domaint::valuest::output(
std::ostream &out,
const namespacet &ns) const
@@ -481,18 +368,6 @@ void constant_propagator_domaint::valuest::output(
<< from_expr(ns, "", replace_pair.second) << '\n';
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void constant_propagator_domaint::output(
std::ostream &out,
const ai_baset &ai,
@@ -501,18 +376,8 @@ void constant_propagator_domaint::output(
values.output(out, ns);
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::valuest::merge
-
- Inputs:
-
- Outputs: Return true if "this" has changed.
-
- Purpose: join
-
-\*******************************************************************/
-
+/// join
+/// \return Return true if "this" has changed.
bool constant_propagator_domaint::valuest::merge(const valuest &src)
{
// nothing to do
@@ -557,18 +422,8 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
return changed;
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::valuest::meet
-
- Inputs:
-
- Outputs: Return true if "this" has changed.
-
- Purpose: meet
-
-\*******************************************************************/
-
+/// meet
+/// \return Return true if "this" has changed.
bool constant_propagator_domaint::valuest::meet(const valuest &src)
{
if(src.is_bottom || is_bottom)
@@ -600,18 +455,7 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src)
return changed;
}
-/*******************************************************************\
-
-Function: constant_propagator_domaint::merge
-
- Inputs:
-
- Outputs: Return true if "this" has changed.
-
- Purpose:
-
-\*******************************************************************/
-
+/// \return Return true if "this" has changed.
bool constant_propagator_domaint::merge(
const constant_propagator_domaint &other,
locationt from,
@@ -620,18 +464,6 @@ bool constant_propagator_domaint::merge(
return values.merge(other.values);
}
-/*******************************************************************\
-
-Function: constant_propagator_ait::replace
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void constant_propagator_ait::replace(
goto_functionst &goto_functions,
const namespacet &ns)
@@ -640,18 +472,6 @@ void constant_propagator_ait::replace(
replace(f_it->second, ns);
}
-/*******************************************************************\
-
-Function: constant_propagator_ait::replace_array_symbol
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void constant_propagator_ait::replace_array_symbol(exprt &expr)
{
if (expr.id()==ID_index)
@@ -668,18 +488,6 @@ void constant_propagator_ait::replace_array_symbol(exprt &expr)
}
-/*******************************************************************\
-
-Function: constant_propagator_ait::replace
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void constant_propagator_ait::replace(
goto_functionst::goto_functiont &goto_function,
const namespacet &ns)
@@ -732,18 +540,6 @@ void constant_propagator_ait::replace(
}
}
-/*******************************************************************\
-
-Function: constant_propagator_ait::replace_types_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void constant_propagator_ait::replace_types_rec(
const replace_symbolt &replace_const,
exprt &expr)
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 0766b458f7d..0b54c79bdb8 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -6,6 +6,9 @@ Author: Peter Schrammel
\*******************************************************************/
+/// \file
+/// Constant propagation
+
#ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
#define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
@@ -30,6 +33,10 @@ class constant_propagator_domaint:public ai_domain_baset
void make_entry() final { values.set_to_top(); }
bool merge(const constant_propagator_domaint &, locationt, locationt);
+ virtual bool ai_simplify(
+ exprt &condition,
+ const namespacet &ns) const override;
+
struct valuest
{
public:
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index 0a3f0306471..face9d8ae67 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Field-insensitive, location-sensitive bitvector analysis
+
#include
#include
@@ -13,18 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::set_bit
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void custom_bitvector_domaint::set_bit(
const irep_idt &identifier,
unsigned bit_nr,
@@ -50,18 +41,6 @@ void custom_bitvector_domaint::set_bit(
}
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::set_bit
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void custom_bitvector_domaint::set_bit(
const exprt &lhs,
unsigned bit_nr,
@@ -72,18 +51,6 @@ void custom_bitvector_domaint::set_bit(
set_bit(id, bit_nr, mode);
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::object2id
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
irep_idt custom_bitvector_domaint::object2id(const exprt &src)
{
if(src.id()==ID_symbol)
@@ -117,18 +84,6 @@ irep_idt custom_bitvector_domaint::object2id(const exprt &src)
return irep_idt();
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::assign_lhs
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void custom_bitvector_domaint::assign_lhs(
const exprt &lhs,
const vectorst &vectors)
@@ -138,18 +93,6 @@ void custom_bitvector_domaint::assign_lhs(
assign_lhs(id, vectors);
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::assign_lhs
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void custom_bitvector_domaint::assign_lhs(
const irep_idt &identifier,
const vectorst &vectors)
@@ -167,18 +110,6 @@ void custom_bitvector_domaint::assign_lhs(
may_bits[identifier]=vectors.may_bits;
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::get_rhs
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
custom_bitvector_domaint::vectorst
custom_bitvector_domaint::get_rhs(const irep_idt &identifier) const
{
@@ -195,18 +126,6 @@ custom_bitvector_domaint::vectorst
return vectors;
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::get_rhs
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
custom_bitvector_domaint::vectorst
custom_bitvector_domaint::get_rhs(const exprt &rhs) const
{
@@ -231,18 +150,6 @@ custom_bitvector_domaint::vectorst
return vectorst();
}
-/*******************************************************************\
-
-Function: custom_bitvector_analysist::get_bit_nr
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
unsigned custom_bitvector_analysist::get_bit_nr(
const exprt &string_expr)
{
@@ -261,18 +168,6 @@ unsigned custom_bitvector_analysist::get_bit_nr(
return bits("(unknown)");
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::aliases
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
std::set custom_bitvector_analysist::aliases(
const exprt &src,
locationt loc)
@@ -309,18 +204,6 @@ std::set custom_bitvector_analysist::aliases(
return std::set();
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::transform
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void custom_bitvector_domaint::transform(
locationt from,
locationt to,
@@ -549,18 +432,6 @@ void custom_bitvector_domaint::transform(
}
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void custom_bitvector_domaint::output(
std::ostream &out,
const ai_baset &ai,
@@ -608,18 +479,6 @@ void custom_bitvector_domaint::output(
}
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::merge
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool custom_bitvector_domaint::merge(
const custom_bitvector_domaint &b,
locationt from,
@@ -673,18 +532,7 @@ bool custom_bitvector_domaint::merge(
return changed;
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::erase_blank_vectors
-
- Inputs:
-
- Outputs:
-
- Purpose: erase blank bitvectors
-
-\*******************************************************************/
-
+/// erase blank bitvectors
void custom_bitvector_domaint::erase_blank_vectors(bitst &bits)
{
for(bitst::iterator a_it=bits.begin();
@@ -698,18 +546,6 @@ void custom_bitvector_domaint::erase_blank_vectors(bitst &bits)
}
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::has_get_must_or_may
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool custom_bitvector_domaint::has_get_must_or_may(const exprt &src)
{
if(src.id()=="get_must" ||
@@ -723,18 +559,6 @@ bool custom_bitvector_domaint::has_get_must_or_may(const exprt &src)
return false;
}
-/*******************************************************************\
-
-Function: custom_bitvector_domaint::eval
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt custom_bitvector_domaint::eval(
const exprt &src,
custom_bitvector_analysist &custom_bitvector_analysis) const
@@ -797,34 +621,10 @@ exprt custom_bitvector_domaint::eval(
}
}
-/*******************************************************************\
-
-Function: custom_bitvector_analysist::instrument
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void custom_bitvector_analysist::instrument(goto_functionst &)
{
}
-/*******************************************************************\
-
-Function: custom_bitvector_analysist::check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void custom_bitvector_analysist::check(
const namespacet &ns,
const goto_functionst &goto_functions,
diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h
index e77cb6fc58b..ff2884cc2ec 100644
--- a/src/analyses/custom_bitvector_analysis.h
+++ b/src/analyses/custom_bitvector_analysis.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Field-insensitive, location-sensitive bitvector analysis
+
#ifndef CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
#define CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
@@ -15,14 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "ai.h"
#include "local_may_alias.h"
-/*******************************************************************\
-
- Class: custom_bitvector_domaint
-
- Purpose:
-
-\*******************************************************************/
-
class custom_bitvector_analysist;
class custom_bitvector_domaint:public ai_domain_baset
diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index 730ec0266e4..4d9d37eae6d 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/src/analyses/dependence_graph.cpp
@@ -9,24 +9,18 @@ Date: August 2013
\*******************************************************************/
+/// \file
+/// Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010
+
#include
+#include
+#include
+
#include "goto_rw.h"
#include "dependence_graph.h"
-/*******************************************************************\
-
-Function: dep_graph_domaint::merge
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool dep_graph_domaint::merge(
const dep_graph_domaint &src,
goto_programt::const_targett from,
@@ -66,18 +60,6 @@ bool dep_graph_domaint::merge(
return changed;
}
-/*******************************************************************\
-
-Function: dep_graph_domaint::control_dependencies
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void dep_graph_domaint::control_dependencies(
goto_programt::const_targett from,
goto_programt::const_targett to,
@@ -144,18 +126,6 @@ void dep_graph_domaint::control_dependencies(
dep_graph.add_dep(dep_edget::kindt::CTRL, c_dep, to);
}
-/*******************************************************************\
-
-Function: may_be_def_use_pair
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
static bool may_be_def_use_pair(
const mp_integer &w_start,
const mp_integer &w_end,
@@ -177,18 +147,6 @@ static bool may_be_def_use_pair(
return false;
}
-/*******************************************************************\
-
-Function: dep_graph_domaint::data_depdendencies
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void dep_graph_domaint::data_dependencies(
goto_programt::const_targett from,
goto_programt::const_targett to,
@@ -238,18 +196,6 @@ void dep_graph_domaint::data_dependencies(
}
}
-/*******************************************************************\
-
-Function: dep_graph_domaint::transform
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void dep_graph_domaint::transform(
goto_programt::const_targett from,
goto_programt::const_targett to,
@@ -297,18 +243,6 @@ void dep_graph_domaint::transform(
data_dependencies(from, to, *dep_graph, ns);
}
-/*******************************************************************\
-
-Function: dep_graph_domaint::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void dep_graph_domaint::output(
std::ostream &out,
const ai_baset &ai,
@@ -326,7 +260,7 @@ void dep_graph_domaint::output(
out << ",";
out << (*it)->location_number;
}
- out << std::endl;
+ out << '\n';
}
if(!data_deps.empty())
@@ -341,21 +275,40 @@ void dep_graph_domaint::output(
out << ",";
out << (*it)->location_number;
}
- out << std::endl;
+ out << '\n';
}
}
-/*******************************************************************\
-
-Function: dependence_grapht::add_dep
-
- Inputs:
+/// Outputs the current value of the domain.
+/// \par parameters: The abstract interpreter and the namespace.
+/// \return The domain, formatted as a JSON object.
+jsont dep_graph_domaint::output_json(
+ const ai_baset &ai,
+ const namespacet &ns) const
+{
+ json_arrayt graph;
- Outputs:
+ for(const auto &cd : control_deps)
+ {
+ json_objectt &link=graph.push_back().make_object();
+ link["locationNumber"]=
+ json_numbert(std::to_string(cd->location_number));
+ link["sourceLocation"]=json(cd->source_location);
+ link["type"]=json_stringt("control");
+ }
- Purpose:
+ for(const auto &dd : data_deps)
+ {
+ json_objectt &link=graph.push_back().make_object();
+ link["locationNumber"]=
+ json_numbert(std::to_string(dd->location_number));
+ link["sourceLocation"]=json(dd->source_location);
+ json_stringt(dd->source_location.as_string());
+ link["type"]=json_stringt("data");
+ }
-\*******************************************************************/
+ return graph;
+}
void dependence_grapht::add_dep(
dep_edget::kindt kind,
diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h
index fae7c7adbd4..4cd7be4c589 100644
--- a/src/analyses/dependence_graph.h
+++ b/src/analyses/dependence_graph.h
@@ -9,6 +9,9 @@ Date: August 2013
\*******************************************************************/
+/// \file
+/// Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010
+
#ifndef CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
#define CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
@@ -87,7 +90,11 @@ class dep_graph_domaint:public ai_domain_baset
const ai_baset &ai,
const namespacet &ns) const final;
- void make_top() final
+ jsont output_json(
+ const ai_baset &ai,
+ const namespacet &ns) const override;
+
+ void make_top() final override
{
assert(node_id!=std::numeric_limits::max());
diff --git a/src/analyses/dirty.cpp b/src/analyses/dirty.cpp
index a159f6ddef2..9a42e7f0a0f 100644
--- a/src/analyses/dirty.cpp
+++ b/src/analyses/dirty.cpp
@@ -8,22 +8,13 @@ Date: March 2013
\*******************************************************************/
+/// \file
+/// Local variables whose address is taken
+
#include
#include "dirty.h"
-/*******************************************************************\
-
-Function: dirtyt::build
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void dirtyt::build(const goto_functiont &goto_function)
{
forall_goto_program_instructions(it, goto_function.body)
@@ -33,18 +24,6 @@ void dirtyt::build(const goto_functiont &goto_function)
}
}
-/*******************************************************************\
-
-Function: dirtyt::find_dirty
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void dirtyt::find_dirty(const exprt &expr)
{
if(expr.id()==ID_address_of)
@@ -58,18 +37,6 @@ void dirtyt::find_dirty(const exprt &expr)
find_dirty(*it);
}
-/*******************************************************************\
-
-Function: dirtyt::find_dirty_address_of
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void dirtyt::find_dirty_address_of(const exprt &expr)
{
if(expr.id()==ID_symbol)
@@ -100,20 +67,8 @@ void dirtyt::find_dirty_address_of(const exprt &expr)
}
}
-/*******************************************************************\
-
-Function: dirtyt::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void dirtyt::output(std::ostream &out) const
{
for(const auto &d : dirty)
- out << d << std::endl;
+ out << d << '\n';
}
diff --git a/src/analyses/dirty.h b/src/analyses/dirty.h
index f60b86703c4..52801d05281 100644
--- a/src/analyses/dirty.h
+++ b/src/analyses/dirty.h
@@ -8,6 +8,9 @@ Date: March 2013
\*******************************************************************/
+/// \file
+/// Variables whose address is taken
+
#ifndef CPROVER_ANALYSES_DIRTY_H
#define CPROVER_ANALYSES_DIRTY_H
diff --git a/src/analyses/does_remove_const.cpp b/src/analyses/does_remove_const.cpp
index fcccd8219c9..90d82f99e19 100644
--- a/src/analyses/does_remove_const.cpp
+++ b/src/analyses/does_remove_const.cpp
@@ -6,6 +6,9 @@
\*******************************************************************/
+/// \file
+/// Analyses
+
#include
#include
#include
@@ -15,21 +18,10 @@
#include "does_remove_const.h"
-/*******************************************************************\
-
-Function: does_remove_constt::does_remove_constt
-
- Inputs:
- goto_program - the goto program to check
- ns - the namespace of the goto program (used for checking type equality)
-
- Outputs:
-
- Purpose: A naive analysis to look for casts that remove const-ness from
- pointers.
-
-\*******************************************************************/
-
+/// 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
+/// equality)
does_remove_constt::does_remove_constt(
const goto_programt &goto_program,
const namespacet &ns):
@@ -37,19 +29,8 @@ does_remove_constt::does_remove_constt(
ns(ns)
{}
-/*******************************************************************\
-
-Function: does_remove_constt::operator()
-
- Inputs:
-
- Outputs: Returns true if the program contains a const-removing cast
-
- Purpose: A naive analysis to look for casts that remove const-ness from
- pointers.
-
-\*******************************************************************/
-
+/// A naive analysis to look for casts that remove const-ness from pointers.
+/// \return Returns true if the program contains a const-removing cast
bool does_remove_constt::operator()() const
{
for(const goto_programt::instructiont &instruction :
@@ -80,22 +61,12 @@ bool does_remove_constt::operator()() const
return false;
}
-/*******************************************************************\
-
-Function: does_remove_constt::does_expr_lose_const()
-
- Inputs:
- expr - The expression to check
-
- Outputs: Returns true if somewhere in the passed expression tree the const-ness
- is lost.
-
- Purpose: Search the expression tree to look for any children that have the
- same base type, but a less strict const qualification.
- If one is found, we return true.
-
-\*******************************************************************/
-
+/// Search the expression tree to look for any children that have the same base
+/// type, but a less strict const qualification. If one is found, we return
+/// true.
+/// \param expr: The expression to check
+/// \return Returns true if somewhere in the passed expression tree the const-
+/// ness is lost.
bool does_remove_constt::does_expr_lose_const(const exprt &expr) const
{
const typet &root_type=expr.type();
@@ -122,29 +93,20 @@ bool does_remove_constt::does_expr_lose_const(const exprt &expr) const
return false;
}
-/*******************************************************************\
-
-Function: does_remove_constt::is_type_at_least_as_const_as
-
- Inputs:
- type_more_const - the type we are expecting to be at least as const qualified
- type_compare - the type we are comparing against which may be less const
- qualified
-
- Outputs: Returns true if type_more_const is at least as const as type_compare
-
- Purpose: A recursive check to check the type_more_const is at least as const
- as type compare.
-
- type_more_const | type_compare || result
- ----------------------------------------
- const int * | const int * -> true
- int * | const int * -> false
- const int * | int * -> true
- int * | int * const -> false
-
-\*******************************************************************/
-
+/// A recursive check to check the type_more_const is at least as const as type
+/// compare.
+///
+/// type_more_const | type_compare || result
+/// ----------------------------------------
+/// const int * | const int * -> true
+/// int * | const int * -> false
+/// const int * | int * -> true
+/// int * | int * const -> false
+/// \param type_more_const: the type we are expecting to be at least as const
+/// qualified
+/// \param type_compare: the type we are comparing against which may be less
+/// const qualified
+/// \return Returns true if type_more_const is at least as const as type_compare
bool does_remove_constt::is_type_at_least_as_const_as(
const typet *type_more_const, const typet *type_compare) const
{
diff --git a/src/analyses/does_remove_const.h b/src/analyses/does_remove_const.h
index 594682c7d50..f0cf2a25799 100644
--- a/src/analyses/does_remove_const.h
+++ b/src/analyses/does_remove_const.h
@@ -5,6 +5,9 @@
Author: DiffBlue Limited. All rights reserved.
\*******************************************************************/
+/// \file
+/// Analyses
+
#ifndef CPROVER_ANALYSES_DOES_REMOVE_CONST_H
#define CPROVER_ANALYSES_DOES_REMOVE_CONST_H
diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
index 1382e9d1689..3b0e7fc3f5c 100644
--- a/src/analyses/escape_analysis.cpp
+++ b/src/analyses/escape_analysis.cpp
@@ -6,22 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Field-insensitive, location-sensitive escape analysis
+
#include
#include "escape_analysis.h"
-/*******************************************************************\
-
-Function: escape_domaint::is_tracked
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool escape_domaint::is_tracked(const symbol_exprt &symbol)
{
const irep_idt &identifier=symbol.get_identifier();
@@ -34,18 +25,6 @@ bool escape_domaint::is_tracked(const symbol_exprt &symbol)
return true;
}
-/*******************************************************************\
-
-Function: escape_domaint::get_function
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
irep_idt escape_domaint::get_function(const exprt &lhs)
{
if(lhs.id()==ID_address_of)
@@ -61,18 +40,6 @@ irep_idt escape_domaint::get_function(const exprt &lhs)
return irep_idt();
}
-/*******************************************************************\
-
-Function: escape_domaint::assign_lhs_cleanup
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void escape_domaint::assign_lhs_cleanup(
const exprt &lhs,
const std::set &cleanup_functions)
@@ -92,18 +59,6 @@ void escape_domaint::assign_lhs_cleanup(
}
}
-/*******************************************************************\
-
-Function: escape_domaint::assign_lhs_aliases
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void escape_domaint::assign_lhs_aliases(
const exprt &lhs,
const std::set &alias_set)
@@ -125,18 +80,6 @@ void escape_domaint::assign_lhs_aliases(
}
}
-/*******************************************************************\
-
-Function: escape_domaint::get_rhs_cleanup
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void escape_domaint::get_rhs_cleanup(
const exprt &rhs,
std::set &cleanup_functions)
@@ -167,18 +110,6 @@ void escape_domaint::get_rhs_cleanup(
}
}
-/*******************************************************************\
-
-Function: escape_domaint::get_rhs_aliases
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void escape_domaint::get_rhs_aliases(
const exprt &rhs,
std::set &alias_set)
@@ -211,18 +142,6 @@ void escape_domaint::get_rhs_aliases(
}
}
-/*******************************************************************\
-
-Function: escape_domaint::get_rhs_aliases_address_of
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void escape_domaint::get_rhs_aliases_address_of(
const exprt &rhs,
std::set &alias_set)
@@ -242,18 +161,6 @@ void escape_domaint::get_rhs_aliases_address_of(
}
}
-/*******************************************************************\
-
-Function: escape_domaint::transform
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void escape_domaint::transform(
locationt from,
locationt to,
@@ -346,18 +253,6 @@ void escape_domaint::transform(
}
}
-/*******************************************************************\
-
-Function: escape_domaint::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void escape_domaint::output(
std::ostream &out,
const ai_baset &ai,
@@ -404,18 +299,6 @@ void escape_domaint::output(
}
}
-/*******************************************************************\
-
-Function: escape_domaint::merge
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool escape_domaint::merge(
const escape_domaint &b,
locationt from,
@@ -480,18 +363,6 @@ bool escape_domaint::merge(
return changed;
}
-/*******************************************************************\
-
-Function: escape_domaint::check_lhs
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void escape_domaint::check_lhs(
const exprt &lhs,
std::set &cleanup_functions)
@@ -527,18 +398,6 @@ void escape_domaint::check_lhs(
}
}
-/*******************************************************************\
-
-Function: escape_analysist::insert_cleanup
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void escape_analysist::insert_cleanup(
goto_functionst::goto_functiont &goto_function,
goto_programt::targett location,
@@ -576,18 +435,6 @@ void escape_analysist::insert_cleanup(
}
}
-/*******************************************************************\
-
-Function: escape_analysist::instrument
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void escape_analysist::instrument(
goto_functionst &goto_functions,
const namespacet &ns)
diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h
index 948bed3fea8..00f865b45e4 100644
--- a/src/analyses/escape_analysis.h
+++ b/src/analyses/escape_analysis.h
@@ -7,6 +7,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Field-insensitive, location-sensitive, over-approximative escape analysis
+
#ifndef CPROVER_ANALYSES_ESCAPE_ANALYSIS_H
#define CPROVER_ANALYSES_ESCAPE_ANALYSIS_H
@@ -16,14 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "ai.h"
-/*******************************************************************\
-
- Class: escape_domaint
-
- Purpose:
-
-\*******************************************************************/
-
class escape_analysist;
class escape_domaint:public ai_domain_baset
diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp
index bc4dd11e889..f6766038eba 100644
--- a/src/analyses/flow_insensitive_analysis.cpp
+++ b/src/analyses/flow_insensitive_analysis.cpp
@@ -7,6 +7,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Flow Insensitive Static Analysis
+
#include
#include
@@ -14,18 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "flow_insensitive_analysis.h"
-/*******************************************************************\
-
-Function: flow_insensitive_abstract_domain_baset::get_guard
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt flow_insensitive_abstract_domain_baset::get_guard(
locationt from,
locationt to) const
@@ -46,18 +37,6 @@ exprt flow_insensitive_abstract_domain_baset::get_guard(
return from->guard;
}
-/*******************************************************************\
-
-Function: flow_insensitive_abstract_domain_baset::get_return_lhs
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt flow_insensitive_abstract_domain_baset::get_return_lhs(locationt to) const
{
// get predecessor of "to"
@@ -76,18 +55,6 @@ exprt flow_insensitive_abstract_domain_baset::get_return_lhs(locationt to) const
return code.lhs();
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::operator()
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void flow_insensitive_analysis_baset::operator()(
const goto_functionst &goto_functions)
{
@@ -95,18 +62,6 @@ void flow_insensitive_analysis_baset::operator()(
fixedpoint(goto_functions);
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::operator()
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void flow_insensitive_analysis_baset::operator()(
const goto_programt &goto_program)
{
@@ -115,45 +70,18 @@ void flow_insensitive_analysis_baset::operator()(
fixedpoint(goto_program, goto_functions);
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void flow_insensitive_analysis_baset::output(
const goto_functionst &goto_functions,
std::ostream &out)
{
forall_goto_functions(f_it, goto_functions)
{
- out << "////" << std::endl;
- out << "//// Function: " << f_it->first << std::endl;
- out << "////" << std::endl;
- out << std::endl;
+ out << "////\n" << "//// Function: " << f_it->first << "\n////\n\n";
output(f_it->second.body, f_it->first, out);
}
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void flow_insensitive_analysis_baset::output(
const goto_programt &goto_program,
const irep_idt &identifier,
@@ -162,18 +90,6 @@ void flow_insensitive_analysis_baset::output(
get_state().output(ns, out);
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::get_next
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
flow_insensitive_analysis_baset::locationt
flow_insensitive_analysis_baset::get_next(
working_sett &working_set)
@@ -191,18 +107,6 @@ flow_insensitive_analysis_baset::get_next(
return l;
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::fixedpoint
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool flow_insensitive_analysis_baset::fixedpoint(
const goto_programt &goto_program,
const goto_functionst &goto_functions)
@@ -231,18 +135,6 @@ bool flow_insensitive_analysis_baset::fixedpoint(
return new_data;
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::visit
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool flow_insensitive_analysis_baset::visit(
locationt l,
working_sett &working_set,
@@ -253,7 +145,7 @@ bool flow_insensitive_analysis_baset::visit(
#if 0
std::cout << "Visiting: " << l->function << " " <<
- l->location_number << std::endl;
+ l->location_number << '\n';
#endif
seen_locations.insert(l);
@@ -294,14 +186,14 @@ bool flow_insensitive_analysis_baset::visit(
}
// if (id2string(l->function).find("debug")!=std::string::npos)
-// std::cout << l->function << std::endl; //=="messages::debug")
+// std::cout << l->function << '\n'; //=="messages::debug")
// {
// static unsigned state_cntr=0;
// std::string s("pastate"); s += std::to_string(state_cntr);
// std::ofstream f(s.c_str());
// goto_program.output_instruction(ns, "", f, l);
-// f << std::endl;
+// f << '\n';
// get_state().output(ns, f);
// f.close();
// state_cntr++;
@@ -310,18 +202,6 @@ bool flow_insensitive_analysis_baset::visit(
return new_data;
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::do_function_call
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool flow_insensitive_analysis_baset::do_function_call(
locationt l_call,
const goto_functionst &goto_functions,
@@ -402,18 +282,6 @@ bool flow_insensitive_analysis_baset::do_function_call(
return new_data;
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::do_function_call_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool flow_insensitive_analysis_baset::do_function_call_rec(
locationt l_call,
const exprt &function,
@@ -523,18 +391,6 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
return new_data;
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::fixedpoint
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void flow_insensitive_analysis_baset::fixedpoint(
const goto_functionst &goto_functions)
{
@@ -548,18 +404,6 @@ void flow_insensitive_analysis_baset::fixedpoint(
}
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::fixedpoint
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool flow_insensitive_analysis_baset::fixedpoint(
const goto_functionst::function_mapt::const_iterator it,
const goto_functionst &goto_functions)
@@ -568,36 +412,12 @@ bool flow_insensitive_analysis_baset::fixedpoint(
return fixedpoint(it->second.body, goto_functions);
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::update
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void flow_insensitive_analysis_baset::update(
const goto_functionst &goto_functions)
{
// no need to copy value sets around
}
-/*******************************************************************\
-
-Function: flow_insensitive_analysis_baset::update
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void flow_insensitive_analysis_baset::update(
const goto_programt &goto_program)
{
diff --git a/src/analyses/flow_insensitive_analysis.h b/src/analyses/flow_insensitive_analysis.h
index 07d1f0f77cd..bf06cf90cdf 100644
--- a/src/analyses/flow_insensitive_analysis.h
+++ b/src/analyses/flow_insensitive_analysis.h
@@ -7,6 +7,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Flow Insensitive Static Analysis
+
#ifndef CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
#define CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp
index 33ad0f7f186..28fabae92b4 100644
--- a/src/analyses/global_may_alias.cpp
+++ b/src/analyses/global_may_alias.cpp
@@ -6,19 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
-#include "global_may_alias.h"
-
-/*******************************************************************\
-
-Function: global_may_alias_domaint::assign_lhs_aliases
-
- Inputs:
-
- Outputs:
-
- Purpose:
+/// \file
+/// Field-insensitive, location-sensitive gobal may alias analysis
-\*******************************************************************/
+#include "global_may_alias.h"
void global_may_alias_domaint::assign_lhs_aliases(
const exprt &lhs,
@@ -37,18 +28,6 @@ void global_may_alias_domaint::assign_lhs_aliases(
}
}
-/*******************************************************************\
-
-Function: global_may_alias_domaint::get_rhs_aliases
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void global_may_alias_domaint::get_rhs_aliases(
const exprt &rhs,
std::set &alias_set)
@@ -77,18 +56,6 @@ void global_may_alias_domaint::get_rhs_aliases(
}
}
-/*******************************************************************\
-
-Function: global_may_alias_domaint::get_rhs_aliases_address_of
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void global_may_alias_domaint::get_rhs_aliases_address_of(
const exprt &rhs,
std::set &alias_set)
@@ -108,18 +75,6 @@ void global_may_alias_domaint::get_rhs_aliases_address_of(
}
}
-/*******************************************************************\
-
-Function: global_may_alias_domaint::transform
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void global_may_alias_domaint::transform(
locationt from,
locationt to,
@@ -163,18 +118,6 @@ void global_may_alias_domaint::transform(
}
}
-/*******************************************************************\
-
-Function: global_may_alias_domaint::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void global_may_alias_domaint::output(
std::ostream &out,
const ai_baset &ai,
@@ -213,18 +156,6 @@ void global_may_alias_domaint::output(
}
}
-/*******************************************************************\
-
-Function: global_may_alias_domaint::merge
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool global_may_alias_domaint::merge(
const global_may_alias_domaint &b,
locationt from,
diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h
index 2f4a49b2d0a..d946b371c05 100644
--- a/src/analyses/global_may_alias.h
+++ b/src/analyses/global_may_alias.h
@@ -7,6 +7,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Field-insensitive, location-sensitive, over-approximative escape analysis
+
#ifndef CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
#define CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
@@ -16,14 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "ai.h"
-/*******************************************************************\
-
- Class: global_may_alias_domaint
-
- Purpose:
-
-\*******************************************************************/
-
class global_may_alias_analysist;
class global_may_alias_domaint:public ai_domain_baset
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index a6871b94d23..3b05797c858 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// GOTO Programs
+
#include
#include
@@ -64,6 +67,8 @@ class goto_checkt
void goto_check(goto_functiont &goto_function, const irep_idt &mode);
+ void collect_allocations(const goto_functionst &goto_functions);
+
protected:
const namespacet &ns;
local_bitvector_analysist *local_bitvector_analysis;
@@ -134,19 +139,43 @@ class goto_checkt
typedef optionst::value_listt error_labelst;
error_labelst error_labels;
-};
-
-/*******************************************************************\
-
-Function: goto_checkt::invalidate
- Inputs:
-
- Outputs:
+ typedef std::pair allocationt;
+ typedef std::list allocationst;
+ allocationst allocations;
+};
- Purpose:
+void goto_checkt::collect_allocations(
+ const goto_functionst &goto_functions)
+{
+ if(!enable_pointer_check)
+ return;
-\*******************************************************************/
+ forall_goto_functions(itf, goto_functions)
+ forall_goto_program_instructions(it, itf->second.body)
+ {
+ const goto_programt::instructiont &instruction=*it;
+ if(!instruction.is_function_call())
+ continue;
+
+ const code_function_callt &call=
+ to_code_function_call(instruction.code);
+ if(call.function().id()!=ID_symbol ||
+ to_symbol_expr(call.function()).get_identifier()!=
+ CPROVER_PREFIX "allocated_memory")
+ continue;
+
+ const code_function_callt::argumentst &args= call.arguments();
+ if(args.size()!=2 ||
+ args[0].type().id()!=ID_unsignedbv ||
+ args[1].type().id()!=ID_unsignedbv)
+ throw "expected two unsigned arguments to "
+ CPROVER_PREFIX "allocated_memory";
+
+ assert(args[0].type()==args[1].type());
+ allocations.push_back({args[0], args[1]});
+ }
+}
void goto_checkt::invalidate(const exprt &lhs)
{
@@ -182,18 +211,6 @@ void goto_checkt::invalidate(const exprt &lhs)
}
}
-/*******************************************************************\
-
-Function: goto_checkt::div_by_zero_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::div_by_zero_check(
const div_exprt &expr,
const guardt &guard)
@@ -220,18 +237,6 @@ void goto_checkt::div_by_zero_check(
guard);
}
-/*******************************************************************\
-
-Function: goto_checkt::undefined_shift_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::undefined_shift_check(
const shift_exprt &expr,
const guardt &guard)
@@ -283,18 +288,6 @@ void goto_checkt::undefined_shift_check(
}
}
-/*******************************************************************\
-
-Function: goto_checkt::mod_by_zero_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::mod_by_zero_check(
const mod_exprt &expr,
const guardt &guard)
@@ -321,18 +314,6 @@ void goto_checkt::mod_by_zero_check(
guard);
}
-/*******************************************************************\
-
-Function: goto_checkt::conversion_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::conversion_check(
const exprt &expr,
const guardt &guard)
@@ -512,18 +493,6 @@ void goto_checkt::conversion_check(
}
}
-/*******************************************************************\
-
-Function: goto_checkt::integer_overflow_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::integer_overflow_check(
const exprt &expr,
const guardt &guard)
@@ -645,18 +614,6 @@ void goto_checkt::integer_overflow_check(
}
}
-/*******************************************************************\
-
-Function: goto_checkt::float_overflow_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::float_overflow_check(
const exprt &expr,
const guardt &guard)
@@ -779,18 +736,6 @@ void goto_checkt::float_overflow_check(
}
}
-/*******************************************************************\
-
-Function: goto_checkt::nan_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::nan_check(
const exprt &expr,
const guardt &guard)
@@ -900,18 +845,6 @@ void goto_checkt::nan_check(
guard);
}
-/*******************************************************************\
-
-Function: goto_checkt::pointer_rel_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::pointer_rel_check(
const exprt &expr,
const guardt &guard)
@@ -942,18 +875,6 @@ void goto_checkt::pointer_rel_check(
}
}
-/*******************************************************************\
-
-Function: goto_checkt::pointer_overflow_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::pointer_overflow_check(
const exprt &expr,
const guardt &guard)
@@ -980,18 +901,6 @@ void goto_checkt::pointer_overflow_check(
}
}
-/*******************************************************************\
-
-Function: goto_checkt::pointer_validity_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::pointer_validity_check(
const dereference_exprt &expr,
const guardt &guard,
@@ -1031,10 +940,49 @@ void goto_checkt::pointer_validity_check(
}
else
{
+ exprt allocs=false_exprt();
+
+ if(!allocations.empty())
+ {
+ exprt::operandst disjuncts;
+
+ for(const auto &a : allocations)
+ {
+ typecast_exprt int_ptr(pointer, a.first.type());
+
+ exprt lb(int_ptr);
+ if(access_lb.is_not_nil())
+ {
+ if(!base_type_eq(lb.type(), access_lb.type(), ns))
+ lb=plus_exprt(lb, typecast_exprt(access_lb, lb.type()));
+ else
+ lb=plus_exprt(lb, access_lb);
+ }
+
+ binary_relation_exprt lb_check(a.first, ID_le, lb);
+
+ exprt ub(int_ptr);
+ if(access_ub.is_not_nil())
+ {
+ if(!base_type_eq(ub.type(), access_ub.type(), ns))
+ ub=plus_exprt(ub, typecast_exprt(access_ub, ub.type()));
+ else
+ ub=plus_exprt(ub, access_ub);
+ }
+
+ binary_relation_exprt ub_check(
+ ub, ID_le, plus_exprt(a.first, a.second));
+
+ disjuncts.push_back(and_exprt(lb_check, ub_check));
+ }
+
+ allocs=disjunction(disjuncts);
+ }
+
if(flags.is_unknown() || flags.is_null())
{
add_guarded_claim(
- not_exprt(null_pointer(pointer)),
+ or_exprt(allocs, not_exprt(null_pointer(pointer))),
"dereference failure: pointer NULL",
"pointer dereference",
expr.find_source_location(),
@@ -1044,7 +992,7 @@ void goto_checkt::pointer_validity_check(
if(flags.is_unknown())
add_guarded_claim(
- not_exprt(invalid_pointer(pointer)),
+ or_exprt(allocs, not_exprt(invalid_pointer(pointer))),
"dereference failure: pointer invalid",
"pointer dereference",
expr.find_source_location(),
@@ -1053,7 +1001,7 @@ void goto_checkt::pointer_validity_check(
if(flags.is_uninitialized())
add_guarded_claim(
- not_exprt(invalid_pointer(pointer)),
+ or_exprt(allocs, not_exprt(invalid_pointer(pointer))),
"dereference failure: pointer uninitialized",
"pointer dereference",
expr.find_source_location(),
@@ -1062,7 +1010,7 @@ void goto_checkt::pointer_validity_check(
if(flags.is_unknown() || flags.is_dynamic_heap())
add_guarded_claim(
- not_exprt(deallocated(pointer, ns)),
+ or_exprt(allocs, not_exprt(deallocated(pointer, ns))),
"dereference failure: deallocated dynamic object",
"pointer dereference",
expr.find_source_location(),
@@ -1071,7 +1019,7 @@ void goto_checkt::pointer_validity_check(
if(flags.is_unknown() || flags.is_dynamic_local())
add_guarded_claim(
- not_exprt(dead_object(pointer, ns)),
+ or_exprt(allocs, not_exprt(dead_object(pointer, ns))),
"dereference failure: dead object",
"pointer dereference",
expr.find_source_location(),
@@ -1089,7 +1037,11 @@ void goto_checkt::pointer_validity_check(
access_ub));
add_guarded_claim(
- implies_exprt(malloc_object(pointer, ns), not_exprt(dynamic_bounds)),
+ or_exprt(
+ allocs,
+ implies_exprt(
+ malloc_object(pointer, ns),
+ not_exprt(dynamic_bounds))),
"dereference failure: pointer outside dynamic object bounds",
"pointer dereference",
expr.find_source_location(),
@@ -1110,7 +1062,7 @@ void goto_checkt::pointer_validity_check(
access_ub));
add_guarded_claim(
- or_exprt(dynamic_object(pointer), not_exprt(object_bounds)),
+ or_exprt(allocs, dynamic_object(pointer), not_exprt(object_bounds)),
"dereference failure: pointer outside object bounds",
"pointer dereference",
expr.find_source_location(),
@@ -1120,35 +1072,11 @@ void goto_checkt::pointer_validity_check(
}
}
-/*******************************************************************\
-
-Function: goto_checkt::array_name
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
std::string goto_checkt::array_name(const exprt &expr)
{
return ::array_name(ns, expr);
}
-/*******************************************************************\
-
-Function: goto_checkt::bounds_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::bounds_check(
const index_exprt &expr,
const guardt &guard)
@@ -1238,7 +1166,8 @@ void goto_checkt::bounds_check(
plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
assert(effective_offset.op0().type()==effective_offset.op1().type());
- assert(effective_offset.type()==size.type());
+ if(effective_offset.type()!=size.type())
+ size.make_typecast(effective_offset.type());
binary_relation_exprt inequality(effective_offset, ID_lt, size);
@@ -1303,18 +1232,6 @@ void goto_checkt::bounds_check(
}
}
-/*******************************************************************\
-
-Function: goto_checkt::add_guarded_claim
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::add_guarded_claim(
const exprt &_expr,
const std::string &comment,
@@ -1362,18 +1279,6 @@ void goto_checkt::add_guarded_claim(
}
}
-/*******************************************************************\
-
-Function: goto_checkt::check_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::check_rec(
const exprt &expr,
guardt &guard,
@@ -1554,36 +1459,12 @@ void goto_checkt::check_rec(
mode);
}
-/*******************************************************************\
-
-Function: goto_checkt::check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::check(const exprt &expr, const irep_idt &mode)
{
guardt guard;
check_rec(expr, guard, false, mode);
}
-/*******************************************************************\
-
-Function: goto_checkt::goto_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_checkt::goto_check(
goto_functiont &goto_function,
const irep_idt &mode)
@@ -1808,17 +1689,17 @@ void goto_checkt::goto_check(
{
i_it->source_location.id(irep_idt());
- if(it->source_location.get_file()!=irep_idt())
+ if(!it->source_location.get_file().empty())
i_it->source_location.set_file(it->source_location.get_file());
- if(it->source_location.get_line()!=irep_idt())
+ if(!it->source_location.get_line().empty())
i_it->source_location.set_line(it->source_location.get_line());
- if(it->source_location.get_function()!=irep_idt())
+ if(!it->source_location.get_function().empty())
i_it->source_location.set_function(
it->source_location.get_function());
- if(it->source_location.get_column()!=irep_idt())
+ if(!it->source_location.get_column().empty())
i_it->source_location.set_column(it->source_location.get_column());
if(it->source_location.get_java_bytecode_index()!=irep_idt())
@@ -1826,7 +1707,7 @@ void goto_checkt::goto_check(
it->source_location.get_java_bytecode_index());
}
- if(i_it->function==irep_idt())
+ if(i_it->function.empty())
i_it->function=it->function;
}
@@ -1841,18 +1722,6 @@ void goto_checkt::goto_check(
}
}
-/*******************************************************************\
-
-Function: goto_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_check(
const namespacet &ns,
const optionst &options,
@@ -1862,18 +1731,6 @@ void goto_check(
goto_check.goto_check(goto_function, irep_idt());
}
-/*******************************************************************\
-
-Function: goto_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_check(
const namespacet &ns,
const optionst &options,
@@ -1881,6 +1738,8 @@ void goto_check(
{
goto_checkt goto_check(ns, options);
+ goto_check.collect_allocations(goto_functions);
+
Forall_goto_functions(it, goto_functions)
{
irep_idt mode=ns.lookup(it->first).mode;
@@ -1888,18 +1747,6 @@ void goto_check(
}
}
-/*******************************************************************\
-
-Function: goto_check
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_check(
const optionst &options,
goto_modelt &goto_model)
diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h
index 2089d744fd2..44d98069de9 100644
--- a/src/analyses/goto_check.h
+++ b/src/analyses/goto_check.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Program Transformation
+
#ifndef CPROVER_ANALYSES_GOTO_CHECK_H
#define CPROVER_ANALYSES_GOTO_CHECK_H
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index e5df484cb9c..73b7a8c3520 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -8,6 +8,7 @@ Date: April 2010
\*******************************************************************/
+
#include
#include
@@ -25,34 +26,10 @@ Date: April 2010
#include "goto_rw.h"
-/*******************************************************************\
-
-Function: range_domain_baset::~range_domain_baset
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
range_domain_baset::~range_domain_baset()
{
}
-/*******************************************************************\
-
-Function: range_domaint::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void range_domaint::output(
const namespacet &ns, std::ostream &out) const
{
@@ -68,18 +45,6 @@ void range_domaint::output(
out << "]";
}
-/*******************************************************************\
-
-Function: rw_range_sett::~rw_range_sett
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
rw_range_sett::~rw_range_sett()
{
for(rw_range_sett::objectst::iterator it=r_range_set.begin();
@@ -93,51 +58,27 @@ rw_range_sett::~rw_range_sett()
delete it->second;
}
-/*******************************************************************\
-
-Function: rw_range_sett::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::output(std::ostream &out) const
{
- out << "READ:" << std::endl;
+ out << "READ:\n";
forall_rw_range_set_r_objects(it, *this)
{
out << " " << it->first;
it->second->output(ns, out);
- out << std::endl;
+ out << '\n';
}
- out << std::endl;
+ out << '\n';
- out << "WRITE:" << std::endl;
+ out << "WRITE:\n";
forall_rw_range_set_w_objects(it, *this)
{
out << " " << it->first;
it->second->output(ns, out);
- out << std::endl;
+ out << '\n';
}
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_complex
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_complex(
get_modet mode,
const exprt &expr,
@@ -149,24 +90,13 @@ void rw_range_sett::get_objects_complex(
range_spect sub_size=
to_range_spect(pointer_offset_bits(op.type().subtype(), ns));
+ assert(sub_size>0);
range_spect offset=
(range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
get_objects_rec(mode, op, range_start+offset, size);
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_if
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_if(
get_modet mode,
const if_exprt &if_expr,
@@ -186,18 +116,6 @@ void rw_range_sett::get_objects_if(
}
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_dereference
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_dereference(
get_modet mode,
const dereference_exprt &deref,
@@ -210,18 +128,6 @@ void rw_range_sett::get_objects_dereference(
get_objects_rec(mode, pointer);
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_byte_extract
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_byte_extract(
get_modet mode,
const byte_extract_exprt &be,
@@ -249,18 +155,6 @@ void rw_range_sett::get_objects_byte_extract(
}
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_shift
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_shift(
get_modet mode,
const shift_exprt &shift,
@@ -309,18 +203,6 @@ void rw_range_sett::get_objects_shift(
}
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_member
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_member(
get_modet mode,
const member_exprt &expr,
@@ -351,18 +233,6 @@ void rw_range_sett::get_objects_member(
get_objects_rec(mode, expr.struct_op(), offset, size);
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_index
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_index(
get_modet mode,
const index_exprt &expr,
@@ -411,18 +281,6 @@ void rw_range_sett::get_objects_index(
size);
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_array
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_array(
get_modet mode,
const array_exprt &expr,
@@ -463,18 +321,6 @@ void rw_range_sett::get_objects_array(
}
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_struct
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_struct(
get_modet mode,
const struct_exprt &expr,
@@ -535,18 +381,6 @@ void rw_range_sett::get_objects_struct(
}
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_typecast
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_typecast(
get_modet mode,
const typecast_exprt &tc,
@@ -572,18 +406,6 @@ void rw_range_sett::get_objects_typecast(
get_objects_rec(mode, op, range_start, new_size);
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_address_of
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_address_of(const exprt &object)
{
if(object.id()==ID_string_constant ||
@@ -634,18 +456,6 @@ void rw_range_sett::get_objects_address_of(const exprt &object)
throw "rw_range_sett: address_of `"+object.id_string()+"' not handled";
}
-/*******************************************************************\
-
-Function: rw_range_sett::add
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::add(
get_modet mode,
const irep_idt &identifier,
@@ -663,18 +473,6 @@ void rw_range_sett::add(
std::make_pair(range_start, range_end));
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_rec(
get_modet mode,
const exprt &expr,
@@ -766,18 +564,6 @@ void rw_range_sett::get_objects_rec(
throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_rec(get_modet mode, const exprt &expr)
{
range_spect size=
@@ -785,18 +571,6 @@ void rw_range_sett::get_objects_rec(get_modet mode, const exprt &expr)
get_objects_rec(mode, expr, 0, size);
}
-/*******************************************************************\
-
-Function: rw_range_sett::get_objects_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_sett::get_objects_rec(const typet &type)
{
// TODO should recurse into various composite types
@@ -807,18 +581,6 @@ void rw_range_sett::get_objects_rec(const typet &type)
}
}
-/*******************************************************************\
-
-Function: rw_range_set_value_sett::get_objects_dereference
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_range_set_value_sett::get_objects_dereference(
get_modet mode,
const dereference_exprt &deref,
@@ -852,18 +614,6 @@ void rw_range_set_value_sett::get_objects_dereference(
get_objects_rec(mode, object, range_start, new_size);
}
-/*******************************************************************\
-
-Function: guarded_range_domaint::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void guarded_range_domaint::output(
const namespacet &ns, std::ostream &out) const
{
@@ -880,18 +630,6 @@ void guarded_range_domaint::output(
out << "]";
}
-/*******************************************************************\
-
-Function: rw_guarded_range_set_value_sett::get_objects_if
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_guarded_range_set_value_sett::get_objects_if(
get_modet mode,
const if_exprt &if_expr,
@@ -918,18 +656,6 @@ void rw_guarded_range_set_value_sett::get_objects_if(
}
}
-/*******************************************************************\
-
-Function: rw_guarded_range_set_value_sett::add
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rw_guarded_range_set_value_sett::add(
get_modet mode,
const irep_idt &identifier,
@@ -948,18 +674,6 @@ void rw_guarded_range_set_value_sett::add(
std::make_pair(range_end, guard.as_expr())));
}
-/*******************************************************************\
-
-Function: goto_rw
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_rw(goto_programt::const_targett target,
const code_assignt &assign,
rw_range_sett &rw_set)
@@ -968,18 +682,6 @@ void goto_rw(goto_programt::const_targett target,
rw_set.get_objects_rec(target, rw_range_sett::get_modet::READ, assign.rhs());
}
-/*******************************************************************\
-
-Function: goto_rw
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_rw(goto_programt::const_targett target,
const code_function_callt &function_call,
rw_range_sett &rw_set)
@@ -999,18 +701,6 @@ void goto_rw(goto_programt::const_targett target,
rw_set.get_objects_rec(target, rw_range_sett::get_modet::READ, *it);
}
-/*******************************************************************\
-
-Function: goto_rw
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_rw(goto_programt::const_targett target,
rw_range_sett &rw_set)
{
@@ -1088,36 +778,12 @@ void goto_rw(goto_programt::const_targett target,
}
}
-/*******************************************************************\
-
-Function: goto_rw
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_rw(const goto_programt &goto_program, rw_range_sett &rw_set)
{
forall_goto_program_instructions(i_it, goto_program)
goto_rw(i_it, rw_set);
}
-/*******************************************************************\
-
-Function: goto_rw
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void goto_rw(const goto_functionst &goto_functions,
const irep_idt &function,
rw_range_sett &rw_set)
diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
index 2e826da7728..06b7a7ab411 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -8,6 +8,7 @@ Date: April 2010
\*******************************************************************/
+
#ifndef CPROVER_ANALYSES_GOTO_RW_H
#define CPROVER_ANALYSES_GOTO_RW_H
diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp
index 17c3dd68562..d81d857b1f8 100644
--- a/src/analyses/interval_analysis.cpp
+++ b/src/analyses/interval_analysis.cpp
@@ -6,23 +6,14 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Interval Analysis
+
#include
#include "interval_domain.h"
#include "interval_analysis.h"
-/*******************************************************************\
-
-Function: instrument_intervals
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void instrument_intervals(
const ait &interval_analysis,
goto_functionst::goto_functiont &goto_function)
@@ -84,18 +75,6 @@ void instrument_intervals(
}
}
-/*******************************************************************\
-
-Function: interval_analysis
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void interval_analysis(
const namespacet &ns,
goto_functionst &goto_functions)
diff --git a/src/analyses/interval_analysis.h b/src/analyses/interval_analysis.h
index be86a6c65f8..1c85fc9a193 100644
--- a/src/analyses/interval_analysis.h
+++ b/src/analyses/interval_analysis.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Interval Analysis
+
#ifndef CPROVER_ANALYSES_INTERVAL_ANALYSIS_H
#define CPROVER_ANALYSES_INTERVAL_ANALYSIS_H
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 1faf8c52364..6dc4fd37fab 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Interval Domain
+
#ifdef DEBUG
#include
#endif
@@ -16,18 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "interval_domain.h"
-/*******************************************************************\
-
-Function: interval_domaint::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void interval_domaint::output(
std::ostream &out,
const ai_baset &ai,
@@ -64,18 +55,6 @@ void interval_domaint::output(
}
}
-/*******************************************************************\
-
-Function: interval_domaint::transform
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void interval_domaint::transform(
locationt from,
locationt to,
@@ -127,22 +106,20 @@ void interval_domaint::transform(
}
}
-/*******************************************************************\
-
-Function: interval_domaint::merge
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-bool interval_domaint::merge(
- const interval_domaint &b,
- locationt from,
- locationt to)
+/// Sets *this to the mathematical join between the two domains. This can be
+/// thought of as an abstract version of union; *this is increased so that it
+/// contains all of the values that are represented by b as well as its original
+/// intervals. The result is an overapproximation, for example:
+/// "[0,1]".join("[3,4]") --> "[0,4]" includes 2 which isn't in [0,1] or [3,4].
+///
+/// Join is used in several places, the most significant being
+/// merge, which uses it to bring together two different paths
+/// of analysis.
+/// \par parameters: The interval domain, b, to join to this domain.
+/// \return True if the join increases the set represented by *this, False if
+/// there is no change.
+bool interval_domaint::join(
+ const interval_domaint &b)
{
if(b.bottom)
return false;
@@ -157,8 +134,8 @@ bool interval_domaint::merge(
for(int_mapt::iterator it=int_map.begin();
it!=int_map.end(); ) // no it++
{
- //search for the variable that needs to be merged
- //containers have different size and variable order
+ // search for the variable that needs to be merged
+ // containers have different size and variable order
const int_mapt::const_iterator b_it=b.int_map.find(it->first);
if(b_it==b.int_map.end())
{
@@ -199,36 +176,12 @@ bool interval_domaint::merge(
return result;
}
-/*******************************************************************\
-
-Function: interval_domaint::assign
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void interval_domaint::assign(const code_assignt &code_assign)
{
havoc_rec(code_assign.lhs());
assume_rec(code_assign.lhs(), ID_equal, code_assign.rhs());
}
-/*******************************************************************\
-
-Function: interval_domaint::havoc_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void interval_domaint::havoc_rec(const exprt &lhs)
{
if(lhs.id()==ID_if)
@@ -251,18 +204,6 @@ void interval_domaint::havoc_rec(const exprt &lhs)
}
}
-/*******************************************************************\
-
-Function: interval_domaint::assume_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void interval_domaint::assume_rec(
const exprt &lhs, irep_idt id, const exprt &rhs)
{
@@ -377,18 +318,6 @@ void interval_domaint::assume_rec(
}
}
-/*******************************************************************\
-
-Function: interval_domaint::assume_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void interval_domaint::assume(
const exprt &cond,
const namespacet &ns)
@@ -396,18 +325,6 @@ void interval_domaint::assume(
assume_rec(simplify_expr(cond, ns), false);
}
-/*******************************************************************\
-
-Function: interval_domaint::assume_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void interval_domaint::assume_rec(
const exprt &cond,
bool negation)
@@ -454,18 +371,6 @@ void interval_domaint::assume_rec(
}
}
-/*******************************************************************\
-
-Function: interval_domaint::make_expression
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt interval_domaint::make_expression(const symbol_exprt &src) const
{
if(is_int(src.type()))
@@ -527,3 +432,58 @@ exprt interval_domaint::make_expression(const symbol_exprt &src) const
else
return true_exprt();
}
+
+/// Uses the abstract state to simplify a given expression using context-
+/// specific information.
+/// \par parameters: The expression to simplify.
+/// \return A simplified version of the expression.
+/*
+ * This implementation is aimed at reducing assertions to true, particularly
+ * range checks for arrays and other bounds checks.
+ *
+ * Rather than work with the various kinds of exprt directly, we use assume,
+ * join and is_bottom. It is sufficient for the use case and avoids duplicating
+ * functionality that is in assume anyway.
+ *
+ * As some expressions (1<=a && a<=2) can be represented exactly as intervals
+ * and some can't (a<1 || a>2), the way these operations are used varies
+ * depending on the structure of the expression to try to give the best results.
+ * For example negating a disjunction makes it easier for assume to handle.
+ */
+
+bool interval_domaint::ai_simplify(
+ exprt &condition,
+ const namespacet &ns) const
+{
+ bool unchanged=true;
+ interval_domaint d(*this);
+
+ // merge intervals to properly handle conjunction
+ if(condition.id()==ID_and) // May be directly representable
+ {
+ interval_domaint a;
+ a.make_top(); // a is everything
+ a.assume(condition, ns); // Restrict a to an over-approximation
+ // of when condition is true
+ if(!a.join(d)) // If d (this) is included in a...
+ { // Then the condition is always true
+ unchanged=condition.is_true();
+ condition.make_true();
+ }
+ }
+ else if(condition.id()==ID_symbol)
+ {
+ // TODO: we have to handle symbol expression
+ }
+ else // Less likely to be representable
+ {
+ d.assume(not_exprt(condition), ns); // Restrict to when condition is false
+ if(d.is_bottom()) // If there there are none...
+ { // Then the condition is always true
+ unchanged=condition.is_true();
+ condition.make_true();
+ }
+ }
+
+ return unchanged;
+}
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index 7e95c65e9de..3076442a3ee 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Interval Domain
+
#ifndef CPROVER_ANALYSES_INTERVAL_DOMAIN_H
#define CPROVER_ANALYSES_INTERVAL_DOMAIN_H
@@ -40,10 +43,17 @@ class interval_domaint:public ai_domain_baset
const ai_baset &ai,
const namespacet &ns) const final;
+protected:
+ bool join(const interval_domaint &b);
+
+public:
bool merge(
const interval_domaint &b,
locationt from,
- locationt to);
+ locationt to)
+ {
+ return join(b);
+ }
// no states
void make_bottom() final
@@ -85,7 +95,11 @@ class interval_domaint:public ai_domain_baset
return bottom;
}
-private:
+ virtual bool ai_simplify(
+ exprt &condition,
+ const namespacet &ns) const override;
+
+protected:
bool bottom;
typedef std::map int_mapt;
diff --git a/src/analyses/interval_template.h b/src/analyses/interval_template.h
index f59d1da1f8f..b06013af53e 100644
--- a/src/analyses/interval_template.h
+++ b/src/analyses/interval_template.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANALYSES_INTERVAL_TEMPLATE_H
#define CPROVER_ANALYSES_INTERVAL_TEMPLATE_H
diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp
index 2da2d7278f4..8e93ce4ee17 100644
--- a/src/analyses/invariant_propagation.cpp
+++ b/src/analyses/invariant_propagation.cpp
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Invariant Propagation
+
#include
#include
#include
@@ -13,54 +16,18 @@ Author: Daniel Kroening, kroening@kroening.com
#include "invariant_propagation.h"
-/*******************************************************************\
-
-Function: invariant_propagationt::make_all_true
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_propagationt::make_all_true()
{
for(auto &state : state_map)
state.second.invariant_set.make_true();
}
-/*******************************************************************\
-
-Function: invariant_propagationt::make_all_false
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_propagationt::make_all_false()
{
for(auto &state : state_map)
state.second.invariant_set.make_false();
}
-/*******************************************************************\
-
-Function: invariant_propagationt::add_objects
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_propagationt::add_objects(
const goto_programt &goto_program)
{
@@ -108,18 +75,6 @@ void invariant_propagationt::add_objects(
}
}
-/*******************************************************************\
-
-Function: invariant_propagationt::get_objects
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_propagationt::get_objects(
const symbolt &symbol,
object_listt &dest)
@@ -132,18 +87,6 @@ void invariant_propagationt::get_objects(
dest.push_back(object_store.add(expr));
}
-/*******************************************************************\
-
-Function: invariant_propagationt::get_objects_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_propagationt::get_objects_rec(
const exprt &src,
std::list &dest)
@@ -179,18 +122,6 @@ void invariant_propagationt::get_objects_rec(
}
}
-/*******************************************************************\
-
-Function: invariant_propagationt::add_vars
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_propagationt::add_objects(
const goto_functionst &goto_functions)
{
@@ -243,18 +174,6 @@ void invariant_propagationt::add_objects(
}
}
-/*******************************************************************\
-
-Function: invariant_propagationt::get_globals
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_propagationt::get_globals(
object_listt &dest)
{
@@ -265,18 +184,6 @@ void invariant_propagationt::get_globals(
get_objects(it->second, dest);
}
-/*******************************************************************\
-
-Function: invariant_propagationt::check_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool invariant_propagationt::check_type(const typet &type) const
{
if(type.id()==ID_pointer)
@@ -297,18 +204,6 @@ bool invariant_propagationt::check_type(const typet &type) const
return false;
}
-/*******************************************************************\
-
-Function: invariant_propagationt::initialize
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_propagationt::initialize(const goto_programt &goto_program)
{
baset::initialize(goto_program);
@@ -330,18 +225,6 @@ void invariant_propagationt::initialize(const goto_programt &goto_program)
add_objects(goto_program);
}
-/*******************************************************************\
-
-Function: invariant_propagationt::initialize
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_propagationt::initialize(const goto_functionst &goto_functions)
{
baset::initialize(goto_functions);
@@ -350,36 +233,12 @@ void invariant_propagationt::initialize(const goto_functionst &goto_functions)
initialize(f_it->second.body);
}
-/*******************************************************************\
-
-Function: invariant_propagationt::simplify
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_propagationt::simplify(goto_functionst &goto_functions)
{
Forall_goto_functions(it, goto_functions)
simplify(it->second.body);
}
-/*******************************************************************\
-
-Function: invariant_propagationt::simplify
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_propagationt::simplify(goto_programt &goto_program)
{
Forall_goto_program_instructions(i_it, goto_program)
diff --git a/src/analyses/invariant_propagation.h b/src/analyses/invariant_propagation.h
index 0884ba85d07..d21f6373bcb 100644
--- a/src/analyses/invariant_propagation.h
+++ b/src/analyses/invariant_propagation.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Invariant Propagation
+
#ifndef CPROVER_ANALYSES_INVARIANT_PROPAGATION_H
#define CPROVER_ANALYSES_INVARIANT_PROPAGATION_H
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
index 15c350f0e0f..425842a86f9 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Invariant Set
+
#include
#include
@@ -16,41 +19,17 @@ Author: Daniel Kroening, kroening@kroening.com
#include
#include
-#include
+#include
#include
#include "invariant_set.h"
-/*******************************************************************\
-
-Function: inv_object_storet::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void inv_object_storet::output(std::ostream &out) const
{
for(unsigned i=0; iget(expr, n);
}
-/*******************************************************************\
-
-Function: inv_object_storet::is_constant_address
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool inv_object_storet::is_constant_address(const exprt &expr)
{
if(expr.id()==ID_address_of)
@@ -250,18 +157,6 @@ bool inv_object_storet::is_constant_address(const exprt &expr)
return false;
}
-/*******************************************************************\
-
-Function: inv_object_storet::is_constant_address_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool inv_object_storet::is_constant_address_rec(const exprt &expr)
{
if(expr.id()==ID_symbol)
@@ -281,18 +176,6 @@ bool inv_object_storet::is_constant_address_rec(const exprt &expr)
return false;
}
-/*******************************************************************\
-
-Function: invariant_sett::add
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::add(
const std::pair &p,
ineq_sett &dest)
@@ -315,18 +198,6 @@ void invariant_sett::add(
}
}
-/*******************************************************************\
-
-Function: invariant_sett::add_eq
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::add_eq(const std::pair &p)
{
eq_set.make_union(p.first, p.second);
@@ -364,18 +235,6 @@ void invariant_sett::add_eq(const std::pair &p)
add_eq(ne_set, p, ne);
}
-/*******************************************************************\
-
-Function: invariant_sett::add_eq
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::add_eq(
ineq_sett &dest,
const std::pair &eq,
@@ -414,18 +273,6 @@ void invariant_sett::add_eq(
}
}
-/*******************************************************************\
-
-Function: invariant_sett::is_eq
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
tvt invariant_sett::is_eq(std::pair p) const
{
std::pair s=p;
@@ -440,18 +287,6 @@ tvt invariant_sett::is_eq(std::pair p) const
return tvt::unknown();
}
-/*******************************************************************\
-
-Function: invariant_sett::is_le
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
tvt invariant_sett::is_le(std::pair p) const
{
std::pair s=p;
@@ -470,25 +305,13 @@ tvt invariant_sett::is_le(std::pair p) const
return tvt::unknown();
}
-/*******************************************************************\
-
-Function: invariant_sett::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::output(
const irep_idt &identifier,
std::ostream &out) const
{
if(is_false)
{
- out << "FALSE" << std::endl;
+ out << "FALSE\n";
return;
}
@@ -510,43 +333,31 @@ void invariant_sett::output(
out << to_string(j, identifier);
}
- out << std::endl;
+ out << '\n';
}
for(const auto &bounds : bounds_map)
{
out << to_string(bounds.first, identifier)
<< " in " << bounds.second
- << std::endl;
+ << '\n';
}
for(const auto &le : le_set)
{
out << to_string(le.first, identifier)
<< " <= " << to_string(le.second, identifier)
- << std::endl;
+ << '\n';
}
for(const auto &ne : ne_set)
{
out << to_string(ne.first, identifier)
<< " != " << to_string(ne.second, identifier)
- << std::endl;
+ << '\n';
}
}
-/*******************************************************************\
-
-Function: invariant_sett::strengthen
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::add_type_bounds(const exprt &expr, const typet &type)
{
if(expr.type()==type)
@@ -567,18 +378,6 @@ void invariant_sett::add_type_bounds(const exprt &expr, const typet &type)
}
}
-/*******************************************************************\
-
-Function: invariant_sett::strengthen
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::strengthen(const exprt &expr)
{
exprt tmp(expr);
@@ -586,25 +385,13 @@ void invariant_sett::strengthen(const exprt &expr)
strengthen_rec(tmp);
}
-/*******************************************************************\
-
-Function: invariant_sett::strengthen_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::strengthen_rec(const exprt &expr)
{
if(expr.type().id()!=ID_bool)
throw "non-Boolean argument to strengthen()";
#if 0
- std::cout << "S: " << from_expr(*ns, "", expr) << std::endl;
+ std::cout << "S: " << from_expr(*ns, "", expr) << '\n';
#endif
if(is_false)
@@ -799,18 +586,6 @@ void invariant_sett::strengthen_rec(const exprt &expr)
}
}
-/*******************************************************************\
-
-Function: invariant_sett::implies
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
tvt invariant_sett::implies(const exprt &expr) const
{
exprt tmp(expr);
@@ -818,25 +593,13 @@ tvt invariant_sett::implies(const exprt &expr) const
return implies_rec(tmp);
}
-/*******************************************************************\
-
-Function: invariant_sett::implies
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
tvt invariant_sett::implies_rec(const exprt &expr) const
{
if(expr.type().id()!=ID_bool)
throw "implies: non-Boolean expression";
#if 0
- std::cout << "I: " << from_expr(*ns, "", expr) << std::endl;
+ std::cout << "I: " << from_expr(*ns, "", expr) << '\n';
#endif
if(is_false) // can't get any stronger
@@ -914,18 +677,6 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
return tvt::unknown();
}
-/*******************************************************************\
-
-Function: invariant_sett::get_bounds
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::get_bounds(unsigned a, boundst &bounds) const
{
// unbounded
@@ -950,18 +701,6 @@ void invariant_sett::get_bounds(unsigned a, boundst &bounds) const
bounds=it->second;
}
-/*******************************************************************\
-
-Function: invariant_sett::nnf
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::nnf(exprt &expr, bool negate)
{
if(expr.type().id()!=ID_bool)
@@ -1075,18 +814,6 @@ void invariant_sett::nnf(exprt &expr, bool negate)
}
}
-/*******************************************************************\
-
-Function: invariant_sett::simplify
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::simplify(
exprt &expr) const
{
@@ -1105,18 +832,6 @@ void invariant_sett::simplify(
}
}
-/*******************************************************************\
-
-Function: invariant_sett::get_constant
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt invariant_sett::get_constant(const exprt &expr) const
{
unsigned a;
@@ -1172,18 +887,6 @@ exprt invariant_sett::get_constant(const exprt &expr) const
return static_cast(get_nil_irep());
}
-/*******************************************************************\
-
-Function: inv_object_storet::to_string
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
std::string inv_object_storet::to_string(
unsigned a,
const irep_idt &identifier) const
@@ -1192,18 +895,6 @@ std::string inv_object_storet::to_string(
return id2string(map[a]);
}
-/*******************************************************************\
-
-Function: invariant_sett::to_string
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
std::string invariant_sett::to_string(
unsigned a,
const irep_idt &identifier) const
@@ -1212,18 +903,6 @@ std::string invariant_sett::to_string(
return object_store->to_string(a, identifier);
}
-/*******************************************************************\
-
-Function: invariant_sett::make_union
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool invariant_sett::make_union(const invariant_sett &other)
{
if(other.threaded &&
@@ -1275,18 +954,6 @@ bool invariant_sett::make_union(const invariant_sett &other)
return false; // no change
}
-/*******************************************************************\
-
-Function: invariant_sett::make_union_bounds_map
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool invariant_sett::make_union_bounds_map(const bounds_mapt &other)
{
bool changed=false;
@@ -1319,18 +986,6 @@ bool invariant_sett::make_union_bounds_map(const bounds_mapt &other)
return changed;
}
-/*******************************************************************\
-
-Function: invariant_sett::modifies
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::modifies(unsigned a)
{
eq_set.isolate(a);
@@ -1339,18 +994,6 @@ void invariant_sett::modifies(unsigned a)
bounds_map.erase(a);
}
-/*******************************************************************\
-
-Function: invariant_sett::modifies
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::modifies(const exprt &lhs)
{
if(lhs.id()==ID_symbol ||
@@ -1411,18 +1054,6 @@ void invariant_sett::modifies(const exprt &lhs)
throw "modifies: unexpected lhs: "+lhs.id_string();
}
-/*******************************************************************\
-
-Function: invariant_sett::assignment
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::assignment(
const exprt &lhs,
const exprt &rhs)
@@ -1442,18 +1073,6 @@ void invariant_sett::assignment(
strengthen(equality);
}
-/*******************************************************************\
-
-Function: invariant_sett::apply_code
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_sett::apply_code(const codet &code)
{
const irep_idt &statement=code.get(ID_statement);
@@ -1508,7 +1127,7 @@ void invariant_sett::apply_code(const codet &code)
}
else
{
- std::cerr << code.pretty() << std::endl;
+ std::cerr << code.pretty() << '\n';
throw "invariant_sett: unexpected statement: "+id2string(statement);
}
}
diff --git a/src/analyses/invariant_set.h b/src/analyses/invariant_set.h
index d5f0a31003c..6def40f54a8 100644
--- a/src/analyses/invariant_set.h
+++ b/src/analyses/invariant_set.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Value Set
+
#ifndef CPROVER_ANALYSES_INVARIANT_SET_H
#define CPROVER_ANALYSES_INVARIANT_SET_H
diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp
index 5f8512c55b5..6dec2f9ff70 100644
--- a/src/analyses/invariant_set_domain.cpp
+++ b/src/analyses/invariant_set_domain.cpp
@@ -6,22 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Invariant Set Domain
+
#include
#include "invariant_set_domain.h"
-/*******************************************************************\
-
-Function: invariant_set_domaint::transform
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void invariant_set_domaint::transform(
locationt from_l,
locationt to_l,
diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h
index 2e231524cbb..4d38b6b2657 100644
--- a/src/analyses/invariant_set_domain.h
+++ b/src/analyses/invariant_set_domain.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Value Set
+
#ifndef CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
#define CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index 905cd6b91ac..64b1e48f959 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -8,6 +8,9 @@ Date: October 2012
\*******************************************************************/
+/// \file
+/// Over-approximate Concurrency for Threaded Goto Programs
+
#include "ai.h"
#include "is_threaded.h"
@@ -78,18 +81,6 @@ class is_threaded_domaint:public ai_domain_baset
}
};
-/*******************************************************************\
-
-Function: is_threadedt::compute
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void is_threadedt::compute(const goto_functionst &goto_functions)
{
// the analysis doesn't actually use the namespace, fake one
diff --git a/src/analyses/is_threaded.h b/src/analyses/is_threaded.h
index 738857b8b8a..5a3823b867e 100644
--- a/src/analyses/is_threaded.h
+++ b/src/analyses/is_threaded.h
@@ -8,6 +8,9 @@ Date: October 2012
\*******************************************************************/
+/// \file
+/// Over-approximate Concurrency for Threaded Goto Programs
+
#ifndef CPROVER_ANALYSES_IS_THREADED_H
#define CPROVER_ANALYSES_IS_THREADED_H
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index 3fc0d10bb09..219d446eea2 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Field-insensitive, location-sensitive may-alias analysis
+
#include
#include
@@ -13,23 +16,11 @@ Author: Daniel Kroening, kroening@kroening.com
#include
#include
-#include
+#include
#include
#include "local_bitvector_analysis.h"
-/*******************************************************************\
-
-Function: local_bitvector_analysist::flagst::print
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void local_bitvector_analysist::flagst::print(std::ostream &out) const
{
if(is_unknown())
@@ -50,18 +41,6 @@ void local_bitvector_analysist::flagst::print(std::ostream &out) const
out << "+integer_address";
}
-/*******************************************************************\
-
-Function: local_bitvector_analysist::loc_infot::merge
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool local_bitvector_analysist::loc_infot::merge(const loc_infot &src)
{
bool result=false;
@@ -78,19 +57,7 @@ bool local_bitvector_analysist::loc_infot::merge(const loc_infot &src)
return result;
}
-/*******************************************************************\
-
-Function: local_bitvector_analysist::is_tracked
-
- Inputs:
-
- Outputs: return 'true' iff we track the object with given
- identifier
-
- Purpose:
-
-\*******************************************************************/
-
+/// \return return 'true' iff we track the object with given identifier
bool local_bitvector_analysist::is_tracked(const irep_idt &identifier)
{
localst::locals_mapt::const_iterator it=locals.locals_map.find(identifier);
@@ -102,18 +69,6 @@ bool local_bitvector_analysist::is_tracked(const irep_idt &identifier)
return true;
}
-/*******************************************************************\
-
-Function: local_bitvector_analysist::assign_lhs
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void local_bitvector_analysist::assign_lhs(
const exprt &lhs,
const exprt &rhs,
@@ -154,18 +109,6 @@ void local_bitvector_analysist::assign_lhs(
}
}
-/*******************************************************************\
-
-Function: local_bitvector_analysist::get
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
local_bitvector_analysist::flagst local_bitvector_analysist::get(
const goto_programt::const_targett t,
const exprt &rhs)
@@ -179,18 +122,6 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get(
return get_rec(rhs, loc_info_src);
}
-/*******************************************************************\
-
-Function: local_bitvector_analysist::get_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
const exprt &rhs,
const loc_infot &loc_info_src)
@@ -312,18 +243,6 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
return flagst::mk_unknown();
}
-/*******************************************************************\
-
-Function: local_bitvector_analysist::build
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void local_bitvector_analysist::build(const goto_functiont &goto_function)
{
if(cfg.nodes.empty())
@@ -400,24 +319,13 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
for(const auto &succ : node.successors)
{
+ assert(succ
#include
@@ -14,25 +17,13 @@ Author: Daniel Kroening, kroening@kroening.com
#include
#include
-#include
+#include
#include
#endif
#include "local_cfg.h"
-/*******************************************************************\
-
-Function: local_cfgt::build
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void local_cfgt::build(const goto_programt &goto_program)
{
nodes.resize(goto_program.instructions.size());
diff --git a/src/analyses/local_cfg.h b/src/analyses/local_cfg.h
index a0187be8177..d2e53cfdab0 100644
--- a/src/analyses/local_cfg.h
+++ b/src/analyses/local_cfg.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// CFG for One Function
+
#ifndef CPROVER_ANALYSES_LOCAL_CFG_H
#define CPROVER_ANALYSES_LOCAL_CFG_H
@@ -13,14 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include
-/*******************************************************************\
-
- Class: local_cfgt
-
- Purpose:
-
-\*******************************************************************/
-
class local_cfgt
{
public:
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index ffaefe73667..02a5c698186 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Field-insensitive, location-sensitive may-alias analysis
+
#include
#include
@@ -13,23 +16,12 @@ Author: Daniel Kroening, kroening@kroening.com
#include
#include
-#include
+#include
#include
#include "local_may_alias.h"
-/*******************************************************************\
-
-Function: local_may_aliast::loc_infot::merge
-
- Inputs:
-
- Outputs: return 'true' iff changed
-
- Purpose:
-
-\*******************************************************************/
-
+/// \return return 'true' iff changed
bool local_may_aliast::loc_infot::merge(const loc_infot &src)
{
bool changed=false;
@@ -49,18 +41,6 @@ bool local_may_aliast::loc_infot::merge(const loc_infot &src)
return changed;
}
-/*******************************************************************\
-
-Function: local_may_aliast::assign_lhs
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void local_may_aliast::assign_lhs(
const exprt &lhs,
const exprt &rhs,
@@ -132,18 +112,6 @@ void local_may_aliast::assign_lhs(
}
}
-/*******************************************************************\
-
-Function: local_may_aliast::get
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
std::set local_may_aliast::get(
const goto_programt::const_targett t,
const exprt &rhs) const
@@ -170,18 +138,6 @@ std::set local_may_aliast::get(
return result;
}
-/*******************************************************************\
-
-Function: local_may_aliast::aliases
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool local_may_aliast::aliases(
const goto_programt::const_targett t,
const exprt &src1, const exprt &src2) const
@@ -210,18 +166,6 @@ bool local_may_aliast::aliases(
return !result.empty();
}
-/*******************************************************************\
-
-Function: local_may_aliast::get_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void local_may_aliast::get_rec(
object_sett &dest,
const exprt &rhs,
@@ -369,18 +313,6 @@ void local_may_aliast::get_rec(
dest.insert(unknown_object);
}
-/*******************************************************************\
-
-Function: local_may_aliast::build
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void local_may_aliast::build(const goto_functiont &goto_function)
{
if(cfg.nodes.empty())
@@ -502,18 +434,6 @@ void local_may_aliast::build(const goto_functiont &goto_function)
}
}
-/*******************************************************************\
-
-Function: local_may_aliast::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void local_may_aliast::output(
std::ostream &out,
const goto_functiont &goto_function,
diff --git a/src/analyses/local_may_alias.h b/src/analyses/local_may_alias.h
index 109ca2b5e19..b54cf4e9e88 100644
--- a/src/analyses/local_may_alias.h
+++ b/src/analyses/local_may_alias.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Field-insensitive, location-sensitive may-alias analysis
+
#ifndef CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
#define CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
@@ -18,14 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "dirty.h"
#include "local_cfg.h"
-/*******************************************************************\
-
- Class: local_may_aliast
-
- Purpose:
-
-\*******************************************************************/
-
class local_may_aliast
{
public:
diff --git a/src/analyses/locals.cpp b/src/analyses/locals.cpp
index 7f30c1c008b..09d7ebfe7c3 100644
--- a/src/analyses/locals.cpp
+++ b/src/analyses/locals.cpp
@@ -8,22 +8,13 @@ Date: March 2013
\*******************************************************************/
+/// \file
+/// Local variables
+
#include
#include "locals.h"
-/*******************************************************************\
-
-Function: localst::build
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void localst::build(const goto_functiont &goto_function)
{
forall_goto_program_instructions(it, goto_function.body)
@@ -39,18 +30,6 @@ void localst::build(const goto_functiont &goto_function)
symbol_exprt(param.get_identifier(), param.type());
}
-/*******************************************************************\
-
-Function: localst::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void localst::output(std::ostream &out) const
{
for(const auto &local : locals_map)
diff --git a/src/analyses/locals.h b/src/analyses/locals.h
index 3cd52254c41..c9c59aaf340 100644
--- a/src/analyses/locals.h
+++ b/src/analyses/locals.h
@@ -8,6 +8,9 @@ Date: March 2013
\*******************************************************************/
+/// \file
+/// Local variables whose address is taken
+
#ifndef CPROVER_ANALYSES_LOCALS_H
#define CPROVER_ANALYSES_LOCALS_H
diff --git a/src/analyses/natural_loops.cpp b/src/analyses/natural_loops.cpp
index 593fc78006d..57e835d7efe 100644
--- a/src/analyses/natural_loops.cpp
+++ b/src/analyses/natural_loops.cpp
@@ -6,32 +6,23 @@ Author: Georg Weissenbacher, georg@weissenbacher.name
\*******************************************************************/
+/// \file
+/// Dominators
+
#include
#include "natural_loops.h"
-/*******************************************************************\
-
-Function: show_natural_loops
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void show_natural_loops(const goto_functionst &goto_functions)
{
forall_goto_functions(it, goto_functions)
{
- std::cout << "*** " << it->first << std::endl;
+ std::cout << "*** " << it->first << '\n';
natural_loopst natural_loops;
natural_loops(it->second.body);
natural_loops.output(std::cout);
- std::cout << std::endl;
+ std::cout << '\n';
}
}
diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h
index ff56c687c93..ce27a306882 100644
--- a/src/analyses/natural_loops.h
+++ b/src/analyses/natural_loops.h
@@ -6,6 +6,9 @@ Author: Georg Weissenbacher, georg@weissenbacher.name
\*******************************************************************/
+/// \file
+/// Compute natural loops in a goto_function
+
#ifndef CPROVER_ANALYSES_NATURAL_LOOPS_H
#define CPROVER_ANALYSES_NATURAL_LOOPS_H
@@ -69,18 +72,7 @@ typedef natural_loops_templatet
void show_natural_loops(const goto_functionst &goto_functions);
-/*******************************************************************\
-
-Function: natural_loops_templatet::compute
-
- Inputs:
-
- Outputs:
-
- Purpose: Finds all back-edges and computes the natural loops
-
-\*******************************************************************/
-
+/// Finds all back-edges and computes the natural loops
#ifdef DEBUG
#include
#endif
@@ -123,19 +115,7 @@ void natural_loops_templatet::compute(P &program)
}
}
-/*******************************************************************\
-
-Function: natural_loops_templatet::compute_natural_loop
-
- Inputs:
-
- Outputs:
-
- Purpose: Computes the natural loop for a given back-edge
- (see Muchnick section 7.4)
-
-\*******************************************************************/
-
+/// Computes the natural loop for a given back-edge (see Muchnick section 7.4)
template
void natural_loops_templatet::compute_natural_loop(T m, T n)
{
@@ -170,18 +150,7 @@ void natural_loops_templatet
::compute_natural_loop(T m, T n)
}
}
-/*******************************************************************\
-
-Function: natural_loops_templatet::output
-
- Inputs:
-
- Outputs:
-
- Purpose: Print all natural loops that were found
-
-\*******************************************************************/
-
+/// Print all natural loops that were found
template
void natural_loops_templatet::output(std::ostream &out) const
{
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index 81c3c1c5069..70ea10b79ca 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -9,6 +9,10 @@ Date: February 2013
\*******************************************************************/
+/// \file
+/// Range-based reaching definitions analysis (following Field- Sensitive
+/// Program Dependence Analysis, Litvak et al., FSE 2010)
+
#include
#include
@@ -19,18 +23,6 @@ Date: February 2013
#include "reaching_definitions.h"
-/*******************************************************************\
-
-Function: rd_range_domaint::populate_cache
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rd_range_domaint::populate_cache(const irep_idt &identifier) const
{
assert(bv_container);
@@ -51,18 +43,6 @@ void rd_range_domaint::populate_cache(const irep_idt &identifier) const
}
}
-/*******************************************************************\
-
-Function: rd_range_domaint::transform
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rd_range_domaint::transform(
locationt from,
locationt to,
@@ -129,18 +109,6 @@ void rd_range_domaint::transform(
#endif
}
-/*******************************************************************\
-
-Function: rd_range_domaint::transform_dead
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rd_range_domaint::transform_dead(
const namespacet &ns,
locationt from)
@@ -157,18 +125,6 @@ void rd_range_domaint::transform_dead(
}
}
-/*******************************************************************\
-
-Function: rd_range_domaint::transform_start_thread
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rd_range_domaint::transform_start_thread(
const namespacet &ns,
reaching_definitions_analysist &rd)
@@ -194,18 +150,6 @@ void rd_range_domaint::transform_start_thread(
}
}
-/*******************************************************************\
-
-Function: rd_range_domaint::transform_function_call
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rd_range_domaint::transform_function_call(
const namespacet &ns,
locationt from,
@@ -269,18 +213,6 @@ void rd_range_domaint::transform_function_call(
}
}
-/*******************************************************************\
-
-Function: rd_range_domaint::transform_end_function
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rd_range_domaint::transform_end_function(
const namespacet &ns,
locationt from,
@@ -349,18 +281,6 @@ void rd_range_domaint::transform_end_function(
}
}
-/*******************************************************************\
-
-Function: rd_range_domaint::transform_assign
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rd_range_domaint::transform_assign(
const namespacet &ns,
locationt from,
@@ -394,18 +314,6 @@ void rd_range_domaint::transform_assign(
}
}
-/*******************************************************************\
-
-Function: rd_range_domaint::kill
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rd_range_domaint::kill(
const irep_idt &identifier,
const range_spect &range_start,
@@ -506,18 +414,6 @@ void rd_range_domaint::kill(
}
}
-/*******************************************************************\
-
-Function: rd_range_domaint::kill_inf
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rd_range_domaint::kill_inf(
const irep_idt &identifier,
const range_spect &range_start)
@@ -552,18 +448,6 @@ void rd_range_domaint::kill_inf(
#endif
}
-/*******************************************************************\
-
-Function: rd_range_domaint::gen
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool rd_range_domaint::gen(
locationt from,
const irep_idt &identifier,
@@ -636,21 +520,9 @@ bool rd_range_domaint::gen(
return true;
}
-/*******************************************************************\
-
-Function: rd_range_domaint::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void rd_range_domaint::output(std::ostream &out) const
{
- out << "Reaching definitions:" << std::endl;
+ out << "Reaching definitions:\n";
if(has_values.is_known())
{
@@ -681,24 +553,13 @@ void rd_range_domaint::output(std::ostream &out) const
out << "@" << itl->first->location_number;
}
- out << "]" << std::endl;
+ out << "]\n";
clear_cache(identifier);
}
}
-/*******************************************************************\
-
-Function: rd_range_domaint::merge_inner
-
- Inputs:
-
- Outputs: returns true iff there is s.th. new
-
- Purpose:
-
-\*******************************************************************/
-
+/// \return returns true iff there is s.th. new
bool rd_range_domaint::merge_inner(
values_innert &dest,
const values_innert &other)
@@ -749,18 +610,7 @@ bool rd_range_domaint::merge_inner(
return more;
}
-/*******************************************************************\
-
-Function: rd_range_domaint::merge
-
- Inputs:
-
- Outputs: returns true iff there is s.th. new
-
- Purpose:
-
-\*******************************************************************/
-
+/// \return returns true iff there is s.th. new
bool rd_range_domaint::merge(
const rd_range_domaint &other,
locationt from,
@@ -796,18 +646,7 @@ bool rd_range_domaint::merge(
return changed;
}
-/*******************************************************************\
-
-Function: rd_range_domaint::merge_shared
-
- Inputs:
-
- Outputs: returns true iff there is s.th. new
-
- Purpose:
-
-\*******************************************************************/
-
+/// \return returns true iff there is s.th. new
bool rd_range_domaint::merge_shared(
const rd_range_domaint &other,
goto_programt::const_targett from,
@@ -857,18 +696,6 @@ bool rd_range_domaint::merge_shared(
return changed;
}
-/*******************************************************************\
-
-Function: rd_range_domaint::get
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
const rd_range_domaint::ranges_at_loct &rd_range_domaint::get(
const irep_idt &identifier) const
{
@@ -884,18 +711,6 @@ const rd_range_domaint::ranges_at_loct &rd_range_domaint::get(
return entry->second;
}
-/*******************************************************************\
-
-Function: reaching_definitions_analysist::~reaching_definitions_analysist
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
reaching_definitions_analysist::~reaching_definitions_analysist()
{
if(is_dirty)
@@ -906,18 +721,6 @@ reaching_definitions_analysist::~reaching_definitions_analysist()
delete value_sets;
}
-/*******************************************************************\
-
-Function: reaching_definitions_analysist::initialize
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void reaching_definitions_analysist::initialize(
const goto_functionst &goto_functions)
{
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index a48a271a9a6..2cc7d815fa3 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -9,6 +9,10 @@ Date: February 2013
\*******************************************************************/
+/// \file
+/// Range-based reaching definitions analysis (following Field- Sensitive
+/// Program Dependence Analysis, Litvak et al., FSE 2010)
+
#ifndef CPROVER_ANALYSES_REACHING_DEFINITIONS_H
#define CPROVER_ANALYSES_REACHING_DEFINITIONS_H
diff --git a/src/analyses/replace_symbol_ext.cpp b/src/analyses/replace_symbol_ext.cpp
index 568ea45e090..75c697030b7 100644
--- a/src/analyses/replace_symbol_ext.cpp
+++ b/src/analyses/replace_symbol_ext.cpp
@@ -6,23 +6,15 @@ Author: Peter Schrammel
\*******************************************************************/
+/// \file
+/// Modified expression replacement for constant propagator
+
#include
#include
#include "replace_symbol_ext.h"
-/*******************************************************************\
-
-Function: replace_symbol_extt::replace
-
- Inputs:
-
- Outputs:
-
- Purpose: does not replace object in address_of expressions
-
-\*******************************************************************/
-
+/// does not replace object in address_of expressions
bool replace_symbol_extt::replace(exprt &dest) const
{
bool result=true;
diff --git a/src/analyses/replace_symbol_ext.h b/src/analyses/replace_symbol_ext.h
index 5a2152db17f..05d7226be40 100644
--- a/src/analyses/replace_symbol_ext.h
+++ b/src/analyses/replace_symbol_ext.h
@@ -6,6 +6,9 @@ Author: Peter Schrammel
\*******************************************************************/
+/// \file
+/// Modified expression replacement for constant propagator
+
#ifndef CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H
#define CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H
diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp
index 8309566f27d..dd6b8ac0f54 100644
--- a/src/analyses/static_analysis.cpp
+++ b/src/analyses/static_analysis.cpp
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Value Set Propagation
+
#include
#include
@@ -17,18 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
#define USE_DEPRECATED_STATIC_ANALYSIS_H
#include "static_analysis.h"
-/*******************************************************************\
-
-Function: static_analysis_baset::get_guard
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt static_analysis_baset::get_guard(
locationt from,
locationt to)
@@ -49,18 +40,6 @@ exprt static_analysis_baset::get_guard(
return from->guard;
}
-/*******************************************************************\
-
-Function: static_analysis_baset::get_return_lhs
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt static_analysis_baset::get_return_lhs(locationt to)
{
// get predecessor of "to"
@@ -79,18 +58,6 @@ exprt static_analysis_baset::get_return_lhs(locationt to)
return code.lhs();
}
-/*******************************************************************\
-
-Function: static_analysis_baset::operator()
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::operator()(
const goto_functionst &goto_functions)
{
@@ -98,18 +65,6 @@ void static_analysis_baset::operator()(
fixedpoint(goto_functions);
}
-/*******************************************************************\
-
-Function: static_analysis_baset::operator()
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::operator()(
const goto_programt &goto_program)
{
@@ -118,18 +73,6 @@ void static_analysis_baset::operator()(
fixedpoint(goto_program, goto_functions);
}
-/*******************************************************************\
-
-Function: static_analysis_baset::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::output(
const goto_functionst &goto_functions,
std::ostream &out) const
@@ -148,18 +91,6 @@ void static_analysis_baset::output(
}
}
-/*******************************************************************\
-
-Function: static_analysis_baset::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::output(
const goto_programt &goto_program,
const irep_idt &identifier,
@@ -179,18 +110,6 @@ void static_analysis_baset::output(
}
}
-/*******************************************************************\
-
-Function: static_analysis_baset::generate_states
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::generate_states(
const goto_functionst &goto_functions)
{
@@ -198,18 +117,6 @@ void static_analysis_baset::generate_states(
generate_states(f_it->second.body);
}
-/*******************************************************************\
-
-Function: static_analysis_baset::generate_states
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::generate_states(
const goto_programt &goto_program)
{
@@ -217,18 +124,6 @@ void static_analysis_baset::generate_states(
generate_state(i_it);
}
-/*******************************************************************\
-
-Function: static_analysis_baset::update
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::update(
const goto_functionst &goto_functions)
{
@@ -236,18 +131,6 @@ void static_analysis_baset::update(
update(f_it->second.body);
}
-/*******************************************************************\
-
-Function: static_analysis_baset::generate_states
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::update(
const goto_programt &goto_program)
{
@@ -270,18 +153,6 @@ void static_analysis_baset::update(
}
}
-/*******************************************************************\
-
-Function: static_analysis_baset::get_next
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
static_analysis_baset::locationt static_analysis_baset::get_next(
working_sett &working_set)
{
@@ -294,18 +165,6 @@ static_analysis_baset::locationt static_analysis_baset::get_next(
return l;
}
-/*******************************************************************\
-
-Function: static_analysis_baset::fixedpoint
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool static_analysis_baset::fixedpoint(
const goto_programt &goto_program,
const goto_functionst &goto_functions)
@@ -332,18 +191,6 @@ bool static_analysis_baset::fixedpoint(
return new_data;
}
-/*******************************************************************\
-
-Function: static_analysis_baset::visit
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool static_analysis_baset::visit(
locationt l,
working_sett &working_set,
@@ -397,18 +244,6 @@ bool static_analysis_baset::visit(
return new_data;
}
-/*******************************************************************\
-
-Function: static_analysis_baset::do_function_call
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::do_function_call(
locationt l_call, locationt l_return,
const goto_functionst &goto_functions,
@@ -480,18 +315,6 @@ void static_analysis_baset::do_function_call(
}
}
-/*******************************************************************\
-
-Function: static_analysis_baset::do_function_call_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::do_function_call_rec(
locationt l_call, locationt l_return,
const exprt &function,
@@ -594,18 +417,6 @@ void static_analysis_baset::do_function_call_rec(
}
}
-/*******************************************************************\
-
-Function: static_analysis_baset::sequential_fixedpoint
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::sequential_fixedpoint(
const goto_functionst &goto_functions)
{
@@ -616,18 +427,6 @@ void static_analysis_baset::sequential_fixedpoint(
fixedpoint(it->second.body, goto_functions);
}
-/*******************************************************************\
-
-Function: static_analysis_baset::concurrent_fixedpoint
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void static_analysis_baset::concurrent_fixedpoint(
const goto_functionst &goto_functions)
{
diff --git a/src/analyses/static_analysis.h b/src/analyses/static_analysis.h
index 2a390fb7e61..17d8dced473 100644
--- a/src/analyses/static_analysis.h
+++ b/src/analyses/static_analysis.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Static Analysis
+
#ifndef CPROVER_ANALYSES_STATIC_ANALYSIS_H
#define CPROVER_ANALYSES_STATIC_ANALYSIS_H
diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp
index 814fcaf3730..dfc012238ab 100644
--- a/src/analyses/uncaught_exceptions_analysis.cpp
+++ b/src/analyses/uncaught_exceptions_analysis.cpp
@@ -6,23 +6,15 @@ Author: Cristina David
\*******************************************************************/
+/// \file
+/// Over-approximating uncaught exceptions analysis
+
#ifdef DEBUG
#include
#endif
#include "uncaught_exceptions_analysis.h"
-/*******************************************************************\
-
-Function: get_exception_type
-
- Inputs:
-
- Outputs:
-
- Purpose: Returns the compile type of an exception
-
-\*******************************************************************/
-
+/// Returns the compile type of an exception
irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type)
{
assert(type.id()==ID_pointer);
@@ -34,18 +26,7 @@ irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type)
return ID_empty;
}
-/*******************************************************************\
-
-Function: get_exception_symbol
-
- Inputs:
-
- Outputs:
-
- Purpose: Returns the symbol corresponding to an exception
-
-\*******************************************************************/
-
+/// Returns the symbol corresponding to an exception
exprt uncaught_exceptions_domaint::get_exception_symbol(const exprt &expr)
{
if(expr.id()!=ID_symbol && expr.has_operands())
@@ -54,18 +35,7 @@ exprt uncaught_exceptions_domaint::get_exception_symbol(const exprt &expr)
return expr;
}
-/*******************************************************************\
-
-Function: uncaught_exceptions_domaint::join
-
- Inputs:
-
- Outputs:
-
- Purpose: The join operator for the uncaught exceptions domain
-
-\*******************************************************************/
-
+/// The join operator for the uncaught exceptions domain
void uncaught_exceptions_domaint::join(
const irep_idt &element)
{
@@ -85,18 +55,7 @@ void uncaught_exceptions_domaint::join(
}
-/*******************************************************************\
-
-Function: uncaught_exceptions_domaint::transform
-
- Inputs:
-
- Outputs:
-
- Purpose: The transformer for the uncaught exceptions domain
-
-\*******************************************************************/
-
+/// The transformer for the uncaught exceptions domain
void uncaught_exceptions_domaint::transform(
const goto_programt::const_targett from,
uncaught_exceptions_analysist &uea,
@@ -175,54 +134,20 @@ void uncaught_exceptions_domaint::transform(
}
}
-/*******************************************************************\
-
-Function: uncaught_exceptions_domaint::get_elements
-
- Inputs:
-
- Outputs:
-
- Purpose: Returns the value of the private member thrown
-
-\*******************************************************************/
-
+/// Returns the value of the private member thrown
const std::set &uncaught_exceptions_domaint::get_elements() const
{
return thrown;
}
-/*******************************************************************\
-
-Function: uncaught_exceptions_domaint::operator()
-
- Inputs:
-
- Outputs:
-
- Purpose: Constructs the class hierarchy
-
-\*******************************************************************/
-
+/// Constructs the class hierarchy
void uncaught_exceptions_domaint::operator()(
const namespacet &ns)
{
class_hierarchy(ns.get_symbol_table());
}
-/*******************************************************************\
-
-Function: uncaught_exceptions_analysist::collect_uncaught_exceptions
-
- Inputs:
-
- Outputs:
-
- Purpose: Runs the uncaught exceptions analysis, which
- populates the exceptions map
-
-\*******************************************************************/
-
+/// Runs the uncaught exceptions analysis, which populates the exceptions map
void uncaught_exceptions_analysist::collect_uncaught_exceptions(
const goto_functionst &goto_functions,
const namespacet &ns)
@@ -256,19 +181,8 @@ void uncaught_exceptions_analysist::collect_uncaught_exceptions(
}
}
-/*******************************************************************\
-
-Function: uncaught_exceptions_analysist::output
-
- Inputs:
-
- Outputs:
-
- Purpose: Prints the exceptions map that maps each method to the
- set of exceptions that may escape it
-
-\*******************************************************************/
-
+/// Prints the exceptions map that maps each method to the set of exceptions
+/// that may escape it
void uncaught_exceptions_analysist::output(
const goto_functionst &goto_functions)
{
@@ -288,19 +202,7 @@ void uncaught_exceptions_analysist::output(
#endif
}
-/*******************************************************************\
-
-Function: uncaught_exceptions_analysist::operator()
-
- Inputs:
-
- Outputs:
-
- Purpose: Applies the uncaught exceptions analysis and
- outputs the result
-
-\*******************************************************************/
-
+/// Applies the uncaught exceptions analysis and outputs the result
void uncaught_exceptions_analysist::operator()(
const goto_functionst &goto_functions,
const namespacet &ns,
@@ -312,19 +214,7 @@ void uncaught_exceptions_analysist::operator()(
output(goto_functions);
}
-/*******************************************************************\
-
-Function: uncaught_exceptions
-
- Inputs:
-
- Outputs:
-
- Purpose: Applies the uncaught exceptions analysis and
- outputs the result
-
-\*******************************************************************/
-
+/// Applies the uncaught exceptions analysis and outputs the result
void uncaught_exceptions(
const goto_functionst &goto_functions,
const namespacet &ns,
diff --git a/src/analyses/uncaught_exceptions_analysis.h b/src/analyses/uncaught_exceptions_analysis.h
index 50ed75b202c..a53998b4bd2 100644
--- a/src/analyses/uncaught_exceptions_analysis.h
+++ b/src/analyses/uncaught_exceptions_analysis.h
@@ -6,6 +6,9 @@ Author: Cristina David
\*******************************************************************/
+/// \file
+/// Over-approximative uncaught exceptions analysis
+
#ifndef CPROVER_ANALYSES_UNCAUGHT_EXCEPTIONS_ANALYSIS_H
#define CPROVER_ANALYSES_UNCAUGHT_EXCEPTIONS_ANALYSIS_H
@@ -15,15 +18,7 @@ Author: Cristina David
#include
#include
-/*******************************************************************\
-
- Class: uncaught_exceptions_domaint
-
- Purpose: defines the domain used by the uncaught
- exceptions analysis
-
-\*******************************************************************/
-
+/// defines the domain used by the uncaught exceptions analysis
class uncaught_exceptions_analysist;
class uncaught_exceptions_domaint
@@ -58,15 +53,8 @@ class uncaught_exceptions_domaint
class_hierarchyt class_hierarchy;
};
-/*******************************************************************\
-
- Class: uncaught_exceptions_analysist
-
- Purpose: computes in exceptions_map an overapproximation of the
- exceptions thrown by each method
-
-\*******************************************************************/
-
+/// computes in exceptions_map an overapproximation of the exceptions thrown by
+/// each method
class uncaught_exceptions_analysist
{
public:
diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp
index 8a6e8dd52a5..60f8c45c1bb 100644
--- a/src/analyses/uninitialized_domain.cpp
+++ b/src/analyses/uninitialized_domain.cpp
@@ -8,23 +8,14 @@ Date: January 2010
\*******************************************************************/
+/// \file
+/// Detection for Uninitialized Local Variables
+
#include
#include
#include "uninitialized_domain.h"
-/*******************************************************************\
-
-Function: uninitialized_domaint::transform
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void uninitialized_domaint::transform(
locationt from,
locationt to,
@@ -60,18 +51,6 @@ void uninitialized_domaint::transform(
}
}
-/*******************************************************************\
-
-Function: uninitialized_domaint::assign
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void uninitialized_domaint::assign(const exprt &lhs)
{
if(lhs.id()==ID_index)
@@ -82,18 +61,6 @@ void uninitialized_domaint::assign(const exprt &lhs)
uninitialized.erase(to_symbol_expr(lhs).get_identifier());
}
-/*******************************************************************\
-
-Function: uninitialized_domaint::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void uninitialized_domaint::output(
std::ostream &out,
const ai_baset &ai,
@@ -108,18 +75,7 @@ void uninitialized_domaint::output(
}
}
-/*******************************************************************\
-
-Function: uninitialized_domaint::merge
-
- Inputs:
-
- Outputs: returns true iff there is s.th. new
-
- Purpose:
-
-\*******************************************************************/
-
+/// \return returns true iff there is s.th. new
bool uninitialized_domaint::merge(
const uninitialized_domaint &other,
locationt from,
diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h
index 6ca27f341b0..a48f9954388 100644
--- a/src/analyses/uninitialized_domain.h
+++ b/src/analyses/uninitialized_domain.h
@@ -8,6 +8,9 @@ Date: January 2010
\*******************************************************************/
+/// \file
+/// Detection for Uninitialized Local Variables
+
#ifndef CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H
#define CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H
diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile
index cfee8e68f07..90bdd1e6a56 100644
--- a/src/ansi-c/Makefile
+++ b/src/ansi-c/Makefile
@@ -24,7 +24,6 @@ SRC = anonymous_member.cpp \
c_typecheck_initializer.cpp \
c_typecheck_type.cpp \
c_typecheck_typecast.cpp \
- c_types.cpp \
cprover_library.cpp \
designator.cpp \
expr2c.cpp \
@@ -55,7 +54,11 @@ CLEANFILES = ansi-c$(LIBEXT) \
arm_builtin_headers.inc cw_builtin_headers.inc \
gcc_builtin_headers_arm.inc gcc_builtin_headers_alpha.inc \
gcc_builtin_headers_mips.inc gcc_builtin_headers_power.inc \
- clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc
+ clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
+ gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
+ gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
+ gcc_builtin_headers_mem_string.inc \
+ gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
all: ansi-c$(LIBEXT)
@@ -116,10 +119,17 @@ cprover_library.cpp: cprover_library.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_generic.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-2.inc
+ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-3.inc
+ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-4.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc
+ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_math.inc
+ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mem_string.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mips.inc
+ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_omp.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_power.inc
+ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_tm.inc
+ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ubsan.inc
ansi_c_internal_additions$(OBJEXT): arm_builtin_headers.inc
ansi_c_internal_additions$(OBJEXT): cw_builtin_headers.inc
ansi_c_internal_additions$(OBJEXT): clang_builtin_headers.inc
@@ -129,7 +139,11 @@ generated_files: cprover_library.inc gcc_builtin_headers_generic.inc \
gcc_builtin_headers_arm.inc gcc_builtin_headers_mips.inc \
gcc_builtin_headers_power.inc arm_builtin_headers.inc \
cw_builtin_headers.inc ansi_c_y.tab.cpp ansi_c_lex.yy.cpp \
- ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc
+ ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
+ gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
+ gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
+ gcc_builtin_headers_mem_string.inc \
+ gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
###############################################################################
diff --git a/src/ansi-c/anonymous_member.cpp b/src/ansi-c/anonymous_member.cpp
index adaff8d4680..197739f5941 100644
--- a/src/ansi-c/anonymous_member.cpp
+++ b/src/ansi-c/anonymous_member.cpp
@@ -6,23 +6,14 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Language Type Checking
+
#include
#include
#include "anonymous_member.h"
-/*******************************************************************\
-
-Function: make_member_expr
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
static exprt make_member_expr(
const exprt &struct_union,
const struct_union_typet::componentt &component,
@@ -46,18 +37,6 @@ static exprt make_member_expr(
return result;
}
-/*******************************************************************\
-
-Function: get_component_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt get_component_rec(
const exprt &struct_union,
const irep_idt &component_name,
@@ -90,18 +69,6 @@ exprt get_component_rec(
return nil_exprt();
}
-/*******************************************************************\
-
-Function: has_component_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool has_component_rec(
const typet &type,
const irep_idt &component_name,
diff --git a/src/ansi-c/anonymous_member.h b/src/ansi-c/anonymous_member.h
index d9b00394b6f..3c58ad70efb 100644
--- a/src/ansi-c/anonymous_member.h
+++ b/src/ansi-c/anonymous_member.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// C Language Type Checking
+
#ifndef CPROVER_ANSI_C_ANONYMOUS_MEMBER_H
#define CPROVER_ANSI_C_ANONYMOUS_MEMBER_H
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index 7dc6f2165cf..7f42f94c8a2 100644
--- a/src/ansi-c/ansi_c_convert_type.cpp
+++ b/src/ansi-c/ansi_c_convert_type.cpp
@@ -6,8 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// SpecC Language Conversion
+
#include
+#include
#include
#include
#include
@@ -16,18 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "ansi_c_convert_type.h"
-/*******************************************************************\
-
-Function: ansi_c_convert_typet::convert
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_convert_typet::read(const typet &type)
{
clear();
@@ -35,18 +27,6 @@ void ansi_c_convert_typet::read(const typet &type)
read_rec(type);
}
-/*******************************************************************\
-
-Function: ansi_c_convert_typet::read_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_convert_typet::read_rec(const typet &type)
{
if(type.id()==ID_merged_type)
@@ -240,18 +220,6 @@ void ansi_c_convert_typet::read_rec(const typet &type)
other.push_back(type);
}
-/*******************************************************************\
-
-Function: ansi_c_convert_typet::write
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_convert_typet::write(typet &type)
{
type.clear();
@@ -271,6 +239,15 @@ void ansi_c_convert_typet::write(typet &type)
throw 0;
}
+ // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
+ if(other.size()==2)
+ {
+ if(other.front().id()==ID_asm && other.back().id()==ID_empty)
+ other.pop_front();
+ else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
+ other.pop_back();
+ }
+
if(other.size()!=1)
{
error().source_location=source_location;
@@ -463,14 +440,25 @@ void ansi_c_convert_typet::write(typet &type)
}
if(int8_cnt)
- type=is_signed?signed_char_type():unsigned_char_type();
+ if(is_signed)
+ type=signed_char_type();
+ else
+ type=unsigned_char_type();
else if(int16_cnt)
- type=is_signed?signed_short_int_type():unsigned_short_int_type();
+ if(is_signed)
+ type=signed_short_int_type();
+ else
+ type=unsigned_short_int_type();
else if(int32_cnt)
- type=is_signed?signed_int_type():unsigned_int_type();
+ if(is_signed)
+ type=signed_int_type();
+ else
+ type=unsigned_int_type();
else if(int64_cnt) // Visual Studio: equivalent to long long int
- type=
- is_signed?signed_long_long_int_type():unsigned_long_long_int_type();
+ if(is_signed)
+ type=signed_long_long_int_type();
+ else
+ type=unsigned_long_long_int_type();
else
assert(false);
}
@@ -508,19 +496,31 @@ void ansi_c_convert_typet::write(typet &type)
throw 0;
}
- type=is_signed?signed_short_int_type():unsigned_short_int_type();
+ if(is_signed)
+ type=signed_short_int_type();
+ else
+ type=unsigned_short_int_type();
}
else if(long_cnt==0)
{
- type=is_signed?signed_int_type():unsigned_int_type();
+ if(is_signed)
+ type=signed_int_type();
+ else
+ type=unsigned_int_type();
}
else if(long_cnt==1)
{
- type=is_signed?signed_long_int_type():unsigned_long_int_type();
+ if(is_signed)
+ type=signed_long_int_type();
+ else
+ type=unsigned_long_int_type();
}
else if(long_cnt==2)
{
- type=is_signed?signed_long_long_int_type():unsigned_long_long_int_type();
+ if(is_signed)
+ type=signed_long_long_int_type();
+ else
+ type=unsigned_long_long_int_type();
}
else
{
diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h
index 0fef20b4928..6ce1a7ebecf 100644
--- a/src/ansi-c/ansi_c_convert_type.h
+++ b/src/ansi-c/ansi_c_convert_type.h
@@ -6,12 +6,14 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Language Conversion
+
#ifndef CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
#define CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
#include
-#include "c_types.h"
#include "c_qualifiers.h"
#include "c_storage_spec.h"
diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp
index 7f9d0980583..74915af0f42 100644
--- a/src/ansi-c/ansi_c_declaration.cpp
+++ b/src/ansi-c/ansi_c_declaration.cpp
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Language Type Checking
+
#include
#include
@@ -14,18 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "ansi_c_declaration.h"
-/*******************************************************************\
-
-Function: ansi_c_declaratort::build
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_declaratort::build(irept &src)
{
typet *p=static_cast(&src);
@@ -42,7 +33,7 @@ void ansi_c_declaratort::build(irept &src)
t.make_nil();
break;
}
- else if(t.id()==irep_idt() ||
+ else if(t.id().empty() ||
t.is_nil())
{
assert(0);
@@ -66,18 +57,6 @@ void ansi_c_declaratort::build(irept &src)
value().make_nil();
}
-/*******************************************************************\
-
-Function: ansi_c_declarationt::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_declarationt::output(std::ostream &out) const
{
out << "Flags:";
@@ -109,18 +88,6 @@ void ansi_c_declarationt::output(std::ostream &out) const
out << "Declarator: " << declarator.pretty() << "\n";
}
-/*******************************************************************\
-
-Function: ansi_c_declarationt::full_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
typet ansi_c_declarationt::full_type(
const ansi_c_declaratort &declarator) const
{
@@ -153,18 +120,6 @@ typet ansi_c_declarationt::full_type(
return result;
}
-/*******************************************************************\
-
-Function: ansi_c_declarationt::to_symbol
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_declarationt::to_symbol(
const ansi_c_declaratort &declarator,
symbolt &symbol) const
diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h
index 3143c2090a5..af5db98e32e 100644
--- a/src/ansi-c/ansi_c_declaration.h
+++ b/src/ansi-c/ansi_c_declaration.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-CC Language Type Checking
+
#ifndef CPROVER_ANSI_C_ANSI_C_DECLARATION_H
#define CPROVER_ANSI_C_ANSI_C_DECLARATION_H
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index ecb2dcc73cd..90f1fda46d4 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include
@@ -17,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include
#include
-#include
+#include
#include
#include
@@ -26,18 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "ansi_c_entry_point.h"
#include "c_nondet_symbol_factory.h"
-/*******************************************************************\
-
-Function: build_function_environment
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt::operandst build_function_environment(
const code_typet::parameterst ¶meters,
code_blockt &init_code,
@@ -68,18 +57,6 @@ exprt::operandst build_function_environment(
return main_arguments;
}
-/*******************************************************************\
-
-Function: record_function_outputs
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void record_function_outputs(
const symbolt &function,
code_blockt &init_code,
@@ -141,18 +118,6 @@ void record_function_outputs(
#endif
}
-/*******************************************************************\
-
-Function: ansi_c_entry_point
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool ansi_c_entry_point(
symbol_tablet &symbol_table,
const std::string &standard_main,
diff --git a/src/ansi-c/ansi_c_entry_point.h b/src/ansi-c/ansi_c_entry_point.h
index 07d09ae2d44..835dd31845d 100644
--- a/src/ansi-c/ansi_c_entry_point.h
+++ b/src/ansi-c/ansi_c_entry_point.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H
#define CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index eb564038e2e..a29419961a0 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include "ansi_c_internal_additions.h"
@@ -15,6 +16,31 @@ const char gcc_builtin_headers_generic[]=
#include "gcc_builtin_headers_generic.inc"
; // NOLINT(whitespace/semicolon)
+const char gcc_builtin_headers_math[]=
+"# 1 \"gcc_builtin_headers_math.h\"\n"
+#include "gcc_builtin_headers_math.inc"
+; // NOLINT(whitespace/semicolon)
+
+const char gcc_builtin_headers_mem_string[]=
+"# 1 \"gcc_builtin_headers_mem_string.h\"\n"
+#include "gcc_builtin_headers_mem_string.inc"
+; // NOLINT(whitespace/semicolon)
+
+const char gcc_builtin_headers_omp[]=
+"# 1 \"gcc_builtin_headers_omp.h\"\n"
+#include "gcc_builtin_headers_omp.inc"
+; // NOLINT(whitespace/semicolon)
+
+const char gcc_builtin_headers_tm[]=
+"# 1 \"gcc_builtin_headers_tm.h\"\n"
+#include "gcc_builtin_headers_tm.inc"
+; // NOLINT(whitespace/semicolon)
+
+const char gcc_builtin_headers_ubsan[]=
+"# 1 \"gcc_builtin_headers_ubsan.h\"\n"
+#include "gcc_builtin_headers_ubsan.inc"
+; // NOLINT(whitespace/semicolon)
+
const char gcc_builtin_headers_ia32[]=
"# 1 \"gcc_builtin_headers_ia32.h\"\n"
#include "gcc_builtin_headers_ia32.inc"
@@ -22,6 +48,12 @@ const char gcc_builtin_headers_ia32[]=
const char gcc_builtin_headers_ia32_2[]=
#include "gcc_builtin_headers_ia32-2.inc"
; // NOLINT(whitespace/semicolon)
+const char gcc_builtin_headers_ia32_3[]=
+#include "gcc_builtin_headers_ia32-3.inc"
+; // NOLINT(whitespace/semicolon)
+const char gcc_builtin_headers_ia32_4[]=
+#include "gcc_builtin_headers_ia32-4.inc"
+; // NOLINT(whitespace/semicolon)
const char gcc_builtin_headers_alpha[]=
"# 1 \"gcc_builtin_headers_alpha.h\"\n"
@@ -58,18 +90,6 @@ const char clang_builtin_headers[]=
#include "clang_builtin_headers.inc"
; // NOLINT(whitespace/semicolon)
-/*******************************************************************\
-
-Function: architecture_string
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
static std::string architecture_string(const std::string &value, const char *s)
{
return std::string("const char *__CPROVER_architecture_")+
@@ -77,18 +97,6 @@ static std::string architecture_string(const std::string &value, const char *s)
"=\""+value+"\";\n";
}
-/*******************************************************************\
-
-Function: architecture_string
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
static std::string architecture_string(int value, const char *s)
{
return std::string("const int __CPROVER_architecture_")+
@@ -96,18 +104,6 @@ static std::string architecture_string(int value, const char *s)
"="+std::to_string(value)+";\n";
}
-/*******************************************************************\
-
-Function: ansi_c_internal_additions
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_internal_additions(std::string &code)
{
code+=
@@ -158,6 +154,8 @@ void ansi_c_internal_additions(std::string &code)
"signed __CPROVER_POINTER_OFFSET(const void *p);\n"
"__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);\n"
"extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n"
+ // NOLINTNEXTLINE(whitespace/line_length)
+ "void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);\n"
// malloc
"void *__CPROVER_malloc(__CPROVER_size_t size);\n"
@@ -211,7 +209,11 @@ void ansi_c_internal_additions(std::string &code)
// arrays
// NOLINTNEXTLINE(whitespace/line_length)
"__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);\n"
+ // overwrite all of *dest (possibly using nondet values), even
+ // if *src is smaller
"void __CPROVER_array_copy(const void *dest, const void *src);\n"
+ // replace at most size-of-*src bytes in *dest
+ "void __CPROVER_array_replace(const void *dest, const void *src);\n"
"void __CPROVER_array_set(const void *dest, ...);\n"
// k-induction
@@ -242,6 +244,11 @@ void ansi_c_internal_additions(std::string &code)
config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
{
code+=gcc_builtin_headers_generic;
+ code+=gcc_builtin_headers_math;
+ code+=gcc_builtin_headers_mem_string;
+ code+=gcc_builtin_headers_omp;
+ code+=gcc_builtin_headers_tm;
+ code+=gcc_builtin_headers_ubsan;
code+=clang_builtin_headers;
// there are many more, e.g., look at
@@ -256,6 +263,8 @@ void ansi_c_internal_additions(std::string &code)
code+=gcc_builtin_headers_ia32;
code+=gcc_builtin_headers_ia32_2;
+ code+=gcc_builtin_headers_ia32_3;
+ code+=gcc_builtin_headers_ia32_4;
}
else if(config.ansi_c.arch=="arm64" ||
config.ansi_c.arch=="armel" ||
@@ -310,18 +319,6 @@ void ansi_c_internal_additions(std::string &code)
ansi_c_architecture_strings(code);
}
-/*******************************************************************\
-
-Function: architecture_strings
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_architecture_strings(std::string &code)
{
// The following are CPROVER-specific.
diff --git a/src/ansi-c/ansi_c_internal_additions.h b/src/ansi-c/ansi_c_internal_additions.h
index 2b4a94f1d9b..a0977a35331 100644
--- a/src/ansi-c/ansi_c_internal_additions.h
+++ b/src/ansi-c/ansi_c_internal_additions.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H
#define CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H
@@ -15,7 +16,16 @@ void ansi_c_internal_additions(std::string &code);
void ansi_c_architecture_strings(std::string &code);
extern const char gcc_builtin_headers_generic[];
+extern const char gcc_builtin_headers_math[];
+extern const char gcc_builtin_headers_mem_string[];
+extern const char gcc_builtin_headers_omp[];
+extern const char gcc_builtin_headers_tm[];
+extern const char gcc_builtin_headers_ubsan[];
+extern const char clang_builtin_headers[];
extern const char gcc_builtin_headers_ia32[];
+extern const char gcc_builtin_headers_ia32_2[];
+extern const char gcc_builtin_headers_ia32_3[];
+extern const char gcc_builtin_headers_ia32_4[];
extern const char arm_builtin_headers[];
#endif // CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index 159b0d6df40..e4a005b7100 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include
#include
@@ -25,52 +26,17 @@ Author: Daniel Kroening, kroening@kroening.com
#include "ansi_c_internal_additions.h"
#include "type2name.h"
-/*******************************************************************\
-
-Function: ansi_c_languaget::extensions
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
std::set ansi_c_languaget::extensions() const
{
return { "c", "i" };
}
-/*******************************************************************\
-
-Function: ansi_c_languaget::modules_provided
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_languaget::modules_provided(std::set &modules)
{
modules.insert(get_base_name(parse_path, true));
}
-/*******************************************************************\
-
-Function: ansi_c_languaget::preprocess
-
- Inputs:
-
- Outputs:
-
- Purpose: ANSI-C preprocessing
-
-\*******************************************************************/
-
+/// ANSI-C preprocessing
bool ansi_c_languaget::preprocess(
std::istream &instream,
const std::string &path,
@@ -83,18 +49,6 @@ bool ansi_c_languaget::preprocess(
return c_preprocess(path, outstream, get_message_handler());
}
-/*******************************************************************\
-
-Function: ansi_c_languaget::parse
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool ansi_c_languaget::parse(
std::istream &instream,
const std::string &path)
@@ -147,18 +101,6 @@ bool ansi_c_languaget::parse(
return result;
}
-/*******************************************************************\
-
-Function: ansi_c_languaget::typecheck
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool ansi_c_languaget::typecheck(
symbol_tablet &symbol_table,
const std::string &module)
@@ -182,18 +124,6 @@ bool ansi_c_languaget::typecheck(
return false;
}
-/*******************************************************************\
-
-Function: ansi_c_languaget::final
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool ansi_c_languaget::final(symbol_tablet &symbol_table)
{
generate_opaque_method_stubs(symbol_table);
@@ -204,52 +134,16 @@ bool ansi_c_languaget::final(symbol_tablet &symbol_table)
return false;
}
-/*******************************************************************\
-
-Function: ansi_c_languaget::show_parse
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_languaget::show_parse(std::ostream &out)
{
parse_tree.output(out);
}
-/*******************************************************************\
-
-Function: new_ansi_c_language
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
languaget *new_ansi_c_language()
{
return new ansi_c_languaget;
}
-/*******************************************************************\
-
-Function: ansi_c_languaget::from_expr
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool ansi_c_languaget::from_expr(
const exprt &expr,
std::string &code,
@@ -259,18 +153,6 @@ bool ansi_c_languaget::from_expr(
return false;
}
-/*******************************************************************\
-
-Function: ansi_c_languaget::from_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool ansi_c_languaget::from_type(
const typet &type,
std::string &code,
@@ -280,18 +162,6 @@ bool ansi_c_languaget::from_type(
return false;
}
-/*******************************************************************\
-
-Function: ansi_c_languaget::type_to_name
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool ansi_c_languaget::type_to_name(
const typet &type,
std::string &name,
@@ -301,18 +171,6 @@ bool ansi_c_languaget::type_to_name(
return false;
}
-/*******************************************************************\
-
-Function: ansi_c_languaget::to_expr
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool ansi_c_languaget::to_expr(
const std::string &code,
const std::string &module,
@@ -359,18 +217,6 @@ bool ansi_c_languaget::to_expr(
return result;
}
-/*******************************************************************\
-
-Function: ansi_c_languaget::~ansi_c_languaget
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
ansi_c_languaget::~ansi_c_languaget()
{
}
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index 9f6fba0cc9b..45b7d6aaa3f 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
#define CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
diff --git a/src/ansi-c/ansi_c_parse_tree.cpp b/src/ansi-c/ansi_c_parse_tree.cpp
index 4f58d094563..4ae1f955ea0 100644
--- a/src/ansi-c/ansi_c_parse_tree.cpp
+++ b/src/ansi-c/ansi_c_parse_tree.cpp
@@ -6,56 +6,21 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include "ansi_c_parse_tree.h"
-/*******************************************************************\
-
-Function: ansi_c_parse_treet::swap
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_parse_treet::swap(ansi_c_parse_treet &ansi_c_parse_tree)
{
ansi_c_parse_tree.items.swap(items);
}
-/*******************************************************************\
-
-Function: ansi_c_parse_treet::clear
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_parse_treet::clear()
{
items.clear();
}
-/*******************************************************************\
-
-Function: ansi_c_parse_treet::output
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_parse_treet::output(std::ostream &out) const
{
for(const auto &item : items)
diff --git a/src/ansi-c/ansi_c_parse_tree.h b/src/ansi-c/ansi_c_parse_tree.h
index e32d5a6ca20..c346b5853fe 100644
--- a/src/ansi-c/ansi_c_parse_tree.h
+++ b/src/ansi-c/ansi_c_parse_tree.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_ANSI_C_PARSE_TREE_H
#define CPROVER_ANSI_C_ANSI_C_PARSE_TREE_H
diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp
index 77a71b62dc2..6ce4f63b141 100644
--- a/src/ansi-c/ansi_c_parser.cpp
+++ b/src/ansi-c/ansi_c_parser.cpp
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include "ansi_c_parser.h"
@@ -13,18 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
ansi_c_parsert ansi_c_parser;
-/*******************************************************************\
-
-Function: ansi_c_parsert::lookup
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
ansi_c_id_classt ansi_c_parsert::lookup(
const irep_idt &base_name,
irep_idt &identifier, // output
@@ -70,18 +59,6 @@ ansi_c_id_classt ansi_c_parsert::lookup(
return ansi_c_id_classt::ANSI_C_UNKNOWN;
}
-/*******************************************************************\
-
-Function: ansi_c_parsert::add_tag_with_body
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_parsert::add_tag_with_body(irept &tag)
{
const std::string scope_name=
@@ -100,18 +77,6 @@ void ansi_c_parsert::add_tag_with_body(irept &tag)
}
}
-/*******************************************************************\
-
-Function: yyansi_cerror
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
extern char *yyansi_ctext;
int yyansi_cerror(const std::string &error)
@@ -120,18 +85,6 @@ int yyansi_cerror(const std::string &error)
return 0;
}
-/*******************************************************************\
-
-Function: ansi_c_parsert::add_declarator
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_parsert::add_declarator(
exprt &declaration,
irept &declarator)
@@ -202,18 +155,6 @@ void ansi_c_parsert::add_declarator(
ansi_c_declaration.declarators().push_back(new_declarator);
}
-/*******************************************************************\
-
-Function: ansi_c_parsert::get_class
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
ansi_c_id_classt ansi_c_parsert::get_class(const typet &type)
{
if(type.id()==ID_typedef)
diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h
index 579797db46a..2dc2c77001a 100644
--- a/src/ansi-c/ansi_c_parser.h
+++ b/src/ansi-c/ansi_c_parser.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_ANSI_C_PARSER_H
#define CPROVER_ANSI_C_ANSI_C_PARSER_H
diff --git a/src/ansi-c/ansi_c_scope.cpp b/src/ansi-c/ansi_c_scope.cpp
index ffd3663e1fa..6a4a626b3f8 100644
--- a/src/ansi-c/ansi_c_scope.cpp
+++ b/src/ansi-c/ansi_c_scope.cpp
@@ -6,22 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include "ansi_c_scope.h"
-/*******************************************************************\
-
-Function: ansi_c_scopet::print
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void ansi_c_scopet::print(std::ostream &out) const
{
out << "Prefix: " << prefix << "\n";
diff --git a/src/ansi-c/ansi_c_scope.h b/src/ansi-c/ansi_c_scope.h
index 6f7b92b876c..0f9bc117729 100644
--- a/src/ansi-c/ansi_c_scope.h
+++ b/src/ansi-c/ansi_c_scope.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_ANSI_C_SCOPE_H
#define CPROVER_ANSI_C_ANSI_C_SCOPE_H
diff --git a/src/ansi-c/ansi_c_typecheck.cpp b/src/ansi-c/ansi_c_typecheck.cpp
index 08da6bbae01..50bfe78dffb 100644
--- a/src/ansi-c/ansi_c_typecheck.cpp
+++ b/src/ansi-c/ansi_c_typecheck.cpp
@@ -6,19 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
-#include "ansi_c_typecheck.h"
-
-/*******************************************************************\
-
-Function: ansi_c_typecheckt::typecheck
-
- Inputs:
-
- Outputs:
-
- Purpose:
+/// \file
+/// ANSI-C Language Type Checking
-\*******************************************************************/
+#include "ansi_c_typecheck.h"
void ansi_c_typecheckt::typecheck()
{
@@ -32,18 +23,6 @@ void ansi_c_typecheckt::typecheck()
}
}
-/*******************************************************************\
-
-Function: ansi_c_typecheck
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool ansi_c_typecheck(
ansi_c_parse_treet &ansi_c_parse_tree,
symbol_tablet &symbol_table,
@@ -55,23 +34,14 @@ bool ansi_c_typecheck(
return ansi_c_typecheck.typecheck_main();
}
-/*******************************************************************\
-
-Function: ansi_c_typecheck
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool ansi_c_typecheck(
exprt &expr,
message_handlert &message_handler,
const namespacet &ns)
{
+ const unsigned errors_before=
+ message_handler.get_message_count(messaget::M_ERROR);
+
symbol_tablet symbol_table;
ansi_c_parse_treet ansi_c_parse_tree;
@@ -99,5 +69,5 @@ bool ansi_c_typecheck(
ansi_c_typecheck.error() << e << messaget::eom;
}
- return ansi_c_typecheck.get_error_found();
+ return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
}
diff --git a/src/ansi-c/ansi_c_typecheck.h b/src/ansi-c/ansi_c_typecheck.h
index aa6672d0d01..fdb9a32f2fe 100644
--- a/src/ansi-c/ansi_c_typecheck.h
+++ b/src/ansi-c/ansi_c_typecheck.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Language Type Checking
+
#ifndef CPROVER_ANSI_C_ANSI_C_TYPECHECK_H
#define CPROVER_ANSI_C_ANSI_C_TYPECHECK_H
diff --git a/src/ansi-c/c_misc.cpp b/src/ansi-c/c_misc.cpp
index 94baea10fa2..6af272c86a0 100644
--- a/src/ansi-c/c_misc.cpp
+++ b/src/ansi-c/c_misc.cpp
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Misc Utilities
+
#include
#ifdef _WIN32
@@ -16,18 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "c_misc.h"
-/*******************************************************************\
-
-Function: MetaChar
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
static void MetaChar(std::string &out, char c, bool inString)
{
switch(c)
@@ -102,18 +93,6 @@ static void MetaChar(std::string &out, char c, bool inString)
}
#if 0
-/*******************************************************************\
-
-Function: MetaChar
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
static std::string MetaChar(char c)
{
std::string result;
@@ -122,18 +101,6 @@ static std::string MetaChar(char c)
}
#endif
-/*******************************************************************\
-
-Function: MetaString
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
std::string MetaString(const std::string &in)
{
std::string result;
diff --git a/src/ansi-c/c_misc.h b/src/ansi-c/c_misc.h
index 40f9d0db5b8..5af7eb4754c 100644
--- a/src/ansi-c/c_misc.h
+++ b/src/ansi-c/c_misc.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Misc Utilities
+
#ifndef CPROVER_ANSI_C_C_MISC_H
#define CPROVER_ANSI_C_C_MISC_H
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 9149d6f8786..2b51ce8fb05 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -6,10 +6,14 @@ Author: DiffBlue Limited. All rights reserved.
\*******************************************************************/
+/// \file
+/// C Nondet Symbol Factory
+
#include
#include
#include
+#include
#include
#include
#include
@@ -20,30 +24,19 @@ Author: DiffBlue Limited. All rights reserved.
#include
-#include
#include
#include
#include "c_nondet_symbol_factory.h"
-/*******************************************************************\
-
-Function: declare_new_tmp_symbol
-
- Inputs:
- symbol_table - The symbol table to create the symbol in
- loc - The location to assign to the symbol
- type - The type of symbol to create
- static_lifetime - Whether the symbol should have a static lifetime
- prefix - The prefix to use for the symbol's basename
-
- Outputs: Returns a reference to the new symbol
-
- Purpose: Create a new temporary static symbol
-
-\*******************************************************************/
-
+/// 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
+/// \param type: The type of symbol to create
+/// \param static_lifetime: Whether the symbol should have a static lifetime
+/// \param prefix: The prefix to use for the symbol's basename
+/// \return Returns a reference to the new symbol
static const symbolt &c_new_tmp_symbol(
symbol_tablet &symbol_table,
const source_locationt &loc,
@@ -58,19 +51,8 @@ static const symbolt &c_new_tmp_symbol(
return tmp_symbol;
}
-/*******************************************************************\
-
-Function: c_get_nondet_bool
-
- Inputs:
- type - Desired type (C_bool or plain bool)
-
- Outputs: nondet expr of that type
-
- Purpose:
-
-\*******************************************************************/
-
+/// \param type: Desired type (C_bool or plain bool)
+/// \return nondet expr of that type
static exprt c_get_nondet_bool(const typet &type)
{
// We force this to 0 and 1 and won't consider other values
@@ -107,23 +89,14 @@ class symbol_factoryt
void gen_nondet_init(code_blockt &assignments, const exprt &expr);
};
-/*******************************************************************\
-
-Function: symbol_factoryt::allocate_object
-
- Inputs:
- assignments - The code block to add code to
- target_expr - The expression which we are allocating a symbol for
- allocate_type - The type to use for the symbol. If this doesn't match
- target_expr then a cast will be used for the assignment
- static_lifetime - Whether the symbol created should have static lifetime
-
- Outputs: Returns the address of the allocated symbol
-
- Purpose: Create a symbol for a pointer to point to
-
-\*******************************************************************/
-
+/// Create a symbol for a pointer to point to
+/// \param assignments: The code block to add code to
+/// \param target_expr: The expression which we are allocating a symbol for
+/// \param allocate_type: The type to use for the symbol. If this doesn't match
+/// target_expr then a cast will be used for the assignment
+/// \param static_lifetime: Whether the symbol created should have static
+/// lifetime
+/// \return Returns the address of the allocated symbol
exprt symbol_factoryt::allocate_object(
code_blockt &assignments,
const exprt &target_expr,
@@ -157,21 +130,11 @@ exprt symbol_factoryt::allocate_object(
return aoe;
}
-/*******************************************************************\
-
-Function: symbol_factoryt::gen_nondet_init
-
- Inputs:
- assignments - The code block to add code to
- expr - The expression which we are generating a non-determinate value for
-
- Outputs:
-
- Purpose: Creates a nondet for expr, including calling itself recursively to
- make appropriate symbols to point to if expr is a pointer.
-
-\*******************************************************************/
-
+/// Creates a nondet for expr, including calling itself recursively to make
+/// appropriate symbols to point to if expr is a pointer.
+/// \param assignments: The code block to add code to
+/// \param expr: The expression which we are generating a non-determinate value
+/// for
void symbol_factoryt::gen_nondet_init(
code_blockt &assignments,
const exprt &expr)
@@ -243,26 +206,16 @@ void symbol_factoryt::gen_nondet_init(
}
}
-/*******************************************************************\
-
-Function: c_nondet_symbol_factory
-
- Inputs:
- init_code - The code block to add generated code to
- symbol_table - The symbol table
- base_name - The name to use for the symbol created
- type - The type for the symbol created
- loc - The location to assign to generated code
- allow_null - Whether to allow a null value when type is a pointer
-
- Outputs: Returns the symbol_exprt for the symbol created
-
- Purpose: Creates a symbol and generates code so that it can vary
- over all possible values for its type. For pointers this
- involves allocating symbols which it can point to.
-
-\*******************************************************************/
-
+/// Creates a symbol and generates code so that it can vary over all possible
+/// values for its type. For pointers this involves allocating symbols which it
+/// can point to.
+/// \param init_code: The code block to add generated code to
+/// \param symbol_table: The symbol table
+/// \param base_name: The name to use for the symbol created
+/// \param type: The type for the symbol created
+/// \param loc: The location to assign to generated code
+/// \param allow_null: Whether to allow a null value when type is a pointer
+/// \return Returns the symbol_exprt for the symbol created
exprt c_nondet_symbol_factory(
code_blockt &init_code,
symbol_tablet &symbol_table,
diff --git a/src/ansi-c/c_nondet_symbol_factory.h b/src/ansi-c/c_nondet_symbol_factory.h
index 8760de6ac55..8d375663e73 100644
--- a/src/ansi-c/c_nondet_symbol_factory.h
+++ b/src/ansi-c/c_nondet_symbol_factory.h
@@ -6,6 +6,9 @@ Author: DiffBlue Limited. All rights reserved.
\*******************************************************************/
+/// \file
+/// C Nondet Symbol Factory
+
#ifndef CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
#define CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp
index 9582d6f3b00..6ff6ec9cb21 100644
--- a/src/ansi-c/c_preprocess.cpp
+++ b/src/ansi-c/c_preprocess.cpp
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include
#include
@@ -21,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include
+#include
#include
#include
#include
@@ -29,7 +31,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include
#include
-#include "c_types.h"
#include "c_preprocess.h"
#define GCC_DEFINES_16 \
@@ -96,18 +97,7 @@ Author: Daniel Kroening, kroening@kroening.com
" -D__INTPTR_TYPE__=\"long long int\""\
" -D__UINTPTR_TYPE__=\"long long unsigned int\""
-/*******************************************************************\
-
-Function: type_max
-
- Inputs:
-
- Outputs:
-
- Purpose: produce a string with the maximum value of a given type
-
-\*******************************************************************/
-
+/// produce a string with the maximum value of a given type
static std::string type_max(const typet &src)
{
if(src.id()==ID_signedbv)
@@ -120,18 +110,7 @@ static std::string type_max(const typet &src)
assert(false);
}
-/*******************************************************************\
-
-Function: shell_quote
-
- Inputs:
-
- Outputs:
-
- Purpose: quote a string for bash and CMD
-
-\*******************************************************************/
-
+/// quote a string for bash and CMD
static std::string shell_quote(const std::string &src)
{
#ifdef _WIN32
@@ -205,18 +184,6 @@ static std::string shell_quote(const std::string &src)
#endif
}
-/*******************************************************************\
-
-Function: error_parse_line
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
static void error_parse_line(
const std::string &line,
bool warning_only,
@@ -337,18 +304,6 @@ static void error_parse_line(
m << error_msg << messaget::eom;
}
-/*******************************************************************\
-
-Function: error_parse
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
static void error_parse(
std::istream &errors,
bool warning_only,
@@ -360,18 +315,7 @@ static void error_parse(
error_parse_line(line, warning_only, message);
}
-/*******************************************************************\
-
-Function: c_preprocess
-
- Inputs:
-
- Outputs:
-
- Purpose: ANSI-C preprocessing
-
-\*******************************************************************/
-
+/// ANSI-C preprocessing
bool c_preprocess(
std::istream &instream,
std::ostream &outstream,
@@ -397,18 +341,7 @@ bool c_preprocess(
return result;
}
-/*******************************************************************\
-
-Function: is_dot_i_file
-
- Inputs:
-
- Outputs:
-
- Purpose: ANSI-C preprocessing
-
-\*******************************************************************/
-
+/// ANSI-C preprocessing
static bool is_dot_i_file(const std::string &path)
{
const char *ext=strrchr(path.c_str(), '.');
@@ -420,18 +353,7 @@ static bool is_dot_i_file(const std::string &path)
return false;
}
-/*******************************************************************\
-
-Function: c_preprocess
-
- Inputs:
-
- Outputs:
-
- Purpose: ANSI-C preprocessing
-
-\*******************************************************************/
-
+/// ANSI-C preprocessing
bool c_preprocess_codewarrior(
const std::string &, std::ostream &, message_handlert &);
bool c_preprocess_arm(
@@ -480,18 +402,7 @@ bool c_preprocess(
return true;
}
-/*******************************************************************\
-
-Function: c_preprocess_visual_studio
-
- Inputs:
-
- Outputs:
-
- Purpose: ANSI-C preprocessing
-
-\*******************************************************************/
-
+/// ANSI-C preprocessing
bool c_preprocess_visual_studio(
const std::string &file,
std::ostream &outstream,
@@ -598,18 +509,7 @@ bool c_preprocess_visual_studio(
return false;
}
-/*******************************************************************\
-
-Function: postprocess_codewarrior
-
- Inputs:
-
- Outputs:
-
- Purpose: post-processing specifically for CodeWarrior
-
-\*******************************************************************/
-
+/// post-processing specifically for CodeWarrior
void postprocess_codewarrior(
std::istream &instream,
std::ostream &outstream)
@@ -645,18 +545,7 @@ void postprocess_codewarrior(
}
}
-/*******************************************************************\
-
-Function: c_preprocess_codewarrior
-
- Inputs:
-
- Outputs:
-
- Purpose: ANSI-C preprocessing
-
-\*******************************************************************/
-
+/// ANSI-C preprocessing
bool c_preprocess_codewarrior(
const std::string &file,
std::ostream &outstream,
@@ -729,18 +618,7 @@ bool c_preprocess_codewarrior(
return false;
}
-/*******************************************************************\
-
-Function: c_preprocess_gcc_clang
-
- Inputs:
-
- Outputs:
-
- Purpose: ANSI-C preprocessing
-
-\*******************************************************************/
-
+/// ANSI-C preprocessing
bool c_preprocess_gcc_clang(
const std::string &file,
std::ostream &outstream,
@@ -1044,18 +922,7 @@ bool c_preprocess_gcc_clang(
return false;
}
-/*******************************************************************\
-
-Function: c_preprocess_arm
-
- Inputs:
-
- Outputs:
-
- Purpose: ANSI-C preprocessing
-
-\*******************************************************************/
-
+/// ANSI-C preprocessing
bool c_preprocess_arm(
const std::string &file,
std::ostream &outstream,
@@ -1177,18 +1044,7 @@ bool c_preprocess_arm(
return false;
}
-/*******************************************************************\
-
-Function: c_preprocess_none
-
- Inputs:
-
- Outputs:
-
- Purpose: ANSI-C preprocessing
-
-\*******************************************************************/
-
+/// ANSI-C preprocessing
bool c_preprocess_none(
const std::string &file,
std::ostream &outstream,
@@ -1223,18 +1079,7 @@ bool c_preprocess_none(
return false;
}
-/*******************************************************************\
-
-Function: test_c_preprocessor
-
- Inputs:
-
- Outputs:
-
- Purpose: tests ANSI-C preprocessing
-
-\*******************************************************************/
-
+/// tests ANSI-C preprocessing
const char c_test_program[]=
"#include \n"
"\n"
diff --git a/src/ansi-c/c_preprocess.h b/src/ansi-c/c_preprocess.h
index 2a50e0bfa36..bdf273d2775 100644
--- a/src/ansi-c/c_preprocess.h
+++ b/src/ansi-c/c_preprocess.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_C_PREPROCESS_H
#define CPROVER_ANSI_C_C_PREPROCESS_H
diff --git a/src/ansi-c/c_qualifiers.cpp b/src/ansi-c/c_qualifiers.cpp
index 75ca8bf9c05..b4ac5650bf2 100644
--- a/src/ansi-c/c_qualifiers.cpp
+++ b/src/ansi-c/c_qualifiers.cpp
@@ -6,22 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include "c_qualifiers.h"
-/*******************************************************************\
-
-Function: c_qualifierst::as_string
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
std::string c_qualifierst::as_string() const
{
std::string qualifiers;
@@ -50,18 +39,6 @@ std::string c_qualifierst::as_string() const
return qualifiers;
}
-/*******************************************************************\
-
-Function: c_qualifierst::read
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_qualifierst::read(const typet &src)
{
if(src.get_bool(ID_C_constant))
@@ -89,18 +66,6 @@ void c_qualifierst::read(const typet &src)
is_noreturn=true;
}
-/*******************************************************************\
-
-Function: c_qualifierst::write
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_qualifierst::write(typet &dest) const
{
if(is_constant)
@@ -144,18 +109,6 @@ void c_qualifierst::write(typet &dest) const
dest.remove(ID_C_noreturn);
}
-/*******************************************************************\
-
-Function: c_qualifierst::clear
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_qualifierst::clear(typet &dest)
{
dest.remove(ID_C_constant);
@@ -167,18 +120,7 @@ void c_qualifierst::clear(typet &dest)
dest.remove(ID_C_noreturn);
}
-/*******************************************************************\
-
-Function: operator <<
-
- Inputs:
-
- Outputs:
-
- Purpose: pretty-print the qualifiers
-
-\*******************************************************************/
-
+/// pretty-print the qualifiers
std::ostream &operator << (
std::ostream &out,
const c_qualifierst &c_qualifiers)
diff --git a/src/ansi-c/c_qualifiers.h b/src/ansi-c/c_qualifiers.h
index 45e5d01d782..2e9948e31e9 100644
--- a/src/ansi-c/c_qualifiers.h
+++ b/src/ansi-c/c_qualifiers.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_C_QUALIFIERS_H
#define CPROVER_ANSI_C_C_QUALIFIERS_H
diff --git a/src/ansi-c/c_sizeof.cpp b/src/ansi-c/c_sizeof.cpp
index 85c91870208..63518a5db36 100644
--- a/src/ansi-c/c_sizeof.cpp
+++ b/src/ansi-c/c_sizeof.cpp
@@ -6,6 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// Conversion of sizeof Expressions
+
+#include
#include
#include
#include
@@ -13,19 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "c_sizeof.h"
#include "c_typecast.h"
-#include "c_types.h"
-
-/*******************************************************************\
-
-Function: c_sizeoft::sizeof_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
exprt c_sizeoft::sizeof_rec(const typet &type)
{
@@ -258,18 +249,6 @@ exprt c_sizeoft::sizeof_rec(const typet &type)
return dest;
}
-/*******************************************************************\
-
-Function: c_sizeoft::c_offsetof
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt c_sizeoft::c_offsetof(
const struct_typet &type,
const irep_idt &component_name)
@@ -320,18 +299,6 @@ exprt c_sizeoft::c_offsetof(
return nil_exprt();
}
-/*******************************************************************\
-
-Function: c_sizeof
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt c_sizeof(const typet &src, const namespacet &ns)
{
c_sizeoft c_sizeof_inst(ns);
@@ -340,18 +307,6 @@ exprt c_sizeof(const typet &src, const namespacet &ns)
return tmp;
}
-/*******************************************************************\
-
-Function: c_offsetof
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt c_offsetof(
const struct_typet &src,
const irep_idt &component_name,
diff --git a/src/ansi-c/c_sizeof.h b/src/ansi-c/c_sizeof.h
index 40329726b75..de5421c0510 100644
--- a/src/ansi-c/c_sizeof.h
+++ b/src/ansi-c/c_sizeof.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_C_SIZEOF_H
#define CPROVER_ANSI_C_C_SIZEOF_H
diff --git a/src/ansi-c/c_storage_spec.cpp b/src/ansi-c/c_storage_spec.cpp
index df4cdb2381c..993a93f724e 100644
--- a/src/ansi-c/c_storage_spec.cpp
+++ b/src/ansi-c/c_storage_spec.cpp
@@ -6,22 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include "c_storage_spec.h"
-/*******************************************************************\
-
-Function: c_storage_spect::read
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_storage_spect::read(const typet &type)
{
if(type.id()==ID_merged_type ||
diff --git a/src/ansi-c/c_storage_spec.h b/src/ansi-c/c_storage_spec.h
index d735e578426..5b392fe4d05 100644
--- a/src/ansi-c/c_storage_spec.h
+++ b/src/ansi-c/c_storage_spec.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_C_STORAGE_SPEC_H
#define CPROVER_ANSI_C_C_STORAGE_SPEC_H
@@ -76,7 +77,13 @@ class c_storage_spect
is_register |=other.is_register;
is_inline |=other.is_inline;
is_thread_local |=other.is_thread_local;
- // attributes belong to the declarator, don't replace them
+ is_weak |=other.is_weak;
+ if(alias.empty())
+ alias=other.alias;
+ if(asm_label.empty())
+ asm_label=other.asm_label;
+ if(section.empty())
+ section=other.section;
return *this;
}
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 52070e29257..5b60bbda473 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -6,11 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include
#include
+#include
#include
#include
#include
@@ -19,21 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com
#include
#include "c_typecast.h"
-#include "c_types.h"
#include "c_qualifiers.h"
-/*******************************************************************\
-
-Function: c_implicit_typecast
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool c_implicit_typecast(
exprt &expr,
const typet &dest_type,
@@ -44,18 +33,6 @@ bool c_implicit_typecast(
return !c_typecast.errors.empty();
}
-/*******************************************************************\
-
-Function: check_c_implicit_typecast
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool check_c_implicit_typecast(
const typet &src_type,
const typet &dest_type,
@@ -68,18 +45,7 @@ bool check_c_implicit_typecast(
return !c_typecast.errors.empty();
}
-/*******************************************************************\
-
-Function: c_implicit_typecast_arithmetic
-
- Inputs:
-
- Outputs:
-
- Purpose: perform arithmetic prompotions and conversions
-
-\*******************************************************************/
-
+/// perform arithmetic prompotions and conversions
bool c_implicit_typecast_arithmetic(
exprt &expr1, exprt &expr2,
const namespacet &ns)
@@ -89,18 +55,6 @@ bool c_implicit_typecast_arithmetic(
return !c_typecast.errors.empty();
}
-/*******************************************************************\
-
-Function: is_void_pointer
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool is_void_pointer(const typet &type)
{
if(type.id()==ID_pointer)
@@ -114,18 +68,6 @@ bool is_void_pointer(const typet &type)
return false;
}
-/*******************************************************************\
-
-Function: check_c_implicit_typecast
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool check_c_implicit_typecast(
const typet &src_type,
const typet &dest_type)
@@ -308,18 +250,6 @@ bool check_c_implicit_typecast(
return true;
}
-/*******************************************************************\
-
-Function: c_typecastt::follow_with_qualifiers
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
typet c_typecastt::follow_with_qualifiers(const typet &src_type)
{
if(src_type.id()!=ID_symbol)
@@ -344,18 +274,6 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
return result_type;
}
-/*******************************************************************\
-
-Function: c_typecastt::get_c_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
c_typecastt::c_typet c_typecastt::get_c_type(
const typet &type) const
{
@@ -441,18 +359,6 @@ c_typecastt::c_typet c_typecastt::get_c_type(
return OTHER;
}
-/*******************************************************************\
-
-Function: c_typecastt::implicit_typecast_arithmetic
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecastt::implicit_typecast_arithmetic(
exprt &expr,
c_typet c_type)
@@ -499,18 +405,6 @@ void c_typecastt::implicit_typecast_arithmetic(
do_typecast(expr, new_type);
}
-/*******************************************************************\
-
-Function: c_typecastt::implicit_typecast_arithmetic
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
c_typecastt::c_typet c_typecastt::minimum_promotion(
const typet &type) const
{
@@ -544,36 +438,12 @@ c_typecastt::c_typet c_typecastt::minimum_promotion(
return max_type;
}
-/*******************************************************************\
-
-Function: c_typecastt::implicit_typecast_arithmetic
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecastt::implicit_typecast_arithmetic(exprt &expr)
{
c_typet c_type=minimum_promotion(expr.type());
implicit_typecast_arithmetic(expr, c_type);
}
-/*******************************************************************\
-
-Function: c_typecastt::implicit_typecast
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecastt::implicit_typecast(
exprt &expr,
const typet &type)
@@ -588,18 +458,6 @@ void c_typecastt::implicit_typecast(
implicit_typecast_followed(expr, src_type, type_qual, dest_type);
}
-/*******************************************************************\
-
-Function: c_typecastt::implicit_typecast_followed
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecastt::implicit_typecast_followed(
exprt &expr,
const typet &src_type,
@@ -721,18 +579,6 @@ void c_typecastt::implicit_typecast_followed(
do_typecast(expr, orig_dest_type);
}
-/*******************************************************************\
-
-Function: c_typecastt::implicit_typecast_arithmetic
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecastt::implicit_typecast_arithmetic(
exprt &expr1,
exprt &expr2)
@@ -847,18 +693,6 @@ void c_typecastt::implicit_typecast_arithmetic(
#endif
}
-/*******************************************************************\
-
-Function: c_typecastt::do_typecast
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
{
// special case: array -> pointer is actually
diff --git a/src/ansi-c/c_typecast.h b/src/ansi-c/c_typecast.h
index cfc3eb79aa5..56d0c832359 100644
--- a/src/ansi-c/c_typecast.h
+++ b/src/ansi-c/c_typecast.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_C_TYPECAST_H
#define CPROVER_ANSI_C_C_TYPECAST_H
diff --git a/src/ansi-c/c_typecheck_argc_argv.cpp b/src/ansi-c/c_typecheck_argc_argv.cpp
index a528a630042..5b6b11c8c1f 100644
--- a/src/ansi-c/c_typecheck_argc_argv.cpp
+++ b/src/ansi-c/c_typecheck_argc_argv.cpp
@@ -6,22 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Conversion / Type Checking
+
#include
#include "c_typecheck_base.h"
-/*******************************************************************\
-
-Function: c_typecheck_baset::add_argc_argv
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
{
const code_typet::parameterst ¶meters=
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 8597eef3852..74a0f33f962 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Conversion / Type Checking
+
#include
#include
#include
@@ -15,52 +18,16 @@ Author: Daniel Kroening, kroening@kroening.com
#include "type2name.h"
#include "c_storage_spec.h"
-/*******************************************************************\
-
-Function: c_typecheck_baset::to_string
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
std::string c_typecheck_baset::to_string(const exprt &expr)
{
return expr2c(expr, *this);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::to_string
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
std::string c_typecheck_baset::to_string(const typet &type)
{
return type2c(type, *this);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::move_symbol
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::move_symbol(symbolt &symbol, symbolt *&new_symbol)
{
symbol.mode=mode;
@@ -75,18 +42,6 @@ void c_typecheck_baset::move_symbol(symbolt &symbol, symbolt *&new_symbol)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_symbol
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
{
current_symbol_id=symbol.name;
@@ -173,18 +128,6 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_new_symbol
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol)
{
if(symbol.is_parameter)
@@ -210,44 +153,11 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol)
}
else
{
- if(symbol.type.id()==ID_array &&
- to_array_type(symbol.type).size().is_nil() &&
- !symbol.is_type)
- {
- // Insert a new type symbol for the array.
- // We do this because we want a convenient way
- // of adjusting the size of the type later on.
-
- type_symbolt new_symbol(symbol.type);
- new_symbol.name=id2string(symbol.name)+"$type";
- new_symbol.base_name=id2string(symbol.base_name)+"$type";
- new_symbol.location=symbol.location;
- new_symbol.mode=symbol.mode;
- new_symbol.module=symbol.module;
-
- symbol.type=symbol_typet(new_symbol.name);
-
- symbolt *new_sp;
- symbol_table.move(new_symbol, new_sp);
- }
-
// check the initializer
do_initializer(symbol);
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_redefinition_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_redefinition_type(
symbolt &old_symbol,
symbolt &new_symbol)
@@ -331,18 +241,6 @@ void c_typecheck_baset::typecheck_redefinition_type(
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_redefinition_non_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_redefinition_non_type(
symbolt &old_symbol,
symbolt &new_symbol)
@@ -615,18 +513,6 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
// mismatch.
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_function_body
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
{
code_typet &code_type=to_code_type(symbol.type);
@@ -653,7 +539,7 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
p_it++)
{
// may be anonymous
- if(p_it->get_base_name()==irep_idt())
+ if(p_it->get_base_name().empty())
{
irep_idt base_name="#anon"+std::to_string(anon_counter++);
p_it->set_base_name(base_name);
@@ -697,18 +583,6 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::apply_asm_label
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::apply_asm_label(
const irep_idt &asm_label,
symbolt &symbol)
@@ -777,18 +651,6 @@ void c_typecheck_baset::apply_asm_label(
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_declaration
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_declaration(
ansi_c_declarationt &declaration)
{
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index 68191f54fe9..684b0b64edc 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Language Type Checking
+
#ifndef CPROVER_ANSI_C_C_TYPECHECK_BASE_H
#define CPROVER_ANSI_C_C_TYPECHECK_BASE_H
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index dfbac98940c..b02e6c29718 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -6,41 +6,20 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// C Language Type Checking
+
#include
#include
#include "ansi_c_declaration.h"
#include "c_typecheck_base.h"
-/*******************************************************************\
-
-Function: c_typecheck_baset::start_typecheck_code
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::start_typecheck_code()
{
case_is_allowed=break_is_allowed=continue_is_allowed=false;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_code
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_code(codet &code)
{
if(code.id()!=ID_code)
@@ -152,18 +131,6 @@ void c_typecheck_baset::typecheck_code(codet &code)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_asm
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_asm(codet &code)
{
const irep_idt flavor=to_code_asm(code).get_flavor();
@@ -197,18 +164,6 @@ void c_typecheck_baset::typecheck_asm(codet &code)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_assign
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_assign(codet &code)
{
if(code.operands().size()!=2)
@@ -225,18 +180,6 @@ void c_typecheck_baset::typecheck_assign(codet &code)
implicit_typecast(code.op1(), code.op0().type());
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_block
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_block(codet &code)
{
Forall_operands(it, code)
@@ -276,18 +219,6 @@ void c_typecheck_baset::typecheck_block(codet &code)
code.operands().swap(new_ops.operands());
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_break
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_break(codet &code)
{
if(!break_is_allowed)
@@ -298,18 +229,6 @@ void c_typecheck_baset::typecheck_break(codet &code)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_continue
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_continue(codet &code)
{
if(!continue_is_allowed)
@@ -320,18 +239,6 @@ void c_typecheck_baset::typecheck_continue(codet &code)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_decl
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_decl(codet &code)
{
// this comes with 1 operand, which is a declaration
@@ -452,18 +359,6 @@ void c_typecheck_baset::typecheck_decl(codet &code)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::is_complete_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool c_typecheck_baset::is_complete_type(const typet &type) const
{
if(type.id()==ID_incomplete_struct ||
@@ -494,18 +389,6 @@ bool c_typecheck_baset::is_complete_type(const typet &type) const
return true;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expression
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expression(codet &code)
{
if(code.operands().size()!=1)
@@ -520,18 +403,6 @@ void c_typecheck_baset::typecheck_expression(codet &code)
typecheck_expr(op);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_for
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_for(codet &code)
{
if(code.operands().size()!=4)
@@ -623,18 +494,6 @@ void c_typecheck_baset::typecheck_for(codet &code)
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_label
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_label(code_labelt &code)
{
// record the label
@@ -643,18 +502,6 @@ void c_typecheck_baset::typecheck_label(code_labelt &code)
typecheck_code(code.code());
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_switch_case
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_switch_case(code_switch_caset &code)
{
if(code.operands().size()!=2)
@@ -690,18 +537,6 @@ void c_typecheck_baset::typecheck_switch_case(code_switch_caset &code)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_gcc_switch_case_range
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_gcc_switch_case_range(codet &code)
{
if(code.operands().size()!=3)
@@ -727,54 +562,18 @@ void c_typecheck_baset::typecheck_gcc_switch_case_range(codet &code)
implicit_typecast(code.op1(), switch_op_type);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_gcc_local_label
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_gcc_local_label(codet &code)
{
// these are just declarations, e.g.,
// __label__ here, there;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_goto
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_goto(code_gotot &code)
{
// we record the label used
labels_used[code.get_destination()]=code.source_location();
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_gcc_computed_goto
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_gcc_computed_goto(codet &code)
{
if(code.operands().size()!=1)
@@ -800,18 +599,6 @@ void c_typecheck_baset::typecheck_gcc_computed_goto(codet &code)
dest.type()=empty_typet();
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_ifthenelse
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_ifthenelse(code_ifthenelset &code)
{
if(code.operands().size()!=3)
@@ -861,18 +648,6 @@ void c_typecheck_baset::typecheck_ifthenelse(code_ifthenelset &code)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_start_thread
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_start_thread(codet &code)
{
if(code.operands().size()!=1)
@@ -885,23 +660,13 @@ void c_typecheck_baset::typecheck_start_thread(codet &code)
typecheck_code(to_code(code.op0()));
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_return
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_return(codet &code)
{
if(code.operands().empty())
{
- if(follow(return_type).id()!=ID_empty)
+ if(follow(return_type).id()!=ID_empty &&
+ return_type.id()!=ID_constructor &&
+ return_type.id()!=ID_destructor)
{
// gcc doesn't actually complain, it just warns!
// We'll put a zero here, which is dubious.
@@ -941,18 +706,6 @@ void c_typecheck_baset::typecheck_return(codet &code)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_switch
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_switch(code_switcht &code)
{
if(code.operands().size()!=2)
@@ -984,18 +737,6 @@ void c_typecheck_baset::typecheck_switch(code_switcht &code)
switch_op_type=old_switch_op_type;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_while
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_while(code_whilet &code)
{
if(code.operands().size()!=2)
@@ -1031,18 +772,6 @@ void c_typecheck_baset::typecheck_while(code_whilet &code)
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_dowhile
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
{
if(code.operands().size()!=2)
@@ -1078,18 +807,6 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_spec_expr
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_spec_expr(
codet &code,
const irep_idt &spec)
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 5d4788e5145..185c576e401 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -6,9 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Language Type Checking
+
#include
#include
+#include
#include
#include
#include
@@ -19,7 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include
#include
-#include "c_types.h"
#include "c_typecast.h"
#include "c_typecheck_base.h"
#include "c_sizeof.h"
@@ -28,18 +31,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "anonymous_member.h"
#include "padding.h"
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr(exprt &expr)
{
if(expr.id()==ID_already_typechecked)
@@ -58,18 +49,6 @@ void c_typecheck_baset::typecheck_expr(exprt &expr)
typecheck_expr_main(expr);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::add_rounding_mode
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::add_rounding_mode(exprt &expr)
{
for(auto &op : expr.operands())
@@ -104,18 +83,6 @@ void c_typecheck_baset::add_rounding_mode(exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::gcc_types_compatible_p
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool c_typecheck_baset::gcc_types_compatible_p(
const typet &type1,
const typet &type2)
@@ -198,18 +165,6 @@ bool c_typecheck_baset::gcc_types_compatible_p(
return false;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_main
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_main(exprt &expr)
{
if(expr.id()==ID_side_effect)
@@ -459,6 +414,11 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
expr.id()==ID_gcc_asm_clobbered_register)
{
}
+ else if(expr.id()==ID_lshr || expr.id()==ID_ashr ||
+ expr.id()==ID_assign_lshr || expr.id()==ID_assign_ashr)
+ {
+ // already type checked
+ }
else
{
err_location(expr);
@@ -467,18 +427,6 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_comma
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_comma(exprt &expr)
{
if(expr.operands().size()!=2)
@@ -495,18 +443,6 @@ void c_typecheck_baset::typecheck_expr_comma(exprt &expr)
expr.set(ID_C_lvalue, true);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_builtin_va_arg
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
{
// The first parameter is the va_list, and the second
@@ -552,18 +488,6 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
symbol_table.move(symbol);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_cw_va_arg_typeof
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_cw_va_arg_typeof(exprt &expr)
{
// used in Code Warrior via
@@ -581,18 +505,6 @@ void c_typecheck_baset::typecheck_expr_cw_va_arg_typeof(exprt &expr)
expr.type()=signed_int_type();
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_builtin_offsetof
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
{
// these need not be constant, due to array indices!
@@ -754,18 +666,6 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
expr.swap(result);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_operands
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
{
if(expr.id()==ID_side_effect &&
@@ -837,18 +737,6 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_symbol
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
{
irep_idt identifier=to_symbol_expr(expr).get_identifier();
@@ -954,18 +842,6 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_side_effect_statement_expression
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_side_effect_statement_expression(
side_effect_exprt &expr)
{
@@ -1042,18 +918,6 @@ void c_typecheck_baset::typecheck_side_effect_statement_expression(
expr.type()=typet(ID_empty);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_sizeof
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
{
typet type;
@@ -1116,18 +980,6 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_alignof
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_alignof(exprt &expr)
{
typet argument_type;
@@ -1150,18 +1002,6 @@ void c_typecheck_baset::typecheck_expr_alignof(exprt &expr)
expr.swap(tmp);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_typecast
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
{
if(expr.operands().size()!=1)
@@ -1318,8 +1158,8 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
// an integer/float of the same size
if((expr_type.id()==ID_signedbv ||
expr_type.id()==ID_unsignedbv) &&
- pointer_offset_size(expr_type, *this)==
- pointer_offset_size(op_vector_type, *this))
+ pointer_offset_bits(expr_type, *this)==
+ pointer_offset_bits(op_vector_type, *this))
{
}
else
@@ -1354,35 +1194,11 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::make_index_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::make_index_type(exprt &expr)
{
implicit_typecast(expr, index_type());
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_index
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_index(exprt &expr)
{
if(expr.operands().size()!=2)
@@ -1443,18 +1259,6 @@ void c_typecheck_baset::typecheck_expr_index(exprt &expr)
expr.type()=final_array_type.subtype();
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::adjust_float_rel
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::adjust_float_rel(exprt &expr)
{
// equality and disequality on float is not mathematical equality!
@@ -1469,18 +1273,6 @@ void c_typecheck_baset::adjust_float_rel(exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_rel
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_rel(
binary_relation_exprt &expr)
{
@@ -1587,18 +1379,6 @@ void c_typecheck_baset::typecheck_expr_rel(
throw 0;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_rel_vector
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_rel_vector(
binary_relation_exprt &expr)
{
@@ -1625,18 +1405,6 @@ void c_typecheck_baset::typecheck_expr_rel_vector(
expr.type()=vector_typet(signed_int_type(), to_vector_type(o_type0).size());
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_ptrmember
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_ptrmember(exprt &expr)
{
if(expr.operands().size()!=1)
@@ -1672,18 +1440,6 @@ void c_typecheck_baset::typecheck_expr_ptrmember(exprt &expr)
typecheck_expr_member(expr);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_member
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_member(exprt &expr)
{
if(expr.operands().size()!=1)
@@ -1766,7 +1522,7 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr)
// copy method identifier
const irep_idt &identifier=component.get(ID_C_identifier);
- if(identifier!=irep_idt())
+ if(!identifier.empty())
expr.set(ID_C_identifier, identifier);
const irep_idt &access=component.get_access();
@@ -1780,18 +1536,6 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_trinary
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr)
{
exprt::operandst &operands=expr.operands();
@@ -1885,18 +1629,6 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr)
throw 0;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_side_effect_gcc_conditional_expresssion
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(
side_effect_exprt &expr)
{
@@ -1928,18 +1660,6 @@ void c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(
expr.type()=if_expr.type();
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_address_of
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_address_of(exprt &expr)
{
if(expr.operands().size()!=1)
@@ -2010,18 +1730,6 @@ void c_typecheck_baset::typecheck_expr_address_of(exprt &expr)
expr.type()=pointer_type(op.type());
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_dereference
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_dereference(exprt &expr)
{
if(expr.operands().size()!=1)
@@ -2065,18 +1773,6 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr)
typecheck_expr_function_identifier(expr);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_function_identifier
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_function_identifier(exprt &expr)
{
if(expr.type().id()==ID_code)
@@ -2089,18 +1785,6 @@ void c_typecheck_baset::typecheck_expr_function_identifier(exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_side_effect
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
{
const irep_idt &statement=expr.get_statement();
@@ -2192,18 +1876,6 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_side_effect_function_call
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_side_effect_function_call(
side_effect_expr_function_callt &expr)
{
@@ -2312,18 +1984,6 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
typecheck_function_call_arguments(expr);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::do_special_functions
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt c_typecheck_baset::do_special_functions(
side_effect_expr_function_callt &expr)
{
@@ -2473,10 +2133,12 @@ exprt c_typecheck_baset::do_special_functions(
throw 0;
}
- exprt pointer_offset_expr=exprt(ID_pointer_offset, expr.type());
- pointer_offset_expr.operands()=expr.arguments();
+ exprt pointer_offset_expr=pointer_offset(expr.arguments().front());
pointer_offset_expr.add_source_location()=source_location;
+ if(expr.type()!=pointer_offset_expr.type())
+ pointer_offset_expr.make_typecast(expr.type());
+
return pointer_offset_expr;
}
else if(identifier==CPROVER_PREFIX "POINTER_OBJECT")
@@ -2928,18 +2590,8 @@ exprt c_typecheck_baset::do_special_functions(
return nil_exprt();
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_function_call_arguments
-
- Inputs: type-checked arguments, type-checked function
-
- Outputs: type-adjusted function arguments
-
- Purpose:
-
-\*******************************************************************/
-
+/// \param type:checked arguments, type-checked function
+/// \return type-adjusted function arguments
void c_typecheck_baset::typecheck_function_call_arguments(
side_effect_expr_function_callt &expr)
{
@@ -3022,35 +2674,11 @@ void c_typecheck_baset::typecheck_function_call_arguments(
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_constant
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_constant(exprt &expr)
{
// nothing to do
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_unary_arithmetic
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_unary_arithmetic(exprt &expr)
{
if(expr.operands().size()!=1)
@@ -3090,18 +2718,6 @@ void c_typecheck_baset::typecheck_expr_unary_arithmetic(exprt &expr)
throw 0;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_unary_boolean
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_unary_boolean(exprt &expr)
{
if(expr.operands().size()!=1)
@@ -3124,18 +2740,6 @@ void c_typecheck_baset::typecheck_expr_unary_boolean(exprt &expr)
expr.type()=bool_typet();
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::gcc_vector_types_compatible
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
bool c_typecheck_baset::gcc_vector_types_compatible(
const vector_typet &type0,
const vector_typet &type1)
@@ -3163,18 +2767,6 @@ bool c_typecheck_baset::gcc_vector_types_compatible(
return type0.subtype()==type1.subtype();
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_binary_arithmetic
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
{
if(expr.operands().size()!=2)
@@ -3276,18 +2868,6 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
throw 0;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_shifts
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_shifts(shift_exprt &expr)
{
assert(expr.id()==ID_shl || expr.id()==ID_shr);
@@ -3357,18 +2937,6 @@ void c_typecheck_baset::typecheck_expr_shifts(shift_exprt &expr)
throw 0;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_arithmetic_pointer
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr)
{
const typet &type=expr.type();
@@ -3387,18 +2955,6 @@ void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_pointer_arithmetic
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
{
assert(expr.operands().size()==2);
@@ -3489,18 +3045,6 @@ void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
throw 0;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_expr_binary_boolean
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_expr_binary_boolean(exprt &expr)
{
if(expr.operands().size()!=2)
@@ -3522,18 +3066,6 @@ void c_typecheck_baset::typecheck_expr_binary_boolean(exprt &expr)
expr.type()=bool_typet();
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_side_effect_assignment
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_side_effect_assignment(
side_effect_exprt &expr)
{
@@ -3728,18 +3260,6 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
throw 0;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::make_constant
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::make_constant(exprt &expr)
{
make_constant_rec(expr);
@@ -3755,18 +3275,6 @@ void c_typecheck_baset::make_constant(exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::make_constant_index
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::make_constant_index(exprt &expr)
{
make_constant(expr);
@@ -3782,18 +3290,6 @@ void c_typecheck_baset::make_constant_index(exprt &expr)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::make_constant_rec
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::make_constant_rec(exprt &expr)
{
}
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index 79dabc9f0e9..db3280f12a9 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -6,8 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Conversion / Type Checking
+
#include
-#include
+#include
#include
#include
#include
@@ -16,23 +19,10 @@ Author: Daniel Kroening, kroening@kroening.com
#include
-#include "c_types.h"
#include "c_typecheck_base.h"
#include "string_constant.h"
#include "anonymous_member.h"
-/*******************************************************************\
-
-Function: c_typecheck_baset::do_initializer
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::do_initializer(
exprt &initializer,
const typet &type,
@@ -60,19 +50,7 @@ void c_typecheck_baset::do_initializer(
initializer=result;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::do_initializer_rec
-
- Inputs:
-
- Outputs:
-
- Purpose: initialize something of type `type' with given
- value `value'
-
-\*******************************************************************/
-
+/// initialize something of type `type' with given value `value'
exprt c_typecheck_baset::do_initializer_rec(
const exprt &value,
const typet &type,
@@ -230,18 +208,6 @@ exprt c_typecheck_baset::do_initializer_rec(
return result;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::do_initializer
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::do_initializer(symbolt &symbol)
{
// this one doesn't need initialization
@@ -285,18 +251,6 @@ void c_typecheck_baset::do_initializer(symbolt &symbol)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::designator_enter
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::designator_enter(
const typet &type,
designatort &designator)
@@ -394,18 +348,8 @@ void c_typecheck_baset::designator_enter(
designator.push_entry(entry);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::do_designated_initializer
-
- Inputs: pre-initialized result, designator
-
- Outputs: sets result
-
- Purpose:
-
-\*******************************************************************/
-
+/// \param pre:initialized result, designator
+/// \return sets result
void c_typecheck_baset::do_designated_initializer(
exprt &result,
designatort &designator,
@@ -646,18 +590,6 @@ void c_typecheck_baset::do_designated_initializer(
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::increment_designator
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::increment_designator(designatort &designator)
{
assert(!designator.empty());
@@ -706,18 +638,6 @@ void c_typecheck_baset::increment_designator(designatort &designator)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::make_designator
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
designatort c_typecheck_baset::make_designator(
const typet &src_type,
const exprt &src)
@@ -865,18 +785,6 @@ designatort c_typecheck_baset::make_designator(
return designator;
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::do_initializer_list
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
exprt c_typecheck_baset::do_initializer_list(
const exprt &value,
const typet &type,
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index ac3fe7f2928..448df44cef4 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -6,8 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// C++ Language Type Checking
+
#include
+#include
#include
#include
#include
@@ -15,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include
#include "c_typecheck_base.h"
-#include "c_types.h"
#include "c_sizeof.h"
#include "c_qualifiers.h"
#include "ansi_c_declaration.h"
@@ -23,18 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "type2name.h"
#include "ansi_c_convert_type.h"
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_type(typet &type)
{
// we first convert, and then check
@@ -134,39 +125,74 @@ void c_typecheck_baset::typecheck_type(typet &type)
typet result;
if(mode=="__QI__") // 8 bits
- result=is_signed?signed_char_type():unsigned_char_type();
+ if(is_signed)
+ result=signed_char_type();
+ else
+ result=unsigned_char_type();
else if(mode=="__byte__") // 8 bits
- result=is_signed?signed_char_type():unsigned_char_type();
+ if(is_signed)
+ result=signed_char_type();
+ else
+ result=unsigned_char_type();
else if(mode=="__HI__") // 16 bits
- result=is_signed?signed_short_int_type():unsigned_short_int_type();
+ if(is_signed)
+ result=signed_short_int_type();
+ else
+ result=unsigned_short_int_type();
else if(mode=="__SI__") // 32 bits
- result=is_signed?signed_int_type():unsigned_int_type();
+ if(is_signed)
+ result=signed_int_type();
+ else
+ result=unsigned_int_type();
else if(mode=="__word__") // long int, we think
- result=is_signed?signed_long_int_type():unsigned_long_int_type();
+ if(is_signed)
+ result=signed_long_int_type();
+ else
+ result=unsigned_long_int_type();
else if(mode=="__pointer__") // we think this is size_t/ssize_t
- result=is_signed?signed_size_type():size_type();
+ if(is_signed)
+ result=signed_size_type();
+ else
+ result=size_type();
else if(mode=="__DI__") // 64 bits
{
if(config.ansi_c.long_int_width==64)
- result=is_signed?signed_long_int_type():unsigned_long_int_type();
+ if(is_signed)
+ result=signed_long_int_type();
+ else
+ result=unsigned_long_int_type();
else
{
assert(config.ansi_c.long_long_int_width==64);
- result=
- is_signed?signed_long_long_int_type():unsigned_long_long_int_type();
+
+ if(is_signed)
+ result=signed_long_long_int_type();
+ else
+ result=unsigned_long_long_int_type();
}
}
else if(mode=="__TI__") // 128 bits
- result=is_signed?gcc_signed_int128_type():gcc_unsigned_int128_type();
+ if(is_signed)
+ result=gcc_signed_int128_type();
+ else
+ result=gcc_unsigned_int128_type();
else if(mode=="__V2SI__") // vector of 2 ints, deprecated by gcc
- result=
- vector_typet(
- is_signed?signed_int_type():unsigned_int_type(),
+ if(is_signed)
+ result=vector_typet(
+ signed_int_type(),
+ from_integer(2, size_type()));
+ else
+ result=vector_typet(
+ unsigned_int_type(),
from_integer(2, size_type()));
else if(mode=="__V4SI__") // vector of 4 ints, deprecated by gcc
- result=
- vector_typet(
- is_signed?signed_int_type():unsigned_int_type(),
+ if(is_signed)
+ result=vector_typet(
+ signed_int_type(),
+ from_integer(4, size_type()));
+ else
+ result=vector_typet(
+ unsigned_int_type(),
from_integer(4, size_type()));
else // give up, just use subtype
result=type.subtype();
@@ -255,18 +281,6 @@ void c_typecheck_baset::typecheck_type(typet &type)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_custom_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_custom_type(typet &type)
{
// they all have a width
@@ -367,18 +381,6 @@ void c_typecheck_baset::typecheck_custom_type(typet &type)
assert(false);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_code_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_code_type(code_typet &type)
{
// the return type is still 'subtype()'
@@ -426,7 +428,7 @@ void c_typecheck_baset::typecheck_code_type(code_typet &type)
irep_idt identifier=declaration.declarator().get_name();
// abstract or not?
- if(identifier==irep_idt())
+ if(identifier.empty())
{
// abstract
parameter.add_source_location()=declaration.type().source_location();
@@ -478,18 +480,6 @@ void c_typecheck_baset::typecheck_code_type(code_typet &type)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_array_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_array_type(array_typet &type)
{
exprt &size=type.size();
@@ -560,7 +550,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
{
// not a constant and not infinity
- assert(current_symbol_id!=irep_idt());
+ assert(!current_symbol_id.empty());
const symbolt &base_symbol=lookup(current_symbol_id);
@@ -616,18 +606,6 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_vector_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_vector_type(vector_typet &type)
{
exprt &size=type.size();
@@ -709,18 +687,6 @@ void c_typecheck_baset::typecheck_vector_type(vector_typet &type)
type.size()=from_integer(s, signed_size_type());
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_compound_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
{
// These get replaced by symbol types later.
@@ -833,18 +799,6 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
original_qualifiers.write(type);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_compound_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_compound_body(
struct_union_typet &type)
{
@@ -908,7 +862,7 @@ void c_typecheck_baset::typecheck_compound_body(
// scan for anonymous members, and name them
for(auto &member : components)
{
- if(member.get_name()!=irep_idt())
+ if(!member.get_name().empty())
continue;
member.set_name("$anon"+std::to_string(anon_member_counter++));
@@ -1021,18 +975,6 @@ void c_typecheck_baset::typecheck_compound_body(
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::enum_constant_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
typet c_typecheck_baset::enum_constant_type(
const mp_integer &min_value,
const mp_integer &max_value) const
@@ -1065,18 +1007,6 @@ typet c_typecheck_baset::enum_constant_type(
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::enum_underlying_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
typet c_typecheck_baset::enum_underlying_type(
const mp_integer &min_value,
const mp_integer &max_value,
@@ -1135,18 +1065,6 @@ typet c_typecheck_baset::enum_underlying_type(
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_c_enum_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_c_enum_type(typet &type)
{
// These come with the declarations
@@ -1330,18 +1248,6 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
type.set(ID_identifier, identifier);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_c_enum_tag_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_c_enum_tag_type(c_enum_tag_typet &type)
{
// It's just a tag.
@@ -1401,18 +1307,6 @@ void c_typecheck_baset::typecheck_c_enum_tag_type(c_enum_tag_typet &type)
type.set_identifier(identifier);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_c_bit_field_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
{
typecheck_type(type.subtype());
@@ -1493,18 +1387,6 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_typeof_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_typeof_type(typet &type)
{
// save location
@@ -1542,18 +1424,6 @@ void c_typecheck_baset::typecheck_typeof_type(typet &type)
c_qualifiers.write(type);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::typecheck_symbol_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::typecheck_symbol_type(typet &type)
{
const irep_idt &identifier=
@@ -1608,18 +1478,6 @@ void c_typecheck_baset::typecheck_symbol_type(typet &type)
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::adjust_function_parameter
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::adjust_function_parameter(typet &type) const
{
if(type.id()==ID_array)
diff --git a/src/ansi-c/c_typecheck_typecast.cpp b/src/ansi-c/c_typecheck_typecast.cpp
index 5d1cfad1332..62069d90feb 100644
--- a/src/ansi-c/c_typecheck_typecast.cpp
+++ b/src/ansi-c/c_typecheck_typecast.cpp
@@ -6,21 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include "c_typecast.h"
#include "c_typecheck_base.h"
-#include "c_types.h"
-
-/*******************************************************************\
-
-Function: c_typecheck_baset::implicit_typecast
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
void c_typecheck_baset::implicit_typecast(
exprt &expr,
@@ -62,18 +50,6 @@ void c_typecheck_baset::implicit_typecast(
}
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::implicit_typecast_arithmetic
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::implicit_typecast_arithmetic(
exprt &expr1,
exprt &expr2)
@@ -82,18 +58,6 @@ void c_typecheck_baset::implicit_typecast_arithmetic(
c_typecast.implicit_typecast_arithmetic(expr1, expr2);
}
-/*******************************************************************\
-
-Function: c_typecheck_baset::implicit_typecast_arithmetic
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void c_typecheck_baset::implicit_typecast_arithmetic(exprt &expr)
{
c_typecastt c_typecast(*this);
diff --git a/src/ansi-c/c_types.cpp b/src/ansi-c/c_types.cpp
deleted file mode 100644
index 6ba5ddaefb3..00000000000
--- a/src/ansi-c/c_types.cpp
+++ /dev/null
@@ -1,721 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#include
-#include
-
-#include "c_types.h"
-
-/*******************************************************************\
-
-Function: index_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet index_type()
-{
- // same as signed size type
- return signed_size_type();
-}
-
-/*******************************************************************\
-
-Function: enum_constant_type
-
- Inputs:
-
- Outputs:
-
- Purpose: return type of enum constants
-
-\*******************************************************************/
-
-typet enum_constant_type()
-{
- // usually same as 'int',
- // but might be unsigned, or shorter than 'int'
- return signed_int_type();
-}
-
-/*******************************************************************\
-
-Function: signed_int_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet signed_int_type()
-{
- typet result=signedbv_typet(config.ansi_c.int_width);
- result.set(ID_C_c_type, ID_signed_int);
- return result;
-}
-
-/*******************************************************************\
-
-Function: signed_short_int_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet signed_short_int_type()
-{
- typet result=signedbv_typet(config.ansi_c.short_int_width);
- result.set(ID_C_c_type, ID_signed_short_int);
- return result;
-}
-
-/*******************************************************************\
-
-Function: unsigned_int_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet unsigned_int_type()
-{
- typet result=unsignedbv_typet(config.ansi_c.int_width);
- result.set(ID_C_c_type, ID_unsigned_int);
- return result;
-}
-
-/*******************************************************************\
-
-Function: unsigned_short_int_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet unsigned_short_int_type()
-{
- typet result=unsignedbv_typet(config.ansi_c.short_int_width);
- result.set(ID_C_c_type, ID_unsigned_short_int);
- return result;
-}
-
-/*******************************************************************\
-
-Function: size_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet size_type()
-{
- // The size type varies. This is unsigned int on some systems,
- // and unsigned long int on others,
- // and unsigned long long on say Windows 64.
-
- if(config.ansi_c.pointer_width==config.ansi_c.int_width)
- return unsigned_int_type();
- else if(config.ansi_c.pointer_width==config.ansi_c.long_int_width)
- return unsigned_long_int_type();
- else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
- return unsigned_long_long_int_type();
- else
- assert(false); // aaah!
-}
-
-/*******************************************************************\
-
-Function: signed_size_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet signed_size_type()
-{
- // we presume this is the same as pointer difference
- return pointer_diff_type();
-}
-
-/*******************************************************************\
-
-Function: signed_long_int_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet signed_long_int_type()
-{
- typet result=signedbv_typet(config.ansi_c.long_int_width);
- result.set(ID_C_c_type, ID_signed_long_int);
- return result;
-}
-
-/*******************************************************************\
-
-Function: signed_long_long_int_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet signed_long_long_int_type()
-{
- typet result=signedbv_typet(config.ansi_c.long_long_int_width);
- result.set(ID_C_c_type, ID_signed_long_long_int);
- return result;
-}
-
-/*******************************************************************\
-
-Function: unsigned_long_int_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet unsigned_long_int_type()
-{
- typet result=unsignedbv_typet(config.ansi_c.long_int_width);
- result.set(ID_C_c_type, ID_unsigned_long_int);
- return result;
-}
-
-/*******************************************************************\
-
-Function: unsigned_long_long_int_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet unsigned_long_long_int_type()
-{
- typet result=unsignedbv_typet(config.ansi_c.long_long_int_width);
- result.set(ID_C_c_type, ID_unsigned_long_long_int);
- return result;
-}
-
-/*******************************************************************\
-
-Function: c_bool_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet c_bool_type()
-{
- typet result=c_bool_typet(config.ansi_c.bool_width);
- return result;
-}
-
-/*******************************************************************\
-
-Function: char_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet char_type()
-{
- typet result;
-
- // this can be signed or unsigned, depending on the architecture
-
- if(config.ansi_c.char_is_unsigned)
- result=unsignedbv_typet(config.ansi_c.char_width);
- else
- result=signedbv_typet(config.ansi_c.char_width);
-
- // There are 3 char types, i.e., this one is
- // different from either signed char or unsigned char!
-
- result.set(ID_C_c_type, ID_char);
-
- return result;
-}
-
-/*******************************************************************\
-
-Function: unsigned_char_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet unsigned_char_type()
-{
- typet result=unsignedbv_typet(config.ansi_c.char_width);
-
- result.set(ID_C_c_type, ID_unsigned_char);
-
- return result;
-}
-
-/*******************************************************************\
-
-Function: signed_char_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet signed_char_type()
-{
- typet result=signedbv_typet(config.ansi_c.char_width);
-
- result.set(ID_C_c_type, ID_signed_char);
-
- return result;
-}
-
-/*******************************************************************\
-
-Function: wchar_t_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet wchar_t_type()
-{
- typet result;
-
- if(config.ansi_c.wchar_t_is_unsigned)
- result=unsignedbv_typet(config.ansi_c.wchar_t_width);
- else
- result=signedbv_typet(config.ansi_c.wchar_t_width);
-
- result.set(ID_C_c_type, ID_wchar_t);
-
- return result;
-}
-
-/*******************************************************************\
-
-Function: char16_t_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet char16_t_type()
-{
- typet result;
-
- // Types char16_t and char32_t denote distinct types with the same size,
- // signedness, and alignment as uint_least16_t and uint_least32_t,
- // respectively, in , called the underlying types.
- result=unsignedbv_typet(16);
-
- result.set(ID_C_c_type, ID_char16_t);
-
- return result;
-}
-
-/*******************************************************************\
-
-Function: char32_t_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet char32_t_type()
-{
- typet result;
-
- // Types char16_t and char32_t denote distinct types with the same size,
- // signedness, and alignment as uint_least16_t and uint_least32_t,
- // respectively, in , called the underlying types.
- result=unsignedbv_typet(32);
-
- result.set(ID_C_c_type, ID_char32_t);
-
- return result;
-}
-
-/*******************************************************************\
-
-Function: float_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet float_type()
-{
- typet result;
-
- if(config.ansi_c.use_fixed_for_float)
- {
- fixedbv_typet tmp;
- tmp.set_width(config.ansi_c.single_width);
- tmp.set_integer_bits(config.ansi_c.single_width/2);
- result=tmp;
- }
- else
- result=ieee_float_spect::single_precision().to_type();
-
- result.set(ID_C_c_type, ID_float);
-
- return result;
-}
-
-/*******************************************************************\
-
-Function: double_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet double_type()
-{
- typet result;
-
- if(config.ansi_c.use_fixed_for_float)
- {
- fixedbv_typet tmp;
- tmp.set_width(config.ansi_c.double_width);
- tmp.set_integer_bits(config.ansi_c.double_width/2);
- result=tmp;
- }
- else
- result=ieee_float_spect::double_precision().to_type();
-
- result.set(ID_C_c_type, ID_double);
-
- return result;
-}
-
-/*******************************************************************\
-
-Function: long_double_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet long_double_type()
-{
- typet result;
-
- if(config.ansi_c.use_fixed_for_float)
- {
- fixedbv_typet tmp;
- tmp.set_width(config.ansi_c.long_double_width);
- tmp.set_integer_bits(config.ansi_c.long_double_width/2);
- result=tmp;
- }
- else
- {
- if(config.ansi_c.long_double_width==128)
- result=ieee_float_spect::quadruple_precision().to_type();
- else if(config.ansi_c.long_double_width==64)
- result=ieee_float_spect::double_precision().to_type();
- else if(config.ansi_c.long_double_width==80)
- {
- // x86 extended precision has 80 bits in total, and
- // deviating from IEEE, does not use a hidden bit.
- // We use the closest we have got, but the below isn't accurate.
- result=ieee_float_spect(63, 15).to_type();
- }
- else if(config.ansi_c.long_double_width==96)
- {
- result=ieee_float_spect(80, 15).to_type();
- // not quite right. The extra bits beyond 80 are usually padded.
- }
- else
- assert(false);
- }
-
- result.set(ID_C_c_type, ID_long_double);
-
- return result;
-}
-
-/*******************************************************************\
-
-Function: gcc_float128_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet gcc_float128_type()
-{
- typet result;
-
- if(config.ansi_c.use_fixed_for_float)
- {
- fixedbv_typet tmp;
- tmp.set_width(128);
- tmp.set_integer_bits(128/2);
- result=tmp;
- }
- else
- {
- result=ieee_float_spect::quadruple_precision().to_type();
- }
-
- // not same as long double!
- result.set(ID_C_c_type, ID_gcc_float128);
-
- return result;
-}
-
-/*******************************************************************\
-
-Function: pointer_diff_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet pointer_diff_type()
-{
- // The pointer-diff type varies. This is signed int on some systems,
- // and signed long int on others, and signed long long on say Windows.
-
- if(config.ansi_c.pointer_width==config.ansi_c.int_width)
- return signed_int_type();
- else if(config.ansi_c.pointer_width==config.ansi_c.long_int_width)
- return signed_long_int_type();
- else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
- return signed_long_long_int_type();
- else
- assert(false); // aaah!
-}
-
-/*******************************************************************\
-
-Function: pointer_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet pointer_type(const typet &subtype)
-{
- return pointer_typet(subtype);
-}
-
-/*******************************************************************\
-
-Function: void_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet void_type()
-{
- return empty_typet();
-}
-
-/*******************************************************************\
-
-Function: gcc_unsigned_int128_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet gcc_unsigned_int128_type()
-{
- typet result=unsignedbv_typet(128);
- result.set(ID_C_c_type, ID_unsigned_int128);
- return result;
-}
-
-/*******************************************************************\
-
-Function: gcc_signed_int128_type
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typet gcc_signed_int128_type()
-{
- typet result=signedbv_typet(128);
- result.set(ID_C_c_type, ID_signed_int128);
- return result;
-}
-
-/*******************************************************************\
-
-Function: c_type_as_string
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-std::string c_type_as_string(const irep_idt &c_type)
-{
- if(c_type==ID_signed_int)
- return "signed int";
- else if(c_type==ID_signed_short_int)
- return "signed short int";
- else if(c_type==ID_unsigned_int)
- return "unsigned int";
- else if(c_type==ID_unsigned_short_int)
- return "unsigned short int";
- else if(c_type==ID_signed_long_int)
- return "signed long int";
- else if(c_type==ID_signed_long_long_int)
- return "signed long long int";
- else if(c_type==ID_unsigned_long_int)
- return "unsigned long int";
- else if(c_type==ID_unsigned_long_long_int)
- return "unsigned long long int";
- else if(c_type==ID_bool)
- return "_Bool";
- else if(c_type==ID_char)
- return "char";
- else if(c_type==ID_unsigned_char)
- return "unsigned char";
- else if(c_type==ID_signed_char)
- return "signed char";
- else if(c_type==ID_wchar_t)
- return "wchar_t";
- else if(c_type==ID_char16_t)
- return "char16_t";
- else if(c_type==ID_char32_t)
- return "char32_t";
- else if(c_type==ID_float)
- return "float";
- else if(c_type==ID_double)
- return "double";
- else if(c_type==ID_long_double)
- return "long double";
- else if(c_type==ID_gcc_float128)
- return "__float128";
- else if(c_type==ID_unsigned_int128)
- return "unsigned __int128";
- else if(c_type==ID_signed_int128)
- return "signed __int128";
- else
- return "";
-}
diff --git a/src/ansi-c/c_types.h b/src/ansi-c/c_types.h
deleted file mode 100644
index 6c571bd448b..00000000000
--- a/src/ansi-c/c_types.h
+++ /dev/null
@@ -1,47 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#ifndef CPROVER_ANSI_C_C_TYPES_H
-#define CPROVER_ANSI_C_C_TYPES_H
-
-#include
-
-typet index_type();
-typet enum_constant_type();
-typet signed_int_type();
-typet unsigned_int_type();
-typet signed_long_int_type();
-typet signed_short_int_type();
-typet unsigned_short_int_type();
-typet signed_long_long_int_type();
-typet unsigned_long_int_type();
-typet unsigned_long_long_int_type();
-typet c_bool_type();
-typet char_type();
-typet unsigned_char_type();
-typet signed_char_type();
-typet wchar_t_type();
-typet char16_t_type();
-typet char32_t_type();
-typet float_type();
-typet double_type();
-typet long_double_type();
-typet gcc_float128_type();
-typet gcc_unsigned_int128_type();
-typet gcc_signed_int128_type();
-typet size_type();
-typet signed_size_type();
-typet pointer_diff_type();
-typet pointer_type(const typet &);
-typet void_type();
-
-// Turns an ID_C_c_type into a string, e.g.,
-// ID_signed_int gets "signed int".
-std::string c_type_as_string(const irep_idt &);
-
-#endif // CPROVER_ANSI_C_C_TYPES_H
diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp
index 382ec324636..6b7f05af994 100644
--- a/src/ansi-c/cprover_library.cpp
+++ b/src/ansi-c/cprover_library.cpp
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include
@@ -21,18 +22,6 @@ struct cprover_library_entryt
#include "cprover_library.inc"
; // NOLINT(whitespace/semicolon)
-/*******************************************************************\
-
-Function: get_cprover_library_text
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
std::string get_cprover_library_text(
const std::set &functions,
const symbol_tablet &symbol_table)
@@ -74,18 +63,6 @@ std::string get_cprover_library_text(
return library_text.str();
}
-/*******************************************************************\
-
-Function: add_cprover_library
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void add_cprover_library(
const std::set &functions,
symbol_tablet &symbol_table,
@@ -101,18 +78,6 @@ void add_cprover_library(
add_library(library_text, symbol_table, message_handler);
}
-/*******************************************************************\
-
-Function: add_library
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void add_library(
const std::string &src,
symbol_tablet &symbol_table,
diff --git a/src/ansi-c/cprover_library.h b/src/ansi-c/cprover_library.h
index 9b6012cbeef..6f36eb5abca 100644
--- a/src/ansi-c/cprover_library.h
+++ b/src/ansi-c/cprover_library.h
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#ifndef CPROVER_ANSI_C_CPROVER_LIBRARY_H
#define CPROVER_ANSI_C_CPROVER_LIBRARY_H
diff --git a/src/ansi-c/designator.cpp b/src/ansi-c/designator.cpp
index 88657e71407..1d54f11d5f1 100644
--- a/src/ansi-c/designator.cpp
+++ b/src/ansi-c/designator.cpp
@@ -6,22 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Language Type Checking
+
#include
#include "designator.h"
-/*******************************************************************\
-
-Function: designatort::print
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
void designatort::print(std::ostream &out) const
{
for(index_listt::const_iterator it=index_list.begin();
diff --git a/src/ansi-c/designator.h b/src/ansi-c/designator.h
index 019f622ef63..d31d3bb3e66 100644
--- a/src/ansi-c/designator.h
+++ b/src/ansi-c/designator.h
@@ -6,6 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+/// \file
+/// ANSI-C Language Type Checking
+
#ifndef CPROVER_ANSI_C_DESIGNATOR_H
#define CPROVER_ANSI_C_DESIGNATOR_H
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index e8ccb805a76..4f18ea3db29 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
+
#include
#include
#include
@@ -20,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include
#include
+#include