Skip to content

Start using the axioms that carry array information #2

Open
@jeroenk

Description

For each global array Bugle generates an axiom, e.g.

axiom {:array_info "$$in"} {:global} {:elem_width 8} {:source_name "in"} {:source_elem_width 32} {:source_dimensions "*"} true;

These are currently not being used, but are supposed to replace the attributes that occur on the race checking variables and the array declarations. The axioms should be used instead and the attributes on the race checking variables and array declarations should be dropped.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions