contracts_wrangler.h File Reference

Parse and annotate contracts. More...

#include <util/message.h>
#include <util/namespace.h>
#include <util/replace_symbol.h>
#include <util/string_utils.h>
#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_model.h>
#include <json/json_parser.h>
#include <regex>

Include dependency graph for contracts_wrangler.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	loop_contracts_clauset
struct	functiont
class	contracts_wranglert

Typedefs
using	functionst = std::list< std::pair< std::regex, functiont > >

Detailed Description

Parse and annotate contracts.

Definition in file contracts_wrangler.h.

Typedef Documentation

functionst

using functionst = std::list<std::pair<std::regex, functiont> >

Definition at line 58 of file contracts_wrangler.h.