Skip to content

Commit e629a48

Browse files
committed
Updated customizing.md
1 parent 91bad6a commit e629a48

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

customizing.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,7 @@ The checker module is the way Code2Inv verifies if the predicted invariant is co
161161

162162
Examples of the checker module can be found in the [`code2inv/prog_generator/checkers` directory](code2inv/prog_generator/checkers).
163163

164-
There are two functions that must be present in the checker- `inv_checker` and `inv_solver`. `inv_checker` will take the verification condition file name, the invariant string (as produced taking the invariant grammar into account) and a list of `(variable_name, variable_value)` assignment pairs. `inv_checker` will assign the variables their values (any variable in the invariant not in the assignment pair is assigned the value of 1) and evaluate the invariant based on these values, which should either return true or false.
164+
There are two functions that must be present in the checker- `inv_checker` and `inv_solver`. `inv_checker` will take the verification condition file name, the invariant string (as produced taking the invariant grammar into account) and a counter-example given as a list of `(variable_name, variable_value)` assignment pairs. `inv_checker` will assign the variables their values (any variable in the invariant not in the assignment pair is assigned the value of 1) and evaluate the invariant based on these values, which should either return true or false.
165165

166166
`inv_solver` will take the verification condition file name and the invariant string and check if the invariant is correct or not and return a list of 3 elements. The invariant will be checked over the precondition, the loop condition and the post condition in that order. For each check, if the invariant is correct and there is no counter example, the corresponding list element will be `None`. If there is a counter example, the corresponding list element will be a dictionary of counter example variables mapped to their values.
167167

0 commit comments

Comments
 (0)