Note

You are not reading the most recent version of this documentation.

StandaloneContext

class Cocotec.CocoPlatform.Coco.StandaloneContext : public Cocotec.CocoPlatform.Coco.Context

A Context that allows new modules to be loaded.

Public Functions

StandaloneContext (APIClient client)
void AddImportPath (string directoryPath)

Appends a directory to the back of the list of paths in which imported modules are loaded. This can only be called prior to load_module and only if load_root_package and add_package_dependency are not called.

bool AddPackageDependency (string directoryPath)

Imports a package and makes it available for importing from. This can only be called prior to load_module and only if load_root_package is not called.

void AddPackageSource (string directoryPath)

Appends a directory to the list of directories from which Coco packages can be resolved. This can only be called prior to load_root_package.

bool LoadRootPackage (string directoryPath)

Loads a Coco package, making all modules in the package available for loading. This can only be called prior to the other load methods, since it will affect how all subsequent modules are loaded into this context.

Return
true if an error occured. If an error was raised, a diagnostic will have been reported to this context’s DiagnosticConsumer.
Parameters
  • directoryPath: The path to the directory containing a Coco.toml file to load.

Cocotec.CocoPlatform.Coco.Node LoadModule (string moduleImportPath, Cocotec.CocoPlatform.Coco.ModulePathType modulePathType)

Loads the given module. If this module is already loaded, this will not reload the module.

Parameters
  • moduleImportPath: This should either be a path to the given file relative to one of the import paths, or the name of a module.

Return
The root Coco element. If loading fails this will be an invalid node in which case diagnostics will be reported to this Context’s DiagnosticConsumer.
Parameters
  • modulePathType: The type of the argument to module_import_path.

Cocotec.CocoPlatform.Coco.Node LoadModule (string moduleImportPath)
Cocotec.CocoPlatform.Coco.Node LoadModule (string moduleImportPath, string moduleData)

Loads the given module using the specified data as its contents.

Parameters
  • moduleImportPath: The path to the module in the form of A.B.C (i.e. ModulePathType::ModulePath).

Return
The root Coco element. If loading fails this will be an invalid node in which case diagnostics will be reported to this Context’s DiagnosticConsumer.
Parameters
  • moduleData: The Coco source code for the given module.

List<Cocotec.CocoPlatform.Coco.Node> LoadPackageModules ()

Loads all modules in the package. Requires that load_root_package has been called.

Return
The nodes for each of the modules that are loaded. If any module could not be loaded, then its corresponding node will not be valid.

void AddDiagnosticsConsumer (Cocotec.CocoPlatform.Coco.DiagnosticConsumer consumer)

Adds a diagnostic consumer that will receive diagnostics about errors found about nodes within this Context. The caller is responsible for ensuring that the DiagnosticConsumer remains valid whilst the context is active: the context does not take ownership of the DiagnosticConsumer at all.

Cocotec.CocoPlatform.Coco.Node InternalLoadBinaryModule (string resourceUri, Google.Protobuf.ByteString moduleData)

Internal method: should not be used directly.

string InternalPrintBinaryModule (Google.Protobuf.ByteString moduleData)

Internal method: should not be used directly.

string InternalPrintBinaryModule (Google.Protobuf.ByteString moduleData, string formatSpecification)

Internal method: should not be used directly.

Cocotec.CocoPlatform.Coco.ExportedEmfmodule InternalExportModuleEmf (Cocotec.CocoPlatform.Coco.Node node, string resourceUri)

Internal method: should not be used directly.

Cocotec.CocoPlatform.Coco.Node InternalNodeWithEmfUri (string proxyUri)

Internal method: should not be used directly.

string InternalNodeEmfUri (Cocotec.CocoPlatform.Coco.Node node)

Internal method: should not be used directly.

Cocotec.CocoPlatform.Coco.VerificationAssertion RootAssertion ()

The root assertion for this context.

Cocotec.CocoPlatform.Coco.VerificationAssertion ModuleAssertion (Cocotec.CocoPlatform.Coco.Node moduleNode)

The assertion that corresponds to given module.

void AddVerificationProgressListener (Cocotec.CocoPlatform.Coco.VerificationProgressListener listener)

Adds a verification progress monitor that will receive callbacks about verification events in this Context. The caller is responsible for ensuring that the VerificationProgressListener remains valid whilst the context is active: the context does not take ownership of the VerificationProgressListener at all.

void SetDeterministicCounterexamples (bool deterministicCounterexamples)

Controls whether the verification will be guaranteed to generate counterexamples deterministically. This means that the same input will always give the same result. Note that enabling this may increase verification time.