Skip to content

Commit 7d817e9

Browse files
committed
Added SSA format details
1 parent 5e23ee2 commit 7d817e9

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

customizing.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,11 @@ You can see more grammar examples in the [`code2inv/prog_generator/grammar_files
155155
The name of the checker module (which we shall discuss in the next section) should be in the format of a python package relative to the `code2inv/prog_generator` directory.
156156
For example, if the checker module is `code2inv/prog_generator/checkers/c_inv_checker.py`, the name should be given as `checkers.c_inv_checker`.
157157

158+
### The Variable Format
159+
160+
The variable format must be specified as `ssa` only if the SSA format of variables is used in the input graph, else leave it blank. For example, refer to our
161+
[C benchmarks](benchmarks/C_instances) and our [C specification file](code2inv/prog_generator/specs/c_spec).
162+
158163
## The Checker Module
159164

160165
The checker module is the way Code2Inv verifies if the predicted invariant is correct, and if it is not, then the checker module must return the set of counter examples for that invariant.

0 commit comments

Comments
 (0)