CODEWITHSUNDEEP
frama-c
user3561024
user3561024

Reputation: 21

Using Impact analysis in Frama-C

I tried using frama-c-gui and was able to perform impact analysis But I am not able to figure out how can we pass statment number on which the impact analysis needs to be performed in batch mode of Frama-C.

Upvotes: 2

Views: 278

Answers (1)

Virgile
Virgile

Reputation: 10148

There is a special annotation //@ impact pragma stmt; that you can use to indicate that you are interested in the impact of the statement following the annotation. Then, if said annotation is in function f, you can use the following command line to print the impacted code on the command line:

frama-c -impact-pragma f -impact-slicing impact.c -then-on "impact slicing" -print
  • -impact-pragma f indicates that you are interested by the statements flagged by a pragma in function f
  • -impact-slicing indicates that you want to create a project named impact slicing containing the statements impacted by the one(s) you have selected.
  • -then-on "impact-slicing" let you continue the analysis on project impact slicing (here we only -print the code, but you can put any option you like after -then-on project_name)

Note however that the impact plugin is quite experimental.

Upvotes: 3

Related Questions