replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Add support for STL NOT instruction 

Extends the language subset of Statement List by the NOT instruction,
used for simply negating the current state of the rlo.
This commit is contained in:
Matthias Weiss 2019-07-26 14:50:05 +01:00
parent e01c4b53ec
commit ae6dd2f454
3 changed files with 22 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/statement-list/scanner.l
View File

@ -116,6 +116,7 @@ void statement_list_scanner_init()
CLR { loc(); return TOK_CLR_RLO; }
S { loc(); return TOK_SET; }
R { loc(); return TOK_RESET; }
NOT { loc(); return TOK_NOT; }
A { loc(); return TOK_AND; }
AN { loc(); return TOK_AND_NOT; }
O { loc(); return TOK_OR; }

16
src/statement-list/statement_list_typecheck.cpp
View File

@ -387,6 +387,8 @@ void statement_list_typecheckt::typecheck_statement_list_instruction(
typecheck_statement_list_accu_real_lte(op_code);
else if(ID_statement_list_accu_real_gte == statement)
typecheck_statement_list_accu_real_gte(op_code);
else if(ID_statement_list_not == statement)
typecheck_statement_list_not(op_code);
else if(ID_statement_list_and == statement)
typecheck_statement_list_and(op_code, tia_element);
else if(ID_statement_list_and_not == statement)
@ -753,6 +755,20 @@ void statement_list_typecheckt::typecheck_statement_list_accu_real_gte(
typecheck_accumulator_compare_instruction(ID_ge);
}
void statement_list_typecheckt::typecheck_statement_list_not(
const codet &op_code)
{
typecheck_instruction_without_operand(op_code);
if(fc_bit)
{
const not_exprt unsimplified{rlo_bit};
rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
or_bit = false;
}
else
initialize_bit_expression(false_exprt{});
}
void statement_list_typecheckt::typecheck_statement_list_and(
const codet &op_code,
const symbolt &tia_element)

5
src/statement-list/statement_list_typecheck.h
View File

@ -364,6 +364,11 @@ private:
// Bit Logic instructions
/// Performs a typecheck on a STL boolean NOT instruction. Reads and modifies
/// the RLO, OR and FC bit.
/// \param op_code: OP code of the instruction.
void typecheck_statement_list_not(const codet &op_code);
/// Performs a typecheck on a STL boolean And instruction. Reads and modifies
/// the RLO, OR and FC bit.
/// \param op_code: OP code of the instruction.