Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] needing help to write a frama-c plugin

  • Subject: [Frama-c-discuss] needing help to write a frama-c plugin
  • From: nicolas.zilio at fr.thalesgroup.com (ZILIO Nicolas)
  • Date: Mon, 1 Sep 2014 09:38:32 +0200
Dear frama-c developers and contributors,

I'm writing to you as I'm quite in trouble making a home-made plugin working. Here is what I would like to do : given a C programm and after having called Impact plugin, i would like to print out in a chosen text file all the files' name of the statements found impacted by Impact plugin, but with no redundancy.

I was by the fact thinking of that algorithm for this task :

in : name of the file where results should be printed, files of the programm,
          statement to be considered subject to change

out : a text file with results

start
  launch value and so impact analysis
  create an empty list for results
  for each statement of the c programm marked as impacted
      get the file's name where is the statement
      if the file's name is not in the list
          add the file's name to the list
      end if
  end for
  print the list of names into the out_file
  print the number of impacted files (ie the length of the list)
end



and in order to do so, I started to write a plugin in the same way about the CFG plugin in the developer's guide and you can find the files of my plugin attached.

Nevertheless, I can't make it working. could you so be kind to tell me :

-am I right about the use of frama-c functions here (the "db.impact.compute_pragmas" and "the x.location")? I saw in the developers's guide that I may use something similar to "!db.impact.compute_pragmas", but I don't understand why as many plugins use for exemple "db.value.is_computed".

-is the way I use Cil.DoChildren sufficient here? I'm a bit confused on how to use it properly.

Moreover, because I'm a lot curious, can I find more documentation about this phrase written in the developers' guide : "An interesting exercise would be to change the AST so that execution of each instruction is logged to a file, and then re-read that file to print in the CFG how much time each instruction has been executed", especially how execution time can be registered here for that?

Thanks in advance for any response and any help,
Regards,

ZILIO Nicolas

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140901/af7407f0/attachment.html>
-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: makefile
Type: application/octet-stream
Taille: 228 octets
Desc: makefile
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140901/af7407f0/attachment.obj>
-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: analyseTU_core.ml
Type: application/octet-stream
Taille: 901 octets
Desc: analyseTU_core.ml
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140901/af7407f0/attachment-0001.obj>
-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: analyseTU_options.ml
Type: application/octet-stream
Taille: 562 octets
Desc: analyseTU_options.ml
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140901/af7407f0/attachment-0002.obj>
-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: analyseTU_register.ml
Type: application/octet-stream
Taille: 332 octets
Desc: analyseTU_register.ml
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140901/af7407f0/attachment-0003.obj>