dump_loop_contracts.h File Reference

Dump Loop Contracts as JSON. More...

#include "synthesizer_utils.h"
#include <iosfwd>
#include <string>

Include dependency graph for dump_loop_contracts.h:

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

Go to the source code of this file.

Macros
#define	OPT_DUMP_LOOP_CONTRACTS   "(json-output):(dump-loop-contracts)"
#define	HELP_DUMP_LOOP_CONTRACTS

Functions
void	dump_loop_contracts (goto_modelt &goto_model, const std::map< loop_idt, exprt > &invariant_map, const std::map< loop_idt, std::set< exprt > > &assigns_map, const std::string &json_output_str, std::ostream &out)

Detailed Description

Dump Loop Contracts as JSON.

Definition in file dump_loop_contracts.h.

Macro Definition Documentation

HELP_DUMP_LOOP_CONTRACTS

#define HELP_DUMP_LOOP_CONTRACTS

Value:

    " --dump-loop-contracts         dump synthesized loop contracts as JSON\n" /* NOLINT(whitespace/line_length) */ \
    " --json-output <file>          specify the output destination of the dumped loop contracts\n"

Definition at line 30 of file dump_loop_contracts.h.

OPT_DUMP_LOOP_CONTRACTS

#define OPT_DUMP_LOOP_CONTRACTS   "(json-output):(dump-loop-contracts)"

Definition at line 27 of file dump_loop_contracts.h.

Function Documentation

dump_loop_contracts()

void dump_loop_contracts	(	goto_modelt &	goto_model,
		const std::map< loop_idt, exprt > &	invariant_map,
		const std::map< loop_idt, std::set< exprt > > &	assigns_map,
		const std::string &	json_output_str,
		std::ostream &	out
	)

Definition at line 19 of file dump_loop_contracts.cpp.