Skip to content
Snippets Groups Projects
Commit b0fd9f28 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[Doc] remove last occurrences of -val

parent 264fedfa
No related branches found
No related tags found
No related merge requests found
...@@ -66,7 +66,7 @@ Sarif document can be validated against the spec ...@@ -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. 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 ```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 flamegraph.pl ./flamegraph.txt > flamegraph.svg
frama-c -load snap.sav -mdr-gen -mdr-flamegraph="./flamegraph.svg" frama-c -load snap.sav -mdr-gen -mdr-flamegraph="./flamegraph.svg"
``` ```
......
...@@ -2,9 +2,9 @@ Nonterm ...@@ -2,9 +2,9 @@ Nonterm
======= =======
Nonterm (for "non-termination") is a small plug-in used to help identify issues 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: non-terminating functions/loops are detected, e.g. as in the code below:
void f(int i) { void f(int i) {
...@@ -17,7 +17,7 @@ non-terminating functions/loops are detected, e.g. as in the code below: ...@@ -17,7 +17,7 @@ non-terminating functions/loops are detected, e.g. as in the code below:
return 0; 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. statement is unreachable.
Note that normalized void functions have an implicit return statement before 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`). ...@@ -30,6 +30,6 @@ have unreachable post-states (i.e. their evaluation results in `Bottom`).
Usage 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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment