Contract File Syntax

Attestor allows to manually specify contracts for methods that should not be analysed automatically (for example library functions). The contracts for one method have to be in the same file. Contracts are specified as JSON-objects of the form

{
  "method": String,
  "contracts":[ ContractObject ]
}

• method is the signature of the method in jimple syntax.
• contracts are a JSON-array of ContractObjects specifying pre- and postconditions.

Note: You do not have to provide all possible preconditions if you don't wish to. Attestor will try to create all missing ones automatically. Also you can output contracts generated by Attestor in this input format in order to reuse them later.

Contract Syntax

Contracts are specified as JSON-objects of the form

{
  "precondition": HeapConfigurationObject,
  "postconditions":[ HeapConfigurationObject ]
}

• precondition is the heap configuration which serves as input to the method analysis. That is, it corresponds to the fragment of the heap that is reachable from the method's input parameters.
• postconditions are all final states in the analysis of the method given the precondition, i.e. the effect of the method on the reachable fragment.

The syntax of HeapConfigurationObjects is explained here