Infrastructure

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

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 (bool) – 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 registered more than once

  • TRLC_Error – if the file is not a rsl, trlc or trlc.md 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

verify_subpackage_distinctness() → bool

Check that sub-package leaf names are sufficiently distinct from types declared in the same parent package.

Must run after RSL parsing, once every package’s symbols table is fully populated with types. Without this, the greedy qualified-name descent (which consults sub_packages first) would silently shadow a same-named member. Objects (declared in TRLC files) are checked separately, once they exist, by verify_subpackage_object_distinctness().

Return type:

bool

verify_subpackage_object_distinctness() → bool

Check that sub-package leaf names are sufficiently distinct from record objects declared in the same parent package.

Must run after TRLC files are parsed, since (unlike types) objects only exist from that point on. Type clashes were already reported by verify_subpackage_distinctness(); this only looks at objects so the same clash is not reported twice.

Return type:

bool