Frama-C I have received the review of my submission to the ICPC 2011 industrial challenge. If you have read the challenge description, you may remember that participating involved writing various fictional e-mails. In my submission, I skimped a bit on that part. Some of the e-mails I replaced by an e-mail...
Read MoreThis blog post is a revised version of part of my submission to the ICPC 2011 Industry Challenge. Please go ahead and read the challenge description. I could only paraphrase it without adding anything to it and so I won't. The study was made with the April development version of...
Read MoreI should have said this earlier — others might have wanted to join in the fun — but I will be sending an entry to participate in the International Conference on Program Comprehension's Industrial Challenge. My write-up will appear here shortly after the submission deadline.
Read MoreThis post follows that post. For cases 2 and 3 in order to get more complete execution traces we again take advantage of Frama_C_dump_each(). Before launching the analysis we insert a call to this primitive right at the end of RoCo_process() so that local variables of that function will be...
Read More