This project is read-only.
1
Vote

Start using the axioms that carry array information

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.

comments