--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on December 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] about slicing



I have seen some documents about frama-c. It seems that sometimes some
slicing problems originate from its dependence analysis, such as value
analysis and PDG. So I want to know whether  in frama-c, there  are some
mechanisms/pragmas that enable users to give fragma-c tool some hints and
help frama-c improve its value analysis and PDG?

*Huizhan Yi,*
Associate Professor, College of Computer, National University of Defense
Technology,China
Work Phone: 0731-84574650
WeiXin Num: huizhanyi
QQ Num?562538519

On Fri, Dec 19, 2014 at 11:45 AM, Huizhan Yi <huizhanyi at gmail.com> wrote:

> Hi
> I am working program slicing with frama-c. I compile and install
> frama-c-Neon-20140301.  When I test some toy applications in the
> frama-c-Neon-20140301/tests/slicing, I find some problem. for example, such
> as the bts1445.i, the result log is
>
> [slicing] slicing requests in progress...
> [value] Analyzing a complete application starting at main
> [value] Computing initial state
> [value] Initial state computed
> [value] Values of globals at initialization
>   x ? {0}
> tests/slicing/bts1445.i:8:[value] entering loop for the first time
> [value] Recording results for main
> [value] done for function main
> [slicing] making slicing project 'Slicing'...
> [slicing] interpreting slicing requests from the command line...
> [slicing] warning: No internal slicing request from the command line.
> [slicing] warning: Adding an extra request on the entry point of function:
> main.
> [pdg] computing for function main
> tests/slicing/bts1445.i:10:[pdg] warning: no final state. Probably
> unreachable...
> [pdg] done for function main
> [slicing] applying all slicing requests...
> [slicing] applying 1 actions...
> [slicing] applying actions: 1/1...
> [slicing] exporting project to 'Slicing export'...
> [slicing] applying all slicing requests...
> [slicing] applying 0 actions...
> [sparecode] remove unused global declarations from project 'Slicing export
> tmp'
> [sparecode] removed unused global declarations in new project 'Slicing
> export'
> /* Generated by Frama-C */
> void main(void)
> {
>   return;
> }
>
> It seems that I do not get correct slice for main function.
>
> I try to slice it with
> frama-c -slice-calls main bts1445.i -then-on "Slicing export" -print
> It is the same result.
>
> The source code for bts1445.i is
> /*  run.config
> OPT: -check -slice-calls main -then-on "Slicing export" -print
> OPT: -check -slice-calls f -main f -then-on "Slicing export" -print
> */
> int x = 0;
>
> int main() {
>   while(1)
>     x=0;
>   return x + 1;
> }
>
> int f() {
>   while(1)
>     x=0;
>   return x + 1;
> }
>
> I think that a right slice is
>
> int x = 0;
>
> int main() {
>   while(1)
>     x=0;
>   return x + 1;
> }
>
> Why is there the problem? There is any method to solve it?
>
> *Huizhan Yi,*
> Associate Professor, College of Computer, National University of Defense
> Technology,China
> Work Phone: 0731-84574650
> WeiXin Num: huizhanyi
> QQ Num?562538519
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141229/6fc86a8a/attachment.html>