		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-function-and-loop-generation

Generation of C functions and loops.

Subtopics

Atc-gen-cfun-correct-thm: Generate the correctness theorem for a C function.
Atc-typed-formals: Calculate the C types of the formal parameters of a target function.
Atc-gen-outer-bindings-and-hyps: Generate the outer bindings, pointer hypotheses, pointer substitutions, and lemma instantiation, for a correctness theorem.
Atc-gen-fundef: Generate a C function definition from a non-recursive ACL2 function, with accompanying theorems.
Atc-gen-exec-stmt-while-for-loop: Generate a version of exec-stmt-while specialized to the loop represented by fn.
Atc-gen-context-preamble: Generate a context preamble from the formals of a function.
Atc-gen-pop-frame-thm: Generate the theorem about popping the frame at the end of a function execution.
Atc-gen-loop-correct-thm: Generate the correctness theorem for a C loop.
Atc-gen-loop-body-correct-thm: Generate the correctness theorem for the body of a loop.
Atc-gen-init-scope-thms: Generate the theorems about the initial scope of a function execution.
Atc-gen-fun-correct-thm: Generate the correctness theorem for a C function.
Atc-gen-fn-result-thm: Generate the theorem about the result(s) of fn.
Atc-gen-loop: Generate a C loop from a recursive ACL2 function, with accompanying theorems.
Atc-gen-loop-test-correct-thm: Generate the correctness theorem for the test of a loop.
Atc-check-guard-conjunct: C type and argument derived from a guard conjunct, if any.
Atc-find-affected: Find the variables affected by a term.
Atc-gen-cfun-final-compustate: Generate a term representing the final computation state after the execution of a C function.
Atc-gen-init-inscope-auto: Generate the automatic storage scope of the initial symbol tale for a C function.
Atc-gen-init-inscope-static: Generate the static storage scope of the initial symbol table for a C function.
Atc-gen-push-init-thm: Generate the theorem about the initial computation state of a function execution.
Atc-gen-loop-measure-fn: Generate a measure function for a recursive target function.
Atc-gen-fun-endstate: Generate a term representing the ending computation state after the execution of a C function.
Atc-gen-loop-termination-thm: Generate the version of the termination theorem tailored to the limits and measure function.
Atc-gen-formal-thm: Generate the theorem about a formal parameter of a target function.
Atc-gen-loop-final-compustate: Generate a term representing the final computation state after the execution of a C loop.
Atc-gen-loop-measure-thm: Generate type prescription theorem asserting that the measure of the recursive function fn yields a natural number.
Atc-gen-object-disjoint-hyps: Generate hypotheses saying that the pointers designate disjoint objects.
Atc-loop-body-term-subst: In a term that represents the body of a loop, replace each recursive call with a term that returns the affected variables.
Atc-gen-omap-update-formals: Generate a term that is an omap::update nest for the formals of a function.
Atc-gen-loop-tthm-formula: Generate the formula for the loop termination theorem.
Atc-gen-init-inscope: Generate the initial symbol table for a C function.
Atc-gen-fn-def*: Generate a local theorem that defines fn using if*.
Atc-gen-param-declon-list: Generate a list of C parameter declarations from a list of ACL2 formal parameters.
Atc-formal-affectablep: Check if a formal parameter is a affectable.
Atc-gen-cfun-fun-env-thm: Generate the theorem saying that looking up a certain C function in the function environment yields the information for that function.
Atc-gen-add-var-formals: Generate a term that is an add-var nest for the formals of a function.
Atc-gen-cfun-fun-env-thm-name: Generate the name of the theorem saying that looking up a certain C function in the function environment yields the information for that function.
Atc-gen-fn-guard: Generate a local function for the guard of fn.
Atc-filter-exec-fun-args: Filter external objects out of the formals, for passing to exec-fun.
Atc-gen-context-preamble-aux-aux
Atc-typed-formals-to-extobjs: List of the formals of a function that represent external objects.
Atc-formal-affectable-listp: Lift atc-formal-affectablep to lists.