Skip to content

[SV-COMP'18 18/19] Fixing issue 'implicit conversion not permitted' for alias variables. #2007

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed

[SV-COMP'18 18/19] Fixing issue 'implicit conversion not permitted' for alias variables. #2007

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 18 additions & 1 deletion src/ansi-c/c_typecast.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -456,6 +456,23 @@ void c_typecastt::implicit_typecast(
implicit_typecast_followed(expr, src_type, type_qual, dest_type);
}

static bool is_array_element_alias(const namespacet& ns, const symbolt* const orig_symbol, const typet &src_type, const typet &dest_type)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Given the type comparison, you're only looking for strict aliases, right? If so suggest renaming function to reflect that.

{
if(orig_symbol==nullptr)
return false;
const symbolt* aliased_symbol;
if(ns.lookup(orig_symbol->name, aliased_symbol))
return false;
if(!aliased_symbol->is_macro)
return false;
if(src_type.id()!=ID_array)
return false;
const typet &src_subtype=ns.follow(src_type.subtype());
if(src_subtype!=dest_type)
return false;
return true;
}

void c_typecastt::implicit_typecast_followed(
exprt &expr,
const typet &src_type,
Expand Down Expand Up @@ -569,7 +586,7 @@ void c_typecastt::implicit_typecast_followed(
}
}

if(check_c_implicit_typecast(src_type, dest_type))
if(check_c_implicit_typecast(src_type, dest_type) && !is_array_element_alias(ns, get_current_symbol(), src_type, dest_type))
errors.push_back("implicit conversion not permitted");
else if(src_type!=dest_type)
do_typecast(expr, orig_dest_type);
Expand Down
8 changes: 7 additions & 1 deletion src/ansi-c/c_typecast.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ bool c_implicit_typecast_arithmetic(
class c_typecastt
{
public:
explicit c_typecastt(const namespacet &_ns):ns(_ns)
explicit c_typecastt(const namespacet &_ns):ns(_ns), current_symbol(nullptr)
{
}

Expand All @@ -63,6 +63,9 @@ class c_typecastt
std::list<std::string> errors;
std::list<std::string> warnings;

void set_current_symbol(const symbolt * const symbol) { current_symbol=symbol; }
const symbolt *get_current_symbol() const { return current_symbol; }

protected:
const namespacet &ns;

Expand Down Expand Up @@ -100,6 +103,9 @@ class c_typecastt
void do_typecast(exprt &dest, const typet &type);

c_typet minimum_promotion(const typet &type) const;

private:
const symbolt *current_symbol;
};

#endif // CPROVER_ANSI_C_C_TYPECAST_H
1 change: 1 addition & 0 deletions src/ansi-c/c_typecheck_typecast.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ void c_typecheck_baset::implicit_typecast(
const typet &dest_type)
{
c_typecastt c_typecast(*this);
c_typecast.set_current_symbol(&current_symbol);

typet src_type=expr.type();

Expand Down