		Search-engine friendly clone of the ACL2 documentation.

Execution-environmentp

Make-execution-environment

Constructor macro for execution-environmentp structures.

Syntax:

(make-execution-environment [:owner-address <owner-address>] 
                            [:sender-address <sender-address>] 
                            [:gas-price <gas-price>] 
                            [:input-data <input-data>] 
                            [:causer-account <causer-account>] 
                            [:value <value>] 
                            [:bytecode <bytecode>] 
                            [:block-header <block-header>] 
                            [:depth <depth>] 
                            [:permission <permission>])

This is our preferred way to construct execution-environmentp structures. It simply conses together a structure with the specified fields.

This macro generates a new execution-environmentp structure from scratch. See also change-execution-environment, which can "change" an existing structure, instead.

The execution-environmentp structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-execution-environment instead.

Definition

This is an ordinary make- macro introduced by std::defaggregate.

Macro: make-execution-environment

(defmacro make-execution-environment (&rest args)
  (std::make-aggregate 'execution-environment
                       args
                       '((:owner-address)
                         (:sender-address)
                         (:gas-price)
                         (:input-data)
                         (:causer-account)
                         (:value)
                         (:bytecode)
                         (:block-header)
                         (:depth)
                         (:permission))
                       'make-execution-environment
                       nil))