cprover
|
Validation of smt response parse trees to produce either a strongly typed smt_responset
representation, or a set of error messages.
More...
#include <solvers/smt2_incremental/smt_response_validation.h>
#include <util/mp_arith.h>
#include <util/range.h>
#include <regex>
Go to the source code of this file.
Functions | |
template<typename argumentt , typename... argumentst> | |
void | collect_messages_impl (std::vector< std::string > &collected_messages, argumentt &&argument) |
template<typename argumentt , typename... argumentst> | |
void | collect_messages_impl (std::vector< std::string > &collected_messages, argumentt &&argument, argumentst &&... arguments) |
template<typename... argumentst> | |
std::vector< std::string > | collect_messages (argumentst &&... arguments) |
Builds a collection of messages composed all messages in the response_or_errort typed arguments in arguments . | |
template<typename smt_to_constructt , typename smt_baset = smt_to_constructt, typename... argumentst> | |
response_or_errort< smt_baset > | validation_propagating (argumentst &&... arguments) |
Given a class to construct and a set of arguments to its constructor which may include errors, either return the collected errors if there are any or construct the class otherwise. | |
static std::string | print_parse_tree (const irept &parse_tree) |
Produces a human-readable representation of the given parse_tree , for use in error messaging. | |
static response_or_errort< irep_idt > | validate_string_literal (const irept &parse_tree) |
static optionalt< response_or_errort< smt_responset > > | valid_smt_error_response (const irept &parse_tree) |
static bool | all_subs_are_pairs (const irept &parse_tree) |
static response_or_errort< irep_idt > | validate_smt_identifier (const irept &parse_tree) |
static optionalt< smt_termt > | valid_smt_bool (const irept &parse_tree) |
static optionalt< smt_termt > | valid_smt_binary (const std::string &text) |
static optionalt< smt_termt > | valid_smt_hex (const std::string &text) |
static optionalt< smt_termt > | valid_smt_bit_vector_constant (const irept &parse_tree) |
static response_or_errort< smt_termt > | validate_term (const irept &parse_tree) |
static response_or_errort< smt_get_value_responset::valuation_pairt > | validate_valuation_pair (const irept &pair_parse_tree) |
static optionalt< response_or_errort< smt_responset > > | valid_smt_get_value_response (const irept &parse_tree) |
response_or_errort< smt_responset > | validate_smt_response (const irept &parse_tree) |
Validation of smt response parse trees to produce either a strongly typed smt_responset
representation, or a set of error messages.
Functions named with the prefix validate_
require the given parse tree to be a particular kind of sub tree. Functions named with the prefix valid_
are called in places where the exact kind of sub-tree expected is unknown and so the function must determine if the sub-tree is of that type at all, before performing validation of it. These functions will return a response_or_errort
in the case where the parse tree is of that type or an empty optional otherwise.
Definition in file smt_response_validation.cpp.
|
static |
Definition at line 185 of file smt_response_validation.cpp.
std::vector< std::string > collect_messages | ( | argumentst &&... | arguments | ) |
Builds a collection of messages composed all messages in the response_or_errort
typed arguments in arguments
.
This is a templated function in order to handle response_or_errort
instances which are specialised differently.
Definition at line 93 of file smt_response_validation.cpp.
void collect_messages_impl | ( | std::vector< std::string > & | collected_messages, |
argumentt && | argument | ||
) |
Definition at line 66 of file smt_response_validation.cpp.
void collect_messages_impl | ( | std::vector< std::string > & | collected_messages, |
argumentt && | argument, | ||
argumentst &&... | arguments | ||
) |
Definition at line 79 of file smt_response_validation.cpp.
|
static |
Produces a human-readable representation of the given parse_tree
, for use in error messaging.
pretty
, but this function is used instead of calling pretty
directly so that will be more straight forward to replace with an implementation specific to our use case which is more easily readable by users of CBMC. Definition at line 136 of file smt_response_validation.cpp.
Definition at line 215 of file smt_response_validation.cpp.
Definition at line 241 of file smt_response_validation.cpp.
Definition at line 204 of file smt_response_validation.cpp.
|
static |
Definition at line 159 of file smt_response_validation.cpp.
|
static |
Definition at line 279 of file smt_response_validation.cpp.
Definition at line 226 of file smt_response_validation.cpp.
|
static |
Definition at line 194 of file smt_response_validation.cpp.
response_or_errort< smt_responset > validate_smt_response | ( | const irept & | parse_tree | ) |
Definition at line 307 of file smt_response_validation.cpp.
|
static |
Definition at line 142 of file smt_response_validation.cpp.
|
static |
Definition at line 253 of file smt_response_validation.cpp.
|
static |
Definition at line 264 of file smt_response_validation.cpp.
response_or_errort< smt_baset > validation_propagating | ( | argumentst &&... | arguments | ) |
Given a class to construct and a set of arguments to its constructor which may include errors, either return the collected errors if there are any or construct the class otherwise.
smt_to_constructt | The class to construct. |
smt_baset | If the class to construct should be upcast to a base class before being stored in the response_or_errort , then the base class should be supplied in this parameter. If no upcast is required, then this should be left empty. |
argumentst | The pack of argument types matching the constructor of smt_to_constructt . These must each be packed into an instance of response_or_errort . |
Definition at line 118 of file smt_response_validation.cpp.