Skip to content

Commit

Permalink
Replace "bounds_check" by ID_C_bounds_check
Browse files Browse the repository at this point in the history
Replaces the hard-coded string by a dstringt to avoid typos, and also
changes it to a comment: the annotation (communicating from the
front-end to goto_checkt) does not change the semantics of the
expression that has been annotated.
  • Loading branch information
tautschnig committed Mar 2, 2021
1 parent cf88f82 commit 631e7b0
Show file tree
Hide file tree
Showing 4 changed files with 11 additions and 6 deletions.
7 changes: 5 additions & 2 deletions src/analyses/goto_check.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1317,9 +1317,12 @@ void goto_checkt::bounds_check(
if(!enable_bounds_check)
return;

if(expr.find("bounds_check").is_not_nil() &&
!expr.get_bool("bounds_check"))
if(
expr.find(ID_C_bounds_check).is_not_nil() &&
!expr.get_bool(ID_C_bounds_check))
{
return;
}

typet array_type = expr.array().type();

Expand Down
6 changes: 3 additions & 3 deletions src/ansi-c/ansi_c_entry_point.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -407,7 +407,7 @@ bool generate_ansi_c_start_function(
argv_symbol.symbol_expr(), argc_symbol.symbol_expr());

// disable bounds check on that one
index_expr.set("bounds_check", false);
index_expr.set(ID_C_bounds_check, false);

init_code.add(code_assignt(index_expr, null));
}
Expand All @@ -423,7 +423,7 @@ bool generate_ansi_c_start_function(
index_exprt index_expr(
envp_symbol.symbol_expr(), envp_size_symbol.symbol_expr());
// disable bounds check on that one
index_expr.set("bounds_check", false);
index_expr.set(ID_C_bounds_check, false);

equal_exprt is_null(std::move(index_expr), std::move(null));

Expand All @@ -449,7 +449,7 @@ bool generate_ansi_c_start_function(
argv_symbol.symbol_expr(), from_integer(0, index_type()));

// disable bounds check on that one
index_expr.set("bounds_check", false);
index_expr.set(ID_C_bounds_check, false);

const pointer_typet &pointer_type =
to_pointer_type(parameters[1].type());
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/string_abstraction.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -567,7 +567,7 @@ void string_abstractiont::abstract_function_call(

index_exprt idx(str_args.back(), from_integer(0, index_type()));
// disable bounds check on that one
idx.set("bounds_check", false);
idx.set(ID_C_bounds_check, false);

str_args.back()=address_of_exprt(idx);
}
Expand Down
2 changes: 2 additions & 0 deletions src/util/irep_ids.def
Original file line number Diff line number Diff line change
Expand Up @@ -841,6 +841,8 @@ IREP_ID_ONE(statement_list_instructions)
IREP_ID_ONE(max)
IREP_ID_ONE(min)
IREP_ID_ONE(constant_interval)
IREP_ID_TWO(C_bounds_check, #bounds_check)
IREP_ID_ONE(count_leading_zeros)

// Projects depending on this code base that wish to extend the list of
// available ids should provide a file local_irep_ids.def in their source tree
Expand Down

0 comments on commit 631e7b0

Please sign in to comment.