Skip to content

Latest commit

 

History

History
 
 

goto-harness

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
CMakeLists.txt
CMakeLists.txt
 
 
Makefile
Makefile
 
 
README.md
README.md
 
 
common_harness_generator_options.h
common_harness_generator_options.h
 
 
function_call_harness_generator.cpp
function_call_harness_generator.cpp
 
 
function_call_harness_generator.h
function_call_harness_generator.h
 
 
function_harness_generator_options.h
function_harness_generator_options.h
 
 
goto_harness_generator.cpp
goto_harness_generator.cpp
 
 
goto_harness_generator.h
goto_harness_generator.h
 
 
goto_harness_generator_factory.cpp
goto_harness_generator_factory.cpp
 
 
goto_harness_generator_factory.h
goto_harness_generator_factory.h
 
 
goto_harness_main.cpp
goto_harness_main.cpp
 
 
goto_harness_parse_options.cpp
goto_harness_parse_options.cpp
 
 
goto_harness_parse_options.h
goto_harness_parse_options.h
 
 
memory_snapshot_harness_generator.cpp
memory_snapshot_harness_generator.cpp
 
 
memory_snapshot_harness_generator.h
memory_snapshot_harness_generator.h
 
 
memory_snapshot_harness_generator_options.h
memory_snapshot_harness_generator_options.h
 
 
module_dependencies.txt
module_dependencies.txt
 
 
recursive_initialization.cpp
recursive_initialization.cpp
 
 
recursive_initialization.h
recursive_initialization.h
 
 

README.md

\ingroup module_hidden \defgroup goto-harness goto-harness

Folder goto-harness

goto-harness generates a proof harness for a function under test. It constructs functions that set up an appropriate environment before calling function. This is most useful when trying to analyze an isolated unit of a program.