		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Function-recursion

Function recursion checks in Leo.

Functions may call other functions, but currently any kind of (direct or indirect) recursion is prohibited. Some forms of bounded recursion may be allowed in the future, but for now that is not the case.

Thus, the Leo static semantics includes the requirement that there is no function recursion. Here we formalize this requirement, by constructing a dependency graph among the functions and ensuring that there are no circularities in the graph.

Subtopics

Statements-callees: Functions called by statements, lists of statements, branches, and lists of branches.
Expressions-callees: Functions called by expressions and lists of expressions.
File-function-recursion-okp: Check if a Leo file has no function recursion.
Topdecl-list-call-graph: Call graph induced by a list of top-level declarations.
Fundecl-call-graph: Call graph induced by a function declaration.
Topdecl-call-graph: Call graph induced by a top-level declaration.
Expression-callees: Functions called by an expression.
Constdecl-callees: Functions called by a constant declaration.
Console-callees: Functions called by a console call.
Vardecl-callees: Functions called by a variable declaration.
Struct-init-list-callees: Functions called by a list of struct component initializers.
Struct-init-callees: Functions called by a struct component initializer.
Statement-list-callees: Functions called by a list of statements.
Expression-list-callees: Functions called by a list of expressions.
Branch-list-callees: Functions called by a list of branchess.
Statement-callees: Functions called by a statement.
Branch-callees: Functions called by a branch.