CodeHawk-C File Organization

C Applications are analyzed by individual compilation unit (cfile called here) by the OCaml analyzer in multiple rounds. After each round, the results of those analyses are integrated by the python interface. This integration includes the generation of supporting proof obligations that reach across compilation units, and making available return value assumptions, by request. These new proof obligations and assumptions are added to the results files to be consumed by the OCaml analyzer. This process continues until stabilization, or when a specified maximum number of rounds is reached.

In the following descriptions we use the abbreviations:

• ppo primary proof obligation

• spo supporting proof obligation

The various intermediate files passed between the OCaml analyzer and python are the following.

At the file level:

<filename>_cfile.xml

global declarations: created by cchcil upon parsing the C source code; never modified

<filename>_cdict.xml

dictionary of types and expressions. Originally created by cchcil upon parsing the C source code, but updated by cchlib in subsequent rounds

<filename>_ctxt.xml

dictionary of contexts used in expressing locations created and updated by cchcil

<filename>_prd.xml

dictionary of predicates used in expressing proof obligations, created and updated by cchpre

<filename>_ixf.xml

dictionary of interface predicates used in expressing assumptions and guarantees external to functions

<filename>_cgl.xml

dictionary of assignments to global variables

<filename>_gxrefs.xml

association table that relates file identifiers of variables (varinfo’s) and structs (compinfo’s) to global identifiers, to facilitate communication and exchange of assumptions/guarantees between different files.

At the function level (all prefixed with <filename_functionname>:

_cfun.xml

function semantics, as produced by CIL, created by cchcil upon parsing the C source code, never modified

_ppo.xml

primary proof obligations for the function, generated once by cchpre, not updated afterwards

_spo.xml

supporting proof obligations for the function, primarily generated and updated by the python side

_pod.xml

dictionary for assumptions, ppos, and spos, initially created by cchpre, and updated by both cchpre and the python side as new spos are added in each round.

_api.xml

external assumptions and guarantees from other functions, global variables, and possibly user-provided contracts.

_vars.xml

variable and expression dictionary containing all variables and expressions used in the invariants

_invs.xml

invariant dictionary containing all location invariants (with locations specified by context)