From b0fd9f28fdaf26d7039d2f5b24920973e66c31f3 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Thu, 31 Oct 2019 15:38:52 +0100 Subject: [PATCH] [Doc] remove last occurrences of -val --- src/plugins/markdown-report/README.md | 2 +- src/plugins/nonterm/README.md | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/plugins/markdown-report/README.md b/src/plugins/markdown-report/README.md index 86db9c16946..baa58e5c82b 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 58e7234fe82..0dda9d6d086 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 -- GitLab