Skip to content

Latest commit

 

History

History

cprover

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
CMakeLists.txt
CMakeLists.txt
 
 
Makefile
Makefile
 
 
README.md
README.md
 
 
address_taken.cpp
address_taken.cpp
 
 
address_taken.h
address_taken.h
 
 
axioms.cpp
axioms.cpp
 
 
axioms.h
axioms.h
 
 
bv_pointers_wide.cpp
bv_pointers_wide.cpp
 
 
bv_pointers_wide.h
bv_pointers_wide.h
 
 
c_safety_checks.cpp
c_safety_checks.cpp
 
 
c_safety_checks.h
c_safety_checks.h
 
 
counterexample_found.cpp
counterexample_found.cpp
 
 
counterexample_found.h
counterexample_found.h
 
 
cprover_main.cpp
cprover_main.cpp
 
 
cprover_parse_options.cpp
cprover_parse_options.cpp
 
 
cprover_parse_options.h
cprover_parse_options.h
 
 
endianness_map_wide.cpp
endianness_map_wide.cpp
 
 
endianness_map_wide.h
endianness_map_wide.h
 
 
equality_propagation.cpp
equality_propagation.cpp
 
 
equality_propagation.h
equality_propagation.h
 
 
find_variables.cpp
find_variables.cpp
 
 
find_variables.h
find_variables.h
 
 
flatten_ok_expr.cpp
flatten_ok_expr.cpp
 
 
flatten_ok_expr.h
flatten_ok_expr.h
 
 
format_hooks.cpp
format_hooks.cpp
 
 
format_hooks.h
format_hooks.h
 
 
free_symbols.cpp
free_symbols.cpp
 
 
free_symbols.h
free_symbols.h
 
 
generalization.cpp
generalization.cpp
 
 
generalization.h
generalization.h
 
 
inductiveness.cpp
inductiveness.cpp
 
 
inductiveness.h
inductiveness.h
 
 
instrument_contracts.cpp
instrument_contracts.cpp
 
 
instrument_contracts.h
instrument_contracts.h
 
 
instrument_given_invariants.cpp
instrument_given_invariants.cpp
 
 
instrument_given_invariants.h
instrument_given_invariants.h
 
 
may_alias.cpp
may_alias.cpp
 
 
may_alias.h
may_alias.h
 
 
may_be_same_object.cpp
may_be_same_object.cpp
 
 
may_be_same_object.h
may_be_same_object.h
 
 
module_dependencies.txt
module_dependencies.txt
 
 
propagate.cpp
propagate.cpp
 
 
propagate.h
propagate.h
 
 
report_properties.cpp
report_properties.cpp
 
 
report_properties.h
report_properties.h
 
 
report_traces.cpp
report_traces.cpp
 
 
report_traces.h
report_traces.h
 
 
sentinel_dll.cpp
sentinel_dll.cpp
 
 
sentinel_dll.h
sentinel_dll.h
 
 
simplify_state_expr.cpp
simplify_state_expr.cpp
 
 
simplify_state_expr.h
simplify_state_expr.h
 
 
solver.cpp
solver.cpp
 
 
solver.h
solver.h
 
 
solver_progress.cpp
solver_progress.cpp
 
 
solver_progress.h
solver_progress.h
 
 
solver_types.cpp
solver_types.cpp
 
 
solver_types.h
solver_types.h
 
 
state.cpp
state.cpp
 
 
state.h
state.h
 
 
state_encoding.cpp
state_encoding.cpp
 
 
state_encoding.h
state_encoding.h
 
 
state_encoding_targets.cpp
state_encoding_targets.cpp
 
 
state_encoding_targets.h
state_encoding_targets.h
 
 
variable_encoding.cpp
variable_encoding.cpp
 
 
variable_encoding.h
variable_encoding.h
 
 
wcwidth.c
wcwidth.c
 
 

README.md

\ingroup module_hidden \defgroup cprover cprover

Folder CPROVER

This contains an experimental encoding from C programs into a Constrained Horn Clause (CHC) system. The satisfiability of the CHC system implies that the assertions (as given or generated) hold. The executable performs the encoding and the solving of the CHC system.

The formula generated uses custom operators that model program heaps, including memory allocation, memory deallocation, and pointer dereferencing. Owing to these custom operators, standard CHC solvers are not applicable.

To run the encoding and the solver on aws-c-common and coreJSON, first ensure that the cprover binary is in your PATH. Then perform the following steps.

aws-c-common

git clone https://github.com/kroening/aws-c-common
cd aws-c-common
git checkout cprover
cd verification/cprover
./setup
./script

coreJSON

git clone https://github.com/kroening/coreJSON
cd coreJSON
git checkout cprover
cd test/cprover
./setup
./script