Lab for Automated Reasoning and Analysis LARA

Annotations

phantm supports in-code annotations given in the form of PHPDoc comments. Those annotations will then be used as part as the type analysis phase. For example:

/**
 * @param int $var
 * @return int
 */
function foo($var) {
   return $var+2;
}

Types allowed as annotations

phantm will support base types such as @int@ or @string@ but can also specify precise array types:

Array types

You can precisely specify array types inside annotations, the syntax is the following:

 Array[ <key> => <type>, ..., ? => <type> ] 

<key> can either be of the form “string” or 42.

the special ”?” key can be used as a placeholder for any other entries. For example, one array that has “foo” being a String or an Int and the rest being Undefined or Int can be represented as:

 Array["foo" => string | int, ? => undef | int]

Typedefs

phantm will support typedefs to allow you give names to complicated types. For example:

/**
 * @typedef mytype = Array["foo" => int, "bar" => string, ? => undef ]
 * @param #mytype $var
 * @return #mytype
 */
function foo($var) {
   return $var;
}

Note that typedefs are global, and collected before any other annotations. This means that if you've two typedefs with the same name, only the second will be used, even for usages preceding it.

 
phantm/annotations.txt · Last modified: 2010/05/04 15:37 by ekneuss
 
© EPFL 2018 - Legal notice