cbmc/require__expr_8h_source.html

 /*******************************************************************\


 Module: Unit test utilities


 Author: Diffblue Ltd.


 \*******************************************************************/


 #ifndef CPROVER_TESTING_UTILS_REQUIRE_EXPR_H

 #define CPROVER_TESTING_UTILS_REQUIRE_EXPR_H


 #include <util/std_code.h>


 // NOLINTNEXTLINE(readability/namespace)

 namespace require_expr

 {

   index_exprt require_index(const exprt &expr, int expected_index);

   index_exprt require_top_index(const exprt &expr);


   member_exprt require_member(

     const exprt &expr, const irep_idt &component_identifier);


   symbol_exprt require_symbol(

     const exprt &expr, const irep_idt &symbol_name);


   symbol_exprt require_symbol(const exprt &expr);


   typecast_exprt require_typecast(const exprt &expr);


   side_effect_exprt require_side_effect_expr(

     const exprt &expr,

     const irep_idt &side_effect_statement);

 }


 #endif // CPROVER_TESTING_UTILS_REQUIRE_EXPR_H

dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38

exprt
Base class for all expressions.
Definition: expr.h:56

index_exprt
Array index operator.
Definition: std_expr.h:1465

member_exprt
Extract member of struct or union.
Definition: std_expr.h:2844

side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1450

symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:131

typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2068

require_expr
Definition: require_expr.h:22

require_expr::require_side_effect_expr
side_effect_exprt require_side_effect_expr(const exprt &expr, const irep_idt &side_effect_statement)
Verify a given exprt is a side_effect_exprt with appropriate statement.
Definition: require_expr.cpp:99

require_expr::require_typecast
typecast_exprt require_typecast(const exprt &expr)
Verify a given exprt is a typecast_expr.
Definition: require_expr.cpp:89

require_expr::require_index
index_exprt require_index(const exprt &expr, int expected_index)
Verify a given exprt is an index_exprt with a a constant value equal to the expected value.
Definition: require_expr.cpp:26

require_expr::require_member
member_exprt require_member(const exprt &expr, const irep_idt &component_identifier)
Verify a given exprt is an member_exprt with a component name equal to the component_identifier.
Definition: require_expr.cpp:55

require_expr::require_top_index
index_exprt require_top_index(const exprt &expr)
Verify a given exprt is an index_exprt with a nil value as its index.
Definition: require_expr.cpp:41

require_expr::require_symbol
symbol_exprt require_symbol(const exprt &expr, const irep_idt &symbol_name)
Verify a given exprt is an symbol_exprt with a identifier name equal to the symbol_name.
Definition: require_expr.cpp:69

std_code.h