Commit a308a3da authored by Adéla Štěpková's avatar Adéla Štěpková
Browse files

add README for tests

parent 9c33fdf4
Loading
Loading
Loading
Loading

tests/README.md

0 → 100644
+14 −0
Original line number Diff line number Diff line
# How to run tests

The tests can be run with `python test.py` in this directory. But before running that, the script `test.py` must be modified according to your preferences.

## [Necessary] Specify a path to a verifier

Because a verifier is not a part of this repository, a path to a verifier must be specified according to your local installation. Setting the `default_verifier` variable should be enough.

## [Optional] Add a new verifier

To add a new verifier, a few things are needed.
* add a path to the verifier, as described above
* in the function `run_verifier`, add a command which runs the verifier
* in the function `get_verifier_result`, specify how to parse the verifier output
 No newline at end of file
+6 −1
Original line number Diff line number Diff line
@@ -220,8 +220,11 @@ if __name__ == "__main__":
    output_dir_c = os.path.join(script_file, "./output/c")
    llvm_as_path = "llvm-as-14"
    llvm2c_path = os.path.join(script_file, "../../tools/llvm2c/build/llvm2c") # LLVM IR to C decompiler

    # SPECIFY YOUR VERIFIER PATHS HERE
    symbiotic_path = os.path.join(script_file, "../../tools/symbiotic25/bin/symbiotic") # symbiotic path
    cbmc_path = "cbmc" # cbmc path
    default_verifier = symbiotic_path 

    name_filter = args.name_filter
    show_output = args.show_output
@@ -233,8 +236,10 @@ if __name__ == "__main__":

    if args.cbmc:
        verifier = cbmc_path
    else:
    if args.symbiotic:
        verifier = symbiotic_path
    else:
        verifier = default_verifier

    main(reverser_path, input_dir, output_dir_ll, output_dir_bc, output_dir_c, llvm_as_path, 
         verifier, llvm2c_path, name_filter, show_output, timeout_sec, sv_comp)