sm.h
External header file
smInt.h
Internal header file
smCmd.c
Interface of the sm package with the shell.
smDummyMac.c
This is a hack, i.e. an auxiliary dummy file to make 'ar' work under Mac OS X.
smInit.c
Initializes and ends NuSMV.
smMain.c
Main NuSMV routine. Parses command line at invocation of NuSMV.
smMisc.c
This file contain the main routine for the batch use of NuSMV.
smVers.c
Supplies the compile date and version information.

sm.h

External header file

By: Adapted to NuSMV by Marco Roveri


smInt.h

Internal header file

By: Adapted to NuSMV by Marco Roveri


smCmd.c

Interface of the sm package with the shell.

By: Adapted to NuSMV by Marco Roveri

Interface of the sm package with the shell.

CommandCmdReset()
Implements the reset command.
CommandPrintUsage()
Implements the print_usage command.

smDummyMac.c

This is a hack, i.e. an auxiliary dummy file to make 'ar' work under Mac OS X.

By: Andrei Tchaltsev

Under Mac OS X the source of libnusmv_la_SOURCES (in nusmv/Makefile.am) requires at least one object file. But under Linux, functions of such an object file (specified as the source of libnusmv_la_SOURCES) somehow are not accessible from other files. So, a dummy object file was created and specified as the source of libnusmv_la_SOURCES, and no function from this dummy file is used.


smInit.c

Initializes and ends NuSMV.

By: Adapted to NuSMV by Marco Roveri

Sm_Reset()
Shuts down and restarts the system
Sm_Init()
Calls the initialization routines of all the packages.
Sm_End()
Calls the end routines of all the packages.
init_preprocessors()
Initializes information about the pre-processors avaliable.
get_executable_name()
Given a command, returns the executable file name (with extension if required)
quit_preprocessors()
Removes information regarding the avaliable pre-processors.
get_preprocessor_call()
Gets the command line call for the specified pre-processor name. Returns NULL if given name is not available, or a string that must be NOT freed
get_preprocessor_filename()
Gets the actual program name of the specified pre-processor. Returns NULL if given name is not available, or a string that must be freed
get_preprocessors_num()
Returns the number of available proprocessors
get_preprocessor_names()
Gets the names of the avaliable pre-processors. Returned string must be freed

smMain.c

Main NuSMV routine. Parses command line at invocation of NuSMV.

By: Adapted to NuSMV by Marco Roveri

main()
required
NusmvrcSource()
Sources the .nusmvrc file.
UsagePrint()
Prints the usage of the NuSMV shell interface.
BannerPrint()
Prints the banner of NuSMV.
sm_ParseLineOptions()
Parses the command line options.

smMisc.c

This file contain the main routine for the batch use of NuSMV.

By: Adapted to NuSMV by Marco Roveri

This file contain the main routine for the batch use of NuSMV. The batch main executes the various model checking steps in a predefined order. After the processing of the input file than it return to the calling shell.

smBatchMain()
The batch main.
print_usage()
Prints usage statistic.
restore_nusmv_stdout()
restore_nusmv_stderr()

smVers.c

Supplies the compile date and version information.

By: Adapted to NuSMV by Marco Roveri

Sm_NuSMVReadVersion()
Returns the current NuSMV version.
Sm_NuSMVObtainLibrary()
Returns the NuSMV library path.
Sm_NuSMVInitPrintMore()
Start piping stdout through the "more" command
Sm_NuSMVEndPrintMore()
Stop piping stdout through the "more" command
DateReadFromDateString()
Returns the date in a brief format assuming its coming from the program `date'.

Last updated on 2009/03/04 12h:51