Add well-formedness checks for symbols.
Add a method that checks a symbol for structural validity according to some predetermined rule, and add it as an extra rule for symbol-table validity that each symbol is well-formed.
This commit is contained in:
parent
5f55c339ff
commit
df616e4e1a
|
@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include "source_location.h"
|
||||
#include "std_expr.h"
|
||||
#include "suffix.h"
|
||||
|
||||
/// Dump the state of a symbol object to a given output stream.
|
||||
/// \param out: The stream to output object state to.
|
||||
|
@ -121,3 +122,25 @@ symbol_exprt symbolt::symbol_expr() const
|
|||
{
|
||||
return symbol_exprt(name, type);
|
||||
}
|
||||
|
||||
/// Check that the instance object is well formed.
|
||||
/// \return: true if well-formed; false otherwise.
|
||||
bool symbolt::is_well_formed() const
|
||||
{
|
||||
// Well-formedness criterion number 1 is for a symbol
|
||||
// to have a non-empty mode (see #1880)
|
||||
if(mode.empty())
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
// Well-formedness criterion number 2 is for a symbol
|
||||
// to have it's base name as a suffix to it's more
|
||||
// general name.
|
||||
if(!has_suffix(id2string(name), id2string(base_name)))
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
|
|
@ -121,6 +121,9 @@ public:
|
|||
PRECONDITION(type.id() == ID_code);
|
||||
value = exprt(ID_compiled);
|
||||
}
|
||||
|
||||
/// Check that a symbol is well formed.
|
||||
bool is_well_formed() const;
|
||||
};
|
||||
|
||||
std::ostream &operator<<(std::ostream &out, const symbolt &symbol);
|
||||
|
|
|
@ -128,6 +128,10 @@ void symbol_tablet::validate(const validation_modet vm) const
|
|||
const auto symbol_key = elem.first;
|
||||
const auto &symbol = elem.second;
|
||||
|
||||
// First of all, ensure symbol well-formedness
|
||||
DATA_CHECK_WITH_DIAGNOSTICS(
|
||||
vm, symbol.is_well_formed(), "Symbol is malformed: ", symbol_key);
|
||||
|
||||
// Check that symbols[id].name == id
|
||||
DATA_CHECK_WITH_DIAGNOSTICS(
|
||||
vm,
|
||||
|
|
|
@ -63,6 +63,7 @@ SRC += analyses/ai/ai.cpp \
|
|||
util/string_utils/split_string.cpp \
|
||||
util/string_utils/strip_string.cpp \
|
||||
util/symbol_table.cpp \
|
||||
util/symbol.cpp \
|
||||
util/unicode.cpp \
|
||||
# Empty last line
|
||||
|
||||
|
|
|
@ -22,6 +22,7 @@ SCENARIO(
|
|||
code_typet fun_type2({}, type2);
|
||||
|
||||
symbolt function_symbol;
|
||||
function_symbol.mode = "C";
|
||||
irep_idt function_symbol_name = "foo";
|
||||
function_symbol.name = function_symbol_name;
|
||||
|
||||
|
|
|
@ -0,0 +1,54 @@
|
|||
/// Author: Diffblue Ltd.
|
||||
|
||||
/// \file Tests for symbol_tablet
|
||||
|
||||
#include <testing-utils/catch.hpp>
|
||||
#include <util/exception_utils.h>
|
||||
#include <util/symbol.h>
|
||||
|
||||
SCENARIO(
|
||||
"Constructed symbol validity checks",
|
||||
"[core][utils][symbol__validity_checks]")
|
||||
{
|
||||
GIVEN("A valid symbol")
|
||||
{
|
||||
symbolt symbol;
|
||||
irep_idt symbol_name = "Test_TestBase";
|
||||
symbol.name = symbol_name;
|
||||
symbol.base_name = "TestBase";
|
||||
symbol.module = "TestModule";
|
||||
symbol.mode = "C";
|
||||
|
||||
THEN("Symbol should be well formed")
|
||||
{
|
||||
REQUIRE(symbol.is_well_formed());
|
||||
}
|
||||
}
|
||||
|
||||
GIVEN("An improperly initialised symbol")
|
||||
{
|
||||
symbolt symbol;
|
||||
|
||||
WHEN("The symbol doesn't have a valid mode")
|
||||
{
|
||||
symbol.mode = "";
|
||||
|
||||
THEN("Symbol well-formedness check should fail")
|
||||
{
|
||||
REQUIRE_FALSE(symbol.is_well_formed());
|
||||
}
|
||||
}
|
||||
|
||||
WHEN("The symbol doesn't have base name as a suffix to name")
|
||||
{
|
||||
symbol.name = "TEST";
|
||||
symbol.base_name = "TestBase";
|
||||
symbol.mode = "C";
|
||||
|
||||
THEN("Symbol well-formedness check should fail")
|
||||
{
|
||||
REQUIRE_FALSE(symbol.is_well_formed());
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
|
@ -35,10 +35,11 @@ SCENARIO(
|
|||
symbol_tablet symbol_table;
|
||||
|
||||
symbolt symbol;
|
||||
irep_idt symbol_name = "Test";
|
||||
irep_idt symbol_name = "Test_TestBase";
|
||||
symbol.name = symbol_name;
|
||||
symbol.base_name = "TestBase";
|
||||
symbol.module = "TestModule";
|
||||
symbol.mode = "C";
|
||||
|
||||
symbol_table.insert(symbol);
|
||||
|
||||
|
|
Loading…
Reference in New Issue