package mopsa

Variables

The type var represents variables in Mopsa. In addition to a unique string name and a type, a variable is decorated with an extensible type var_kind that allows annotating the variable with extra information that is specific to its language.

New kinds of variables can be added by extending var_kind with a new variant. For example, for some toy language Toy in which variables, in addition to a name and a type, have an initial value, a new variable kind can be created with

type var_kind += V_toy of expr

This new variable kind needs to be registered

let () = register_var {
    compare = (fun next v1 v2 ->
        match vkind v1, vkind v2 with
        | V_toy init1, V_toy init2 -> compare_expr init1 init2
        | _ -> next v1 v2
      );
    print = (fun fmt next v ->
        match vkind v with
        | V_toy v -> Format.pp_print_string fmt v.vname
        | _ -> next fmt v
      );
  }

Another property of variables is their access mode. When a variable represents a single dimension in the concrete, assignments on this variable are performed with strong updates, i.e. the update destroys the previous value.

On the other hand, when an abstract domain summarizes the value of several concrete dimensions into a single variable, only weak updates can be performed to preserve the value of unmodified concrete dimensions.

Access modes

Variables

Registration

Common variables

Containers for variables

Deprecated