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] Use Frama-C to dump all read and write memory accesses in a given C program

  • Subject: [Frama-c-discuss] Use Frama-C to dump all read and write memory accesses in a given C program
  • From: s.darabi at utwente.nl (s.darabi at utwente.nl)
  • Date: Tue, 11 Oct 2016 12:45:11 +0000
Dear Frama-C users and developers,


I am a PhD student working on the verification of parallel C programs where we verify data-race freedom of a program by checking the program against its (manually written) specifications. At the moment, I am looking for techniques which help me to generate the specifications automatically (as much as possible). In particular, I need to know all the read or write memory accesses in a given C program. Do you think I can use Frama-C for that purpose? if yes, can you give me some hints about how to do it?

Thanks in advance,

Saeed?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161011/7d715729/attachment.html>