Linking: replace conflicting pointer types when one declaration is extern
This commit is contained in:
parent
3b724a80b3
commit
80ff4e58a8
|
@ -0,0 +1,11 @@
|
|||
#include <stdlib.h>
|
||||
|
||||
void foo();
|
||||
|
||||
int main()
|
||||
{
|
||||
extern void *p;
|
||||
p = malloc(sizeof(int));
|
||||
foo();
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,6 @@
|
|||
int *p;
|
||||
|
||||
void foo()
|
||||
{
|
||||
*p = 42;
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
b.c
|
||||
a.c --pointer-check
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -67,6 +67,15 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
|
|||
// and have static lifetime
|
||||
new_name=root_name;
|
||||
symbol.is_static_lifetime=true;
|
||||
|
||||
if(symbol.value.is_not_nil())
|
||||
{
|
||||
// According to the C standard this should be an error, but at least some
|
||||
// versions of Visual Studio insist to use this in their C library, and
|
||||
// GCC just warns as well.
|
||||
warning().source_location = symbol.value.find_source_location();
|
||||
warning() << "`extern' symbol should not have an initializer" << eom;
|
||||
}
|
||||
}
|
||||
else if(!is_function && symbol.value.id()==ID_code)
|
||||
{
|
||||
|
|
|
@ -216,6 +216,23 @@ exprt goto_symext::address_arithmetic(
|
|||
else
|
||||
result=address_of_exprt(result);
|
||||
}
|
||||
else if(expr.id() == ID_typecast)
|
||||
{
|
||||
const typecast_exprt &tc_expr = to_typecast_expr(expr);
|
||||
|
||||
result = address_arithmetic(tc_expr.op(), state, guard, keep_array);
|
||||
|
||||
// treat &array as &array[0]
|
||||
const typet &expr_type = ns.follow(expr.type());
|
||||
typet dest_type_subtype;
|
||||
|
||||
if(expr_type.id() == ID_array && !keep_array)
|
||||
dest_type_subtype = expr_type.subtype();
|
||||
else
|
||||
dest_type_subtype = expr_type;
|
||||
|
||||
result = typecast_exprt(result, pointer_type(dest_type_subtype));
|
||||
}
|
||||
else
|
||||
throw unsupported_operation_exceptiont(
|
||||
"goto_symext::address_arithmetic does not handle " + expr.id_string());
|
||||
|
|
|
@ -24,6 +24,21 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include "linking_class.h"
|
||||
|
||||
bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
|
||||
{
|
||||
expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
|
||||
|
||||
if(it == expr_map.end())
|
||||
return true;
|
||||
|
||||
const exprt &e = it->second;
|
||||
|
||||
typet type = s.type();
|
||||
static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
std::string linkingt::expr_to_string(
|
||||
const namespacet &ns,
|
||||
const irep_idt &identifier,
|
||||
|
@ -864,6 +879,11 @@ bool linkingt::adjust_object_type_rec(
|
|||
"conflicting pointer types for variable");
|
||||
#endif
|
||||
|
||||
if(info.old_symbol.is_extern && !info.new_symbol.is_extern)
|
||||
{
|
||||
info.set_to_new = true; // store new type
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
else if(t1.id()==ID_array &&
|
||||
|
@ -950,10 +970,10 @@ void linkingt::duplicate_object_symbol(
|
|||
symbolt &new_symbol)
|
||||
{
|
||||
// both are variables
|
||||
bool set_to_new = false;
|
||||
|
||||
if(!base_type_eq(old_symbol.type, new_symbol.type, ns))
|
||||
{
|
||||
bool set_to_new=false;
|
||||
bool failed=
|
||||
adjust_object_type(old_symbol, new_symbol, set_to_new);
|
||||
|
||||
|
@ -1033,6 +1053,14 @@ void linkingt::duplicate_object_symbol(
|
|||
}
|
||||
}
|
||||
}
|
||||
else if(
|
||||
set_to_new && !old_symbol.value.is_nil() &&
|
||||
!old_symbol.value.get_bool(ID_C_zero_initializer))
|
||||
{
|
||||
// the type has been updated, now make sure that the initialising assignment
|
||||
// will have matching types
|
||||
old_symbol.value.make_typecast(old_symbol.type);
|
||||
}
|
||||
}
|
||||
|
||||
void linkingt::duplicate_non_type_symbol(
|
||||
|
|
|
@ -18,6 +18,12 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/typecheck.h>
|
||||
#include <util/std_expr.h>
|
||||
|
||||
class casting_replace_symbolt : public replace_symbolt
|
||||
{
|
||||
private:
|
||||
bool replace_symbol_expr(symbol_exprt &dest) const override;
|
||||
};
|
||||
|
||||
class linkingt:public typecheckt
|
||||
{
|
||||
public:
|
||||
|
@ -35,7 +41,7 @@ public:
|
|||
virtual void typecheck();
|
||||
|
||||
rename_symbolt rename_symbol;
|
||||
unchecked_replace_symbolt object_type_updates;
|
||||
casting_replace_symbolt object_type_updates;
|
||||
|
||||
protected:
|
||||
bool needs_renaming_type(
|
||||
|
|
Loading…
Reference in New Issue