NuSMV/code/nusmv/core/parser/parser.h File Reference

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/node/node.h"

Go to the source code of this file.

Defines
#define	OPT_PARSER_IS_LAX   "parser_is_lax"
	Interface with the parser.
Functions
void	Parser_CloseInput (void)
	Close the input file.
void	Parser_get_syntax_error (node_ptr node, const char **out_filename, int *out_lineno, const char **out_token, const char **out_message)
	Returns information out of nodes contained in list returned by Parser_get_syntax_errors_list.
node_ptr	Parser_get_syntax_errors_list (const NuSMVEnv_ptr env)
	Returns a list of SYNTAX_ERROR nodes.
void	Parser_Init (NuSMVEnv_ptr env)
	Initializes the parser.
void	Parser_OpenInput (const NuSMVEnv_ptr env, const char *filename)
void	Parser_print_syntax_error (node_ptr error, FILE *fout)
	Prints information contained in one node ot the list returned by Parser_get_syntax_errors_list.
void	Parser_Quit (NuSMVEnv_ptr env)
	Deinitializes the parser.
int	Parser_read_model (NuSMVEnv_ptr env, char *ifile)
int	Parser_read_psl_from_file (const NuSMVEnv_ptr env, const char *filename, node_ptr *res)
	Parses a PSL expression from the given file.
int	Parser_read_psl_from_string (const NuSMVEnv_ptr env, int argc, const char **argv, node_ptr *res)
	Parses a PSL expression from the given string.
int	Parser_ReadCmdFromFile (NuSMVEnv_ptr env, const char *filename, node_ptr *res)
	Parse a command expression from file.
int	Parser_ReadCmdFromString (NuSMVEnv_ptr env, int argc, const char **argv, const char *head, const char *tail, node_ptr *pc)
	Parse a comand from a given string.
int	Parser_ReadIdentifierExprFromString (NuSMVEnv_ptr env, const char *str_expr, node_ptr *res)
	Parse an identifier expression from string.
int	Parser_ReadLtlExprFromFile (NuSMVEnv_ptr env, const char *filename)
	Parse LTL expression from a given file.
int	Parser_ReadNextExprFromFile (NuSMVEnv_ptr env, const char *filename, node_ptr *res)
	Parse a next expression from file.
int	Parser_ReadNextExprFromString (NuSMVEnv_ptr env, const char *str_expr, node_ptr *res)
	Parse a next expression from string.
int	Parser_ReadSimpExprFromString (NuSMVEnv_ptr env, const char *str_expr, node_ptr *res)
	Parse a simple expression from string.
int	Parser_ReadSMVFromFile (NuSMVEnv_ptr env, const char *filename)
	Parse SMV code from a given file.
int	Parser_ReadTypeFromString (NuSMVEnv_ptr env, const char *str_type, node_ptr *res)
	Parse a type declaration from string.
int	Parser_skip_multiline_comment (int(*read_function)(void))
	Skips multiline comment during parsing.
int	Parser_skip_one_line_comment (int(*read_function)(void))
	Skips one line comment during parsing.
void	Parser_switch_to_smv (void)

---

Define Documentation

#define OPT_PARSER_IS_LAX   "parser_is_lax"

Interface with the parser.

Author:

Marco Roveri This file describe the interface with the parser. The result of the parsing is stored in a global variable called parsed_tree.

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

void Parser_CloseInput

(

void

)

Close the input file.

Closes the input file and corresponding buffer used by the parser to read tokens. NB: This function should be invoked only after successive invocation of parser_open_input_pp.

See also:

Parser_OpenInput

void Parser_get_syntax_error	(	node_ptr	node,
		const char **	out_filename,
		int *	out_lineno,
		const char **	out_token,
		const char **	out_message
	)

Returns information out of nodes contained in list returned by Parser_get_syntax_errors_list.

Each node contains information which will be set in output params filename, lineno and message. Those information must be NOT modified or freed by the caller. If not interested in an information, pass NULL with the respective parameter.

See also:

Parser_get_syntax_errors_list

node_ptr Parser_get_syntax_errors_list

(

const NuSMVEnv_ptr

env

)

Returns a list of SYNTAX_ERROR nodes.

Each node of the list can be passed to Parser_get_syntax_error to get information out of it. The returned lists must be NOT modified or freed by the caller.

See also:

Parser_get_syntax_error

void Parser_Init

(

NuSMVEnv_ptr

env

)

Initializes the parser.

Initializes the parser

void Parser_OpenInput	(	const NuSMVEnv_ptr	env,
		const char *	filename
	)

Todo:

Missing synopsis

Todo:

Missing description

void Parser_print_syntax_error	(	node_ptr	error,
		FILE *	fout
	)

Prints information contained in one node ot the list returned by Parser_get_syntax_errors_list.

The syntax error information contained in the given node is printed to the given output file.

See also:

Parser_get_syntax_errors_list

void Parser_Quit

(

NuSMVEnv_ptr

env

)

Deinitializes the parser.

Deinitializes the parser

int Parser_read_model	(	NuSMVEnv_ptr	env,
		char *	ifile
	)

Reads a NuSMV file into NuSMV.

int Parser_read_psl_from_file	(	const NuSMVEnv_ptr	env,
		const char *	filename,
		node_ptr *	res
	)

Parses a PSL expression from the given file.

The PSL parser is directly called. The resulting parse tree is returned through res. 1 is returned if an error occurred.

int Parser_read_psl_from_string	(	const NuSMVEnv_ptr	env,
		int	argc,
		const char **	argv,
		node_ptr *	res
	)

Parses a PSL expression from the given string.

The PSL parser is directly called. The resulting parse tree is returned through res. 1 is returned if an error occurred.

int Parser_ReadCmdFromFile	(	NuSMVEnv_ptr	env,
		const char *	filename,
		node_ptr *	res
	)

Parse a command expression from file.

The resulting parse tree is returned through res. If a parsing error occurs then return 1, else return 0.

int Parser_ReadCmdFromString	(	NuSMVEnv_ptr	env,
		int	argc,
		const char **	argv,
		const char *	head,
		const char *	tail,
		node_ptr *	pc
	)

Parse a comand from a given string.

Create a string for a command, and then call nsumv_yyparse to read from the created string. If a parsing error occurs than return 1, else return 0. The result of parsing is stored in pc to be used from the caller.

int Parser_ReadIdentifierExprFromString	(	NuSMVEnv_ptr	env,
		const char *	str_expr,
		node_ptr *	res
	)

Parse an identifier expression from string.

The resulting parse tree is returned through res. If a parsing error occurs then return 1, else return 0.

int Parser_ReadLtlExprFromFile	(	NuSMVEnv_ptr	env,
		const char *	filename
	)

Parse LTL expression from a given file.

Parse SMV code from a given file. If no file is provided, parse from stdin. If a parsing error occurs then return 1, else return 0. The result of parsing is stored in the global variable parsed_tree to be used from the caller.

int Parser_ReadNextExprFromFile	(	NuSMVEnv_ptr	env,
		const char *	filename,
		node_ptr *	res
	)

Parse a next expression from file.

The resulting parse tree is returned through res. If a parsing error occurs then return 1, else return 0.

int Parser_ReadNextExprFromString	(	NuSMVEnv_ptr	env,
		const char *	str_expr,
		node_ptr *	res
	)

Parse a next expression from string.

The resulting parse tree is returned through res. If a parsing error occurs then return 1, else return 0.

int Parser_ReadSimpExprFromString	(	NuSMVEnv_ptr	env,
		const char *	str_expr,
		node_ptr *	res
	)

Parse a simple expression from string.

The resulting parse tree is returned through res. If a parsing error occurs then return 1, else return 0.

int Parser_ReadSMVFromFile	(	NuSMVEnv_ptr	env,
		const char *	filename
	)

Parse SMV code from a given file.

Parse SMV code from a given file. If no file is provided, parse from stdin. If a parsing error occurs then return 1, else return 0. The result of parsing is stored in the global variable parsed_tree to be used from the caller.

int Parser_ReadTypeFromString	(	NuSMVEnv_ptr	env,
		const char *	str_type,
		node_ptr *	res
	)

Parse a type declaration from string.

The resulting parse tree is returned through res. If a parsing error occurs then return 1, else return 0.

E.g. "2..5" will return a ITYPE node containing TWODOTS node. It works with all itypes of the language, i.e. all var types but process and module instances.

int Parser_skip_multiline_comment

(

int(*)(void)

read_function

)

Skips multiline comment during parsing.

Skips multiline comment during parsing

int Parser_skip_one_line_comment

(

int(*)(void)

read_function

)

Skips one line comment during parsing.

Skips one line comment during parsing

void Parser_switch_to_smv

(

void

)

Todo:

Missing synopsis

Todo:

Missing description