viperproject / axiom-profiler-2

The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
https://viperproject.github.io/axiom-profiler-2/
8 stars 3 forks source link

Unsanitized variable and function names being converted to html #57

Closed cschmitter closed 4 days ago

cschmitter commented 1 week ago

Function and variable names are not sanitized before being formatted into HTML, leading to names not being correctly displayed.

Currently this bug is particularly notable in log files generated by silicon, which annotates Viper variable and functions names with their types, e.g. silicon takes the function append(p, q) and rewrites it as append<Sequence<Int>>(p, q). When these variable names are formatted into HTML to be displayed in the selected nodes info section the <Sequence<Int> is interpreted as an HTML tag leaving append>(p, q) to be displayed.

image

This issue is not present in the matching loop graphs as the <> are not interpreted as tags.

image