--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on October 2013 ---
Hello, On Tue, Oct 15, 2013 at 12:12 PM, David Yang <abiao.yang at gmail.com> wrote: > The interpret function is the function in eval.c file of gawk-3.0.2 > software system. > According to the NEWS file in gawk, ?Uses volatile declaration if STDC > 0 to avoid problems due to longjmp.? The bad news is that it would be an enormous amount of work to correctly and precisely model longjmp so that you can analyze a gawk program that uses it. The good news is that since you are not going to model longjmp anyway, you can effectively ignore the volatile qualifier in the source files of gawk. Adding the option -Dvolatile= to the pre-processor's command-line options should do it. Without the ?volatile? qualifier, those pointers that are inputs of the analysis' entry point have variables generated for them to point to according to -context-width and similar options. The pointer arguments for functions that are not the entry point of the analysis will behave as you would expect. Pascal -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131015/dd6c76da/attachment.html>