Infrastructure

class trlc.trlc.Source_Manager(mh, lint_mode=True, parse_trlc=True, verify_mode=False, debug_vcg=False, error_recovery=True, cvc5_binary=None)

Bases: object

Dependency and source manager for TRLC.

This is the main entry point when using the Python API. Create an instance of this, register the files you want to look at, and finally call the process method.

Parameters:

  • mh (Message_Handler) – The message handler to use

  • error_recovery (bool) – If true attempts to continue parsing after errors. This may generate weird error messages since it’s impossible to reliably recover the parse context in all cases.

  • lint_mode (bool) – If true enables additional warning messages.

  • verify_mode (bool) – If true performs in-depth static analysis for user-defined checks. Requires CVC5 and PyVCG to be installed.

  • parse_trlc (bool) – If true parses trlc files, otherwise they are ignored.

  • debug_vcg – If true and verify_mode is also true, emit the individual SMTLIB2 VCs and generate a picture of the program graph. Requires Graphviz to be installed.

process()

Parse all registered files.

Returns:

a symbol table (or None if there were any errors)

Return type:

Symbol_Table

register_directory(dir_name)

Schedule a directory tree for parsing.

Parameters:

dir_name – name of the directory

Raises:

  • AssertionError – if the directory does not exist

  • AssertionError – if any item in the directory is already registered

  • TRLC_Error – on any parse errors

Returns:

true if the directory could be registered without issues

Return type:

bool

register_file(file_name, file_content=None, primary=True)

Schedule a file for parsing.

Parameters:

  • file_name (str) – name of the file

  • file_content (str) – content of the file

  • primary (bool) – should be False if the file is a potential include file, and True otherwise.

Raises:

  • AssertionError – if the file does not exist

  • AssertionError – if the file is registed more than once

  • TRLC_Error – if the file is not a rsl/trlc file

  • AssertionError – if the content is not of type string

Returns:

true if the file could be registered without issues

Return type:

bool

register_include(dir_name)

Make contents of a directory available for automatic inclusion

Parameters:

dir_name (str) – name of the directory

Raises:

AssertionError – if dir_name is not a directory