@@ -189,12 +189,12 @@ static exprt get_root_object_expr(
189
189
190
190
if (root_object_symbol.is_static_lifetime )
191
191
{
192
- // / Global variable. Read its actual incoming value set:
192
+ // Global variable. Read its actual incoming value set:
193
193
return root_object_symbol.symbol_expr ();
194
194
}
195
195
else
196
196
{
197
- // / Parameter. Get the value-set for the actual argument:
197
+ // Parameter. Get the value-set for the actual argument:
198
198
size_t paramidx = (size_t )-1 ;
199
199
const auto ¶ms = to_code_type (function_symbol.type ).parameters ();
200
200
for (size_t i = 0 , ilim = params.size (); i != ilim; ++i)
@@ -233,11 +233,11 @@ static void follow_access_path(
233
233
++it)
234
234
{
235
235
std::string access_path_label = id2string (it->label ());
236
- // / If expr is of type Z and Z <: Y <: X <: ... <: A and we are
237
- // / accessing a field of A then access_path_label will be
238
- // / ".@Y.@X.@W. ... [email protected] _name". For an array dereference, the access
239
- // / path will have the label "[]", and the access path entry before
240
- // / it will have a label ending in ".data".
236
+ // If expr is of type Z and Z <: Y <: X <: ... <: A and we are
237
+ // accessing a field of A then access_path_label will be
238
+ // ".@Y.@X.@W. ... [email protected] _name". For an array dereference, the access
239
+ // path will have the label "[]", and the access path entry before
240
+ // it will have a label ending in ".data".
241
241
DATA_INVARIANT (
242
242
access_path_label.size () >= 2 ,
243
243
" Access path label must have length at least 2" );
@@ -274,9 +274,9 @@ static void follow_access_path(
274
274
return ;
275
275
}
276
276
277
- // / We should just have a field name. It should not start with a
278
- // / superclass identifier (".@superclass_name") or the special fields
279
- // / ".@class_identifier" or ".@lock" on java.lang.Object.
277
+ // We should just have a field name. It should not start with a
278
+ // superclass identifier (".@superclass_name") or the special fields
279
+ // ".@class_identifier" or ".@lock" on java.lang.Object.
280
280
DATA_INVARIANT (
281
281
access_path_label[0 ] == ' .' && access_path_label[1 ] != ' @' ,
282
282
" the label of an access path entry is malformed" );
@@ -454,7 +454,7 @@ void local_value_set_analysist::transform_function_stub(
454
454
}
455
455
else if (has_prefix (evse_label, PRECISE_EVS_PREFIX))
456
456
{
457
- // / Precise EVS
457
+ // Precise EVS
458
458
PRECONDITION (!evse.access_path_entries ().empty ());
459
459
exprt precise_access_path_expr =
460
460
get_expr_from_precise_evs (evse, function_symbol, fcall, ns, *this );
@@ -546,7 +546,7 @@ void local_value_set_analysist::transform_function_stub(
546
546
exprt precise_access_path_expr = get_expr_from_precise_evs (
547
547
precise_evs, function_symbol, fcall, ns, *this );
548
548
549
- // / Weak write - can we do strong writes?
549
+ // Weak write - can we do strong writes?
550
550
bool add_to_sets = true ;
551
551
const auto &rhs_expr = assignment.second ;
552
552
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)
643
643
void local_value_set_analysist::operator ()(const goto_programt &goto_program)
644
644
{
645
645
initialize (goto_program);
646
- // / This is a dummy variable that will always be empty because we handle
647
- // / function calls specially
646
+ // This is a dummy variable that will always be empty because we handle
647
+ // function calls specially
648
648
goto_functionst goto_functions;
649
649
650
650
while (true )
@@ -672,10 +672,10 @@ bool local_value_set_analysist::add_precise_evs_initializers(
672
672
673
673
bool any_change = false ;
674
674
675
- // / For each precise EVS that was written somewhere in this function, we
676
- // / insert a copy of the EVS with is_initializer set to true to the value-set
677
- // / at the first instruction, to detect on a subsequent fixedpoint analysis
678
- // / whether there are paths where it goes unaltered.
675
+ // For each precise EVS that was written somewhere in this function, we
676
+ // insert a copy of the EVS with is_initializer set to true to the value-set
677
+ // at the first instruction, to detect on a subsequent fixedpoint analysis
678
+ // whether there are paths where it goes unaltered.
679
679
680
680
for (locationt loc = goto_program.instructions .begin ();
681
681
loc != goto_program.instructions .end ();
0 commit comments