|
CBMC
|
#include "validate_code.h"#include "goto_instruction_code.h"#include <util/std_code.h>#include <util/validate_helpers.h>
Include dependency graph for validate_code.cpp:Go to the source code of this file.
Macros | |
| #define | CALL_ON_CODE(code_type) C<codet, code_type>()(code, std::forward<Args>(args)...) |
Functions | |
| template<template< typename, typename > class C, typename... Args> | |
| void | call_on_code (const codet &code, Args &&... args) |
| void | check_code (const codet &code, const validation_modet vm) |
| Check that the given code statement is well-formed (shallow checks only, i.e., enclosed statements, subexpressions, etc. More... | |
| void | validate_code (const codet &code, const namespacet &ns, const validation_modet vm) |
| Check that the given code statement is well-formed, assuming that all its enclosed statements, subexpressions, etc. More... | |
| void | validate_full_code (const codet &code, const namespacet &ns, const validation_modet vm) |
| Check that the given code statement is well-formed (full check, including checks of all subexpressions) More... | |
| #define CALL_ON_CODE | ( | code_type | ) | C<codet, code_type>()(code, std::forward<Args>(args)...) |
Definition at line 20 of file validate_code.cpp.
| void call_on_code | ( | const codet & | code, |
| Args &&... | args | ||
| ) |
Definition at line 24 of file validate_code.cpp.
| void check_code | ( | const codet & | code, |
| const validation_modet | vm | ||
| ) |
Check that the given code statement is well-formed (shallow checks only, i.e., enclosed statements, subexpressions, etc.
are not checked)
The function determines the type T of the statement code (by inspecting the id() field) and then calls T::check(code, vm).
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.
Definition at line 70 of file validate_code.cpp.
| void validate_code | ( | const codet & | code, |
| const namespacet & | ns, | ||
| const validation_modet | vm | ||
| ) |
Check that the given code statement is well-formed, assuming that all its enclosed statements, subexpressions, etc.
have already been checked for well-formedness.
The function determines the type T of the statement code (by inspecting the id() field) and then calls T::validate(code, ns, vm).
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.
Definition at line 84 of file validate_code.cpp.
| void validate_full_code | ( | const codet & | code, |
| const namespacet & | ns, | ||
| const validation_modet | vm | ||
| ) |
Check that the given code statement is well-formed (full check, including checks of all subexpressions)
The function determines the type T of the statement code (by inspecting the id() field) and then calls T::validate_full(code, ns, vm).
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.
Definition at line 100 of file validate_code.cpp.