Add a generator for the visible steps appearing in a trace.

model-checking / cbmc-viewer

CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.

https://model-checking.github.io/cbmc-viewer/

Apache License 2.0

32 stars 11 forks source link

Add a generator for the visible steps appearing in a trace. #76

Closed markrtuttle closed 2 years ago

markrtuttle commented 2 years ago

CBMC marks some steps in a trace as hidden. Before this commit, viewer made visible all hidden function invocations, function returns, and variable assignments. These hidden variable assignments included some assignments to variables internal to CBMC. With this commit, viewer makes visible only those variable assignments that initialize static data.