Well-formedness check for assume and assert instructions
Check that the guard evaluates to a Boolean value.
This commit is contained in:
parent
5aa708a987
commit
909f897449
|
@ -685,8 +685,18 @@ void goto_programt::instructiont::validate(
|
|||
case GOTO:
|
||||
break;
|
||||
case ASSUME:
|
||||
DATA_CHECK_WITH_DIAGNOSTICS(
|
||||
vm,
|
||||
targets.empty(),
|
||||
"assume instruction should not have a target",
|
||||
source_location);
|
||||
break;
|
||||
case ASSERT:
|
||||
DATA_CHECK_WITH_DIAGNOSTICS(
|
||||
vm,
|
||||
targets.empty(),
|
||||
"assert instruction should not have a target",
|
||||
source_location);
|
||||
break;
|
||||
case OTHER:
|
||||
break;
|
||||
|
|
|
@ -538,6 +538,11 @@ inline code_assumet &to_code_assume(codet &code)
|
|||
return static_cast<code_assumet &>(code);
|
||||
}
|
||||
|
||||
inline void validate_expr(const code_assumet &x)
|
||||
{
|
||||
validate_operands(x, 1, "assume must have one operand");
|
||||
}
|
||||
|
||||
/// A non-fatal assertion, which checks a condition then permits execution to
|
||||
/// continue.
|
||||
class code_assertt:public codet
|
||||
|
@ -585,6 +590,11 @@ inline code_assertt &to_code_assert(codet &code)
|
|||
return static_cast<code_assertt &>(code);
|
||||
}
|
||||
|
||||
inline void validate_expr(const code_assertt &x)
|
||||
{
|
||||
validate_operands(x, 1, "assert must have one operand");
|
||||
}
|
||||
|
||||
/// Create a fatal assertion, which checks a condition and then halts if it does
|
||||
/// not hold. Equivalent to `ASSERT(condition); ASSUME(condition)`.
|
||||
///
|
||||
|
|
|
@ -15,6 +15,7 @@ SRC += analyses/ai/ai.cpp \
|
|||
analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
|
||||
analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
|
||||
compound_block_locations.cpp \
|
||||
goto-programs/goto_program_assume.cpp \
|
||||
goto-programs/goto_program_dead.cpp \
|
||||
goto-programs/goto_program_declaration.cpp \
|
||||
goto-programs/goto_trace_output.cpp \
|
||||
|
|
|
@ -0,0 +1,64 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Unit tests for goto_program::validate
|
||||
|
||||
Author: Diffblue Ltd.
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
#include <goto-programs/goto_function.h>
|
||||
#include <testing-utils/catch.hpp>
|
||||
#include <util/arith_tools.h>
|
||||
|
||||
SCENARIO(
|
||||
"Validation of well-formed assert/assume codes",
|
||||
"[core][goto-programs][validate]")
|
||||
{
|
||||
GIVEN("A program with one assumption")
|
||||
{
|
||||
symbol_tablet symbol_table;
|
||||
const typet type1 = signedbv_typet(32);
|
||||
symbolt symbol;
|
||||
irep_idt symbol_name = "a";
|
||||
symbol.name = symbol_name;
|
||||
symbol_exprt varx(symbol_name, type1);
|
||||
exprt val10 = from_integer(10, type1);
|
||||
binary_relation_exprt x_le_10(varx, ID_le, val10);
|
||||
|
||||
goto_functiont goto_function;
|
||||
auto &instructions = goto_function.body.instructions;
|
||||
instructions.emplace_back(goto_program_instruction_typet::ASSUME);
|
||||
|
||||
symbol.type = type1;
|
||||
symbol_table.insert(symbol);
|
||||
namespacet ns(symbol_table);
|
||||
instructions.back().make_assertion(x_le_10);
|
||||
|
||||
WHEN("Instruction has no targets")
|
||||
{
|
||||
THEN("The consistency check succeeds")
|
||||
{
|
||||
goto_function.body.validate(ns, validation_modet::INVARIANT);
|
||||
REQUIRE(true);
|
||||
}
|
||||
}
|
||||
|
||||
WHEN("Instruction has a target")
|
||||
{
|
||||
instructions.back().targets.push_back(instructions.begin());
|
||||
THEN("The consistency check fails")
|
||||
{
|
||||
bool caught = false;
|
||||
try
|
||||
{
|
||||
goto_function.body.validate(ns, validation_modet::EXCEPTION);
|
||||
}
|
||||
catch(incorrect_goto_program_exceptiont &e)
|
||||
{
|
||||
caught = true;
|
||||
}
|
||||
REQUIRE(caught);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
Loading…
Reference in New Issue