		Search-engine friendly clone of the ACL2 documentation.

Transformation-tools

Split-all-gso

A transformation to split all global struct objects.

Introduction

This is a meta transformation which repeatedly applies splitgso to any global struct object it can.

General Form

(split-all-gso const-old
               const-new
               :gcc  ... ; optional
               :ienv ... ; optional
  )

Inputs

const-old

Specifies the code to be transformed.
This must be a symbol that names an existing ACL2 constant that contains a validated translation unit ensemble, i.e. a value of type transunit-ensemble resulting from validation, and in particular containing validation information. This constant could result from c$::input-files, or from some other transformation.

const-new

Specifies the name of the constant for the transformed code.
This must be a symbol that is valid name for a new ACL2 constant.

:gcc — default nil

Boolean flag saying whether certain GCC extensions should be accepted or not. This is used when re-validating intermediate outputs (see c$::validator).

:ienv — default (c$::ienv-default)

The implementation environment under which re-validation is performed.

Subtopics

Split-all-gso-implementation: Implementation of split-all-gso.