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] about slicing

  • Subject: [Frama-c-discuss] about slicing
  • From: huizhanyi at gmail.com (Huizhan Yi)
  • Date: Mon, 29 Dec 2014 10:43:02 -0500
  • In-reply-to: <CAFZNyL7iNh+u1b-vG4Z3h_HxSE+M5s4c8oErQB=8J08+XhKLMA@mail.gmail.com>
  • References: <CAFZNyL7iNh+u1b-vG4Z3h_HxSE+M5s4c8oErQB=8J08+XhKLMA@mail.gmail.com>
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>