forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request diffblue#454 from diffblue/owen-jones-diffblue/fix…
…-comment-formatting Replace /// with // for non-doxygen comments
- Loading branch information
Showing
3 changed files
with
42 additions
and
42 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -189,12 +189,12 @@ static exprt get_root_object_expr( | |
|
||
if(root_object_symbol.is_static_lifetime) | ||
{ | ||
/// Global variable. Read its actual incoming value set: | ||
// Global variable. Read its actual incoming value set: | ||
return root_object_symbol.symbol_expr(); | ||
} | ||
else | ||
{ | ||
/// Parameter. Get the value-set for the actual argument: | ||
// Parameter. Get the value-set for the actual argument: | ||
size_t paramidx = (size_t)-1; | ||
const auto ¶ms = to_code_type(function_symbol.type).parameters(); | ||
for(size_t i = 0, ilim = params.size(); i != ilim; ++i) | ||
|
@@ -233,11 +233,11 @@ static void follow_access_path( | |
++it) | ||
{ | ||
std::string access_path_label = id2string(it->label()); | ||
/// If expr is of type Z and Z <: Y <: X <: ... <: A and we are | ||
/// accessing a field of A then access_path_label will be | ||
/// ".@Y.@X.@W. ... [email protected]_name". For an array dereference, the access | ||
/// path will have the label "[]", and the access path entry before | ||
/// it will have a label ending in ".data". | ||
// If expr is of type Z and Z <: Y <: X <: ... <: A and we are | ||
// accessing a field of A then access_path_label will be | ||
// ".@Y.@X.@W. ... [email protected]_name". For an array dereference, the access | ||
// path will have the label "[]", and the access path entry before | ||
// it will have a label ending in ".data". | ||
DATA_INVARIANT( | ||
access_path_label.size() >= 2, | ||
"Access path label must have length at least 2"); | ||
|
@@ -274,9 +274,9 @@ static void follow_access_path( | |
return; | ||
} | ||
|
||
/// We should just have a field name. It should not start with a | ||
/// superclass identifier (".@superclass_name") or the special fields | ||
/// ".@class_identifier" or ".@lock" on java.lang.Object. | ||
// We should just have a field name. It should not start with a | ||
// superclass identifier (".@superclass_name") or the special fields | ||
// ".@class_identifier" or ".@lock" on java.lang.Object. | ||
DATA_INVARIANT( | ||
access_path_label[0] == '.' && access_path_label[1] != '@', | ||
"the label of an access path entry is malformed"); | ||
|
@@ -454,7 +454,7 @@ void local_value_set_analysist::transform_function_stub( | |
} | ||
else if(has_prefix(evse_label, PRECISE_EVS_PREFIX)) | ||
{ | ||
/// Precise EVS | ||
// Precise EVS | ||
PRECONDITION(!evse.access_path_entries().empty()); | ||
exprt precise_access_path_expr = | ||
get_expr_from_precise_evs(evse, function_symbol, fcall, ns, *this); | ||
|
@@ -546,7 +546,7 @@ void local_value_set_analysist::transform_function_stub( | |
exprt precise_access_path_expr = get_expr_from_precise_evs( | ||
precise_evs, function_symbol, fcall, ns, *this); | ||
|
||
/// Weak write - can we do strong writes? | ||
// Weak write - can we do strong writes? | ||
bool add_to_sets = true; | ||
const auto &rhs_expr = assignment.second; | ||
auto demoted_rhs_values = pre_call_rhs_value_sets.at(assignment.second); | ||
|
@@ -643,8 +643,8 @@ bool local_value_set_analysist::is_singular(const std::set<exprt> &values) | |
void local_value_set_analysist::operator()(const goto_programt &goto_program) | ||
{ | ||
initialize(goto_program); | ||
/// This is a dummy variable that will always be empty because we handle | ||
/// function calls specially | ||
// This is a dummy variable that will always be empty because we handle | ||
// function calls specially | ||
goto_functionst goto_functions; | ||
|
||
while(true) | ||
|
@@ -672,10 +672,10 @@ bool local_value_set_analysist::add_precise_evs_initializers( | |
|
||
bool any_change = false; | ||
|
||
/// For each precise EVS that was written somewhere in this function, we | ||
/// insert a copy of the EVS with is_initializer set to true to the value-set | ||
/// at the first instruction, to detect on a subsequent fixedpoint analysis | ||
/// whether there are paths where it goes unaltered. | ||
// For each precise EVS that was written somewhere in this function, we | ||
// insert a copy of the EVS with is_initializer set to true to the value-set | ||
// at the first instruction, to detect on a subsequent fixedpoint analysis | ||
// whether there are paths where it goes unaltered. | ||
|
||
for(locationt loc = goto_program.instructions.begin(); | ||
loc != goto_program.instructions.end(); | ||
|