Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help 
GOTO-HARNESS(1) 		  User Commands 		 GOTO-HARNESS(1)

NAME
     goto-harness - Generate environments for symbolic analysis

SYNOPSIS
     goto-harness [-?] [-h] [--help]
	    show help

     goto-harness --version
	    show version

     goto-harness in out --harness-function-name name --harness-type har-
     ness-type [harness-options]
	    build  harness  for  in  and  write  harness  to out; the harness is
	    printed as C code, if out has a .c suffix, else a  GOTO  binary  in-
	    cluding the harness is generated

DESCRIPTION
     goto-harness  constructs  functions  that set up an appropriate environment
     before calling functions under analysis. This is most useful when trying to
     analyze an isolated unit of a program.

     A typical sequence of tool invocations is as follows.  Given  a  C  program
     program.c, we generate a harness for function test_function:

	    # Compile the program
	    goto-cc program.c -o program.gb
	    # Run goto-harness to produce harness file
	    goto-harness --harness-type call-function --harness-function-name generated_harness_test_function
	      --function test_function program.gb harness.c
	    # Run the checks targeting the generated harness
	    cbmc --pointer-check harness.c --function generated_harness_test_function

     goto-harness  has	two  main  modes  of operation. First,function-call har-
     nesses, which automatically synthesize an environment  without  having  any
     information  about the program state. Second, memory-snapshot harnesses, in
     which case goto-harness loads an existing program	state  as  generated  by
     memory-analyzer(1) and selectively havocs some variables.

OPTIONS
     --harness-function-name name
	    Use  name  as  the	name  of the harness function that is generated,
	    i.e., the new entry point.

     --harness-type [call-function|initialize-with-memory-snapshot]
	    Select the type of harness to generate. In addition to  options  ap-
	    plicable to both harness generators, each of them also has dedicated
	    options that are described below.

   Common generator options
     --min-null-tree-depth N
	    Set  the minimum level at which a pointer can first be NULL in a re-
	    cursively non-deterministically initialized struct to N. Defaults to
	    1.

     --max-nondet-tree-depth N
	    Set the maximum height of the non-deterministic object tree to N. At
	    that level, all pointers will be set to NULL. Defaults to 2.

     --min-array-size N
	    Set the minimum size of arrays of non-constant size allocated by the
	    harness to N. Defaults to 1.

     --max-array-size N
	    Set the maximum size of arrays of non-constant size allocated by the
	    harness to N. Defaults to 2.

     --nondet-globals
	    Set global variables to non-deterministic values in harness.

     --havoc-member member-expr
	    Non-deterministically initialize member-expr of some  global  object
	    (may be given multiple times).

     --function-pointer-can-be-null function-name
	    Name  of parameters of the target function or of global variables of
	    function-pointer type that can non-deterministically be set to NULL.

   Function harness generator (--harness-type call-function):
     --function function-name
	    Generate an environment to call function  function-name,  which  the
	    harness will then call.

     --treat-pointer-as-array p
	    Treat  the	(pointer-typed) function parameter with name p as an ar-
	    ray.

     --associated-array-size array_name:size_name
	    Set the function parameter size_name to the size of the array  para-
	    meter array_name (implies --treat-pointer-as-array array_name).

     --treat-pointers-equal p,q,r[;s,t]
	    Assume  the  pointer-typed	function parameters q and r are equal to
	    parameter p, and s equal to t, and so on.

     --treat-pointers-equal-maybe
	    Function parameter equality is non-deterministic.

     --treat-pointer-as-cstring p
	    Treat the function parameter with the name p as a string of  charac-
	    ters.

   Memory   snapshot   harness	generator  (--harness-type  initialise-from-mem-
     ory-snapshot):
     --memory-snapshot file
	    Initialize memory from JSON memory snapshot stored in file.

     --initial-goto-location func[:n]
	    Use function func and GOTO binary location number n as entry point.

     --initial-source-location file:n
	    Use given file name file and line number n in  that  file  as  entry
	    point.

     --havoc-variables vars
	    Non-deterministically initialize all symbols named vars.

     --pointer-as-array p
	    Treat the global pointer with name p as an array.

     --size-of-array array_name:size_name
	    Set  the  variable	size_name  to the size of the array variable ar-
	    ray_name (implies --pointer-as-array array_name).

ENVIRONMENT
     All tools honor the TMPDIR environment variable when  generating  temporary
     files and directories.

BUGS
     If    you	  encounter    a    problem    please	create	 an   issue   at
     https://github.com/diffblue/cbmc/issues

SEE ALSO
     cbmc(1), goto-cc(1), memory-analyzer(1)

COPYRIGHT
     2019, Diffblue

goto-harness-5.59.0		    June 2022			 GOTO-HARNESS(1)

Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=goto-harness&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>

home | help