cprover
refinement Directory Reference
+ Directory dependency graph for refinement:

Files

file  bv_refinement.h [code]
 Abstraction Refinement Loop.
 
file  bv_refinement_loop.cpp [code]
 
file  refine_arithmetic.cpp [code]
 
file  refine_arrays.cpp [code]
 
file  string_builtin_function.cpp [code]
 
file  string_builtin_function.h [code]
 
file  string_constraint.cpp [code]
 
file  string_constraint.h [code]
 Defines string constraints.
 
file  string_constraint_generator.h [code]
 Generates string constraints to link results from string functions with their arguments.
 
file  string_constraint_generator_code_points.cpp [code]
 Generates string constraints for Java functions dealing with code points.
 
file  string_constraint_generator_comparison.cpp [code]
 Generates string constraints for function comparing strings, such as: equals, equalsIgnoreCase, compareTo, hashCode, intern.
 
file  string_constraint_generator_concat.cpp [code]
 Generates string constraints for functions adding content add the end of strings.
 
file  string_constraint_generator_constants.cpp [code]
 Generates string constraints for constant strings.
 
file  string_constraint_generator_float.cpp [code]
 Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool.
 
file  string_constraint_generator_format.cpp [code]
 Generates string constraints for the Java format function.
 
file  string_constraint_generator_indexof.cpp [code]
 Generates string constraints for the family of indexOf and lastIndexOf java functions.
 
file  string_constraint_generator_insert.cpp [code]
 Generates string constraints for the family of insert Java functions.
 
file  string_constraint_generator_main.cpp [code]
 Generates string constraints to link results from string functions with their arguments.
 
file  string_constraint_generator_testing.cpp [code]
 Generates string constraints for string functions that return Boolean values.
 
file  string_constraint_generator_transformation.cpp [code]
 Generates string constraints for string transformations, that is, functions taking one string and returning another.
 
file  string_constraint_generator_valueof.cpp [code]
 Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool.
 
file  string_constraint_instantiation.cpp [code]
 Defines related function for string constraints.
 
file  string_constraint_instantiation.h [code]
 Defines related function for string constraints.
 
file  string_refinement.cpp [code]
 String support via creating string constraints and progressively instantiating the universal constraints as needed.
 
file  string_refinement.h [code]
 String support via creating string constraints and progressively instantiating the universal constraints as needed.
 
file  string_refinement_invariant.h [code]
 
file  string_refinement_util.cpp [code]
 
file  string_refinement_util.h [code]