diff --git a/src/plugins/markdown-report/README.md b/src/plugins/markdown-report/README.md index 86db9c1694633b271267538b55aae070ac230310..baa58e5c82bc662b90482f72eba6e2ee0a46f7ce 100644 --- a/src/plugins/markdown-report/README.md +++ b/src/plugins/markdown-report/README.md @@ -66,7 +66,7 @@ Sarif document can be validated against the spec Checking out [`https://github.com/Frama-C/open-source-case-studies`](https://github.com/Frama-C/open-source-case-studies), start with a simple analysis and generate the intermediary SVG and Markdown files. ```shell -frama-c -val 2048.c -val-flamegraph="flamegraph.txt" -save snap.sav +frama-c -eva 2048.c -eva-flamegraph="flamegraph.txt" -save snap.sav flamegraph.pl ./flamegraph.txt > flamegraph.svg frama-c -load snap.sav -mdr-gen -mdr-flamegraph="./flamegraph.svg" ``` diff --git a/src/plugins/nonterm/README.md b/src/plugins/nonterm/README.md index 58e7234fe82bac290bdbe00bb17bcfac9d57d2cd..0dda9d6d08644e372039dcd122815c860d32163b 100644 --- a/src/plugins/nonterm/README.md +++ b/src/plugins/nonterm/README.md @@ -2,9 +2,9 @@ Nonterm ======= Nonterm (for "non-termination") is a small plug-in used to help identify issues -when running a Value analysis. +when running Eva. -It runs after Value and outputs warnings when reachable but definitively +It runs after Eva and outputs warnings when reachable but definitively non-terminating functions/loops are detected, e.g. as in the code below: void f(int i) { @@ -17,7 +17,7 @@ non-terminating functions/loops are detected, e.g. as in the code below: return 0; } -A warning is emitted when a function is reachable by Value, but its return +A warning is emitted when a function is reachable by Eva, but its return statement is unreachable. Note that normalized void functions have an implicit return statement before @@ -30,6 +30,6 @@ have unreachable post-states (i.e. their evaluation results in `Bottom`). Usage ----- -Apply it after running Value, as in: +Apply it after running Eva, as in: - frama-c -val file.c -then -nonterm + frama-c -eva file.c -then -nonterm