Structure of Justifications

Justifications consist of a type for referencing the correct counter, followed by a tag and an explanation. Use tags and explanations for your own classification and documentation needs.

A justification looks like:

if (world_still_exists) // CTC++ Justify False | EFFORT: Simulation too expensive, else-branch reviewed instead.

or, inside a justification file, starting with the line number:

182 False | EFFORT: Simulation too expensive, else-branch reviewed instead.

The examples show the common structure of justifications:

type

"False" in example above. Available types are:

True: For true counters in if or loop decisions.
False: For false counters in if or loop decisions.
Function: Whole functions can be justified (Note that this does not refer to unreachable code).
empty: Without a specification, single counters like return or case are referred.
TF-String: For true-false evaluation alternatives in composite decisions. Example: For (a && b) || c, you can justify the combination (F && _) || T with:
```
123 F_T | LOGIC: Contradiction due to variable dependency 
```
You can also use additional _ to match more TF-combinations with one justification.
```
123 __T | EFFORT: Testing c as true is really, really expensive. 
```
will also match (F && _) || T, but also (T && F) || T. For reading convenice, you can use ? instead of _.
FullLine: All counters on the line are justified. This can be useful for complex macro code expanded on one line.

tag

"EFFORT": A short text or tag to categorize justifications according to your requirements. Justification information in overview and detail pages is grouped by these tags.

explanation

"Simulation too expensive...": A long explanation for every justification. This explanation is shown in source code view together with the tag for each justified counter.

Separator | is used between type and short text, and : between tag and explanation.