mc-imperial / gpuverify

GPUVerify: a Verifier for GPU Kernels
http://multicore.doc.ic.ac.uk/tools/GPUVerify/
Other
58 stars 15 forks source link

Start using the axioms that carry array information #2

Open jeroenk opened 9 years ago

jeroenk commented 9 years ago

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.