User Tools

Site Tools



This is a short summary of all useful information about the coverage tool FShell that we've come across while working on the Rapita Vetess project.

Command line


The general syntax is as follows:

fshell [parameters] [files]

Both source files and goto object files are accepted as files to be analysed.


The following list provides a summary of the most useful command line options.

Parameter Description
Output contains more detailed variable descriptions (not just base name).
Additional information includes: identifier, data type, location (file, function, line).
Switches to XML output, allowing for programmatic parsing of results.
--fuction [function-name] 
Defines the entry function FShell uses.
--unwind [bound]
Sets the global loop unwinding bound.


Once FShell has been started, a wide range of queries can be entered to generate coverage test cases. The following sections give a broad overview of FQL expressions.


There are two main forms of FQL queries:

cover [pattern]
cover [pattern] passing [pattern]

The second option is intended as a convenience format. I personally do not recommend using it.

A pattern is usually comprised of quantifiers that refer to elements in the code and rules governing the occurrence of these elements. The syntax of these rules is similar to regular expressions.

Quantifier Required element in trace
A function call statement to the requested function.
Entry edge of specified function (first statement in function).
Wildcard. Equivalent to “.” in regular expressions.
Rule element Semantics
Concatenation, meaning A is immediately followed by B.

Meaning: A function call statement of “sort” is immediately followed by the first instruction in the function “sort”, without any elements in between. This is of course always the case with any function call.

Repetition. This feature easily throws the query parser off-guard and parentheses are frequently necessary.

Meaning: a call to “sort” eventually followed by a call to “end”, with arbitrary elements in between.

Equivalent to:
Accepts anything not matching the stated pattern.

Meaning: A call of “start” eventually followed by a call of “end”, without any calls to “forbidden” in between.

Alternative. Allows specifying multiple patterns at once, all of which FShell tries to cover, producing multiple assignments (and hence test cases) if necessary.
@CALL(entry)->@CALL(end) + @CALL(entry)->@CALL(failure)

Meaning: Cover both a trace from a call to function “entry” to a call to “end” and “failure” respectively. It may be the case that these two traces are mutually exclusive, in which case FShell produces multiple assignments.

The examples in the FShell distribution make heavy use of some very specific macros defined in FShell. While very useful in their specific scenarios, they are not a required part of FQL queries, even though almost all example queries include them.

Macro Semantics
one edge per basic block
one edge per (atomic) condition outcome
one edge per decision outcome (if, for, while, switch, ?:)
all edges contributing to decisions
all edges in file a
all edges in source line x
all edges in function f
all assignments to variable t
all right hand side uses of variable t
all exit edges of f


Cover a call of a function “sort” eventually followed by a call of “filter”:

cover @CALL(sort)->@CALL(filter)

Cover a call of “start” eventually followed by a call of “end”, without any calls to “forbidden” in between:

cover @CALL(start)."NOT(@CALL(forbidden))*".@CALL(end)

Cover a trace from “entry” to “end” and from “entry” to “failure” using multiple assignments (and test cases) if necessary:

cover @CALL(entry)->@CALL(end) + @CALL(entry)->@CALL(failure)
// FShell will generate two assignments for this code example:
int a;
if(a) {
} else {
// But only one for this example:

Full syntax

Control commands:
<Command> ::= `(QUIT|EXIT)'
            | `HELP'
            | `ADD' `SOURCECODE' <Defines> <TOK_QUOTED_STRING>
            | `SHOW' `FILENAMES'
            | `SHOW' `SOURCECODE' `ALL'
            | `SET' <Options>
<Defines> ::=
            | <Defines> `-D' <TOK_C_IDENT>
            | <Defines> `-D' <TOK_C_IDENT> `=' <TOK_QUOTED_STRING>
<Options> ::= `ENTRY' <TOK_C_IDENT>
            | `LIMIT' `COUNT' <TOK_NAT_NUMBER>
            | `NO_ZERO_INIT'
            | `ABSTRACT' <TOK_C_IDENT>
Comments start with `//' and end at the end of the line

Macro definitions:
<Macro> ::= `#define' <Macro Decl> <Some Def or Empty>
<Macro Decl> ::= <Identifier>
               | <Identifier> `(' <Macro Args> `)'
<Macro Args> ::= <Identifier>
               | <Macro Args> `,' <Identifier>

<Query>                   ::= <Scope> <Cover> <Passing>
<Scope>                   ::=
                            | `IN' <Filter>
<Cover>                   ::= `COVER' <Start_Anchor> <Coverage_Pattern> <End_Anchor>
<Passing>                 ::=
                            | `PASSING' <Start_Anchor> <Path_Pattern> <End_Anchor>
<Start_Anchor>            ::=
                            | `^'
<End_Anchor>              ::=
                            | `$'
<Coverage_Pattern>        ::= <Coverage_Pattern_Term>
                            | <Coverage_Pattern> `+' <Coverage_Pattern_Term>
<Coverage_Pattern_Term>   ::= <Coverage_Pattern_Factor>
                            | <Coverage_Pattern_Term> `.' <Coverage_Pattern_Factor>
                            | <Coverage_Pattern_Term> `->' <Coverage_Pattern_Factor>
<Coverage_Pattern_Factor> ::= <ECP_Atom>
                            | `(' <Coverage_Pattern> `)'
                            | `"' <Path_Pattern> `"'
<Path_Pattern>            ::= <Path_Pattern_Term>
                            | <Path_Pattern> `+' <Path_Pattern_Term>
<Path_Pattern_Term>       ::= <Path_Pattern_Factor>
                            | <Path_Pattern_Term> `.' <Path_Pattern_Factor>
                            | <Path_Pattern_Term> `->' <Path_Pattern_Factor>
<Path_Pattern_Factor>     ::= <ECP_Atom>
                            | `(' <Path_Pattern> `)'
                            | <Path_Pattern_Factor> `*'
                            | <Path_Pattern_Factor> `>=' <TOK_NAT_NUMBER>
                            | <Path_Pattern_Factor> `==' <TOK_NAT_NUMBER>
                            | <Path_Pattern_Factor> `<=' <TOK_NAT_NUMBER>
<ECP_Atom>                ::= <Predicate>
                            | `NODES' `(' <Filter> `)'
                            | `EDGES' `(' <Filter> `)'
                            | <Filter>
                            | `PATHS' `(' <Filter> `,' <TOK_NAT_NUMBER> `)'
<Predicate>               ::= `{[^{}]+}'
<Filter>                  ::= <Filter_Function>
                            | `(' <Filter> `)'
                            | `NOT' `(' <Filter> `)'
                            | <Filter> `|' <Filter>
                            | <Filter> `&' <Filter>
                            | `SETMINUS' `(' <Filter> `,' <Filter> `)'
                            | `COMPOSE' `(' <Filter> `,' <Filter> `)'
<Filter_Function>         ::= `ID'
                            | `@FILE' `(' <TOK_QUOTED_STRING> `)'
                            | `@LINE' `(' <TOK_NAT_NUMBER> `)'
                            | `@[0-9]+'
                            | `@COLUMN' `(' <TOK_NAT_NUMBER> `)'
                            | `@FUNC' `(' <TOK_C_IDENT> `)'
                            | `@LABEL' `(' <TOK_C_IDENT> `)'
                            | `@CALL' `(' <TOK_C_IDENT> `)'
                            | `@CALLS'
                            | `@ENTRY' `(' <TOK_C_IDENT> `)'
                            | `@EXIT' `(' <TOK_C_IDENT> `)'
                            | `@BASICBLOCKENTRY'
                            | `@CONDITIONEDGE'
                            | `@DEF' `(' <TOK_C_IDENT> `)'
                            | `@USE' `(' <TOK_C_IDENT> `)'
                            | `@STMTTYPE' `(' <Stmttypes> `)'
<Stmttype>                ::= `IF'
                            | `FOR'
                            | `WHILE'
                            | `SWITCH'
                            | `?:'
                            | `ASSERT'
<Stmttypes>               ::= <Stmttype>
                            | <Stmttypes> `,' <Stmttype>

Michael's dissertation

All information in this chapter is based on Michael's dissertation: query-driven_program_testing.pdf

fshell.txt · Last modified: 2013/12/06 09:41 by pkesseli