dump_loop_contracts.cpp File Reference

Dump Loop Contracts as JSON. More...

#include "dump_loop_contracts.h"
#include <util/json_stream.h>
#include <util/simplify_expr.h>
#include <ansi-c/expr2c.h>

Include dependency graph for dump_loop_contracts.cpp:

Go to the source code of this file.

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.cpp.

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.