Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000807Frama-CPlug-in > slicingpublic2011-04-28 14:492014-02-12 16:59
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000807: sliced program does not terminate (csmith)
Descriptionsame conditions as bug 806.

Compile the original with gcc -m32 -D__FRAMAC -I runtime show_each.c noterm.c (executable terminates) and the sliced program with gcc -m32 show_each.c noterm.s.c
TagsNo tags attached.
Attached Filesc file icon noterm.c [^] (7,874 bytes) 2011-04-28 14:49 [Show Content]

- Relationships

-  Notes
(0001826)
Anne (reporter)
2011-04-28 17:12

I managed to reduce the problem to :
frama-c -slice-calls printf toto.c \
        -then-on 'Slicing export' -print -ocode toto.s.c

with toto.c :

#include <stdio.h>
int G;
void f (void) {
  int b = 7; int a = 2;
  if ((( a || 42) && b)) {
    while (1) { G = 21; return; }
  }
}
int main (void) {
  f();
  printf ("RES = %d\n", G);
  return 0;
}

but now, I have to see what's going wrong...
(0001827)
Anne (reporter)
2011-04-28 17:22

What I really don't understand is that if I put the internal form of the condition in the source code :
  if (a) { goto _LOR; }
  else {
    _LOR: /* internal */ ;
    if (b) { while (1) { ... } }
    }
It works !
(0001828)
Anne (reporter)
2011-04-28 18:01

Ok : in the generated internal form, there is a statement block in the else branch. This statement is unreachable since [a = 2] and the label is inside the block. That might be the reason why it doesn't work. Anyway, this is at least the difference between the 2 examples.

To be continued...
(0001831)
Anne (reporter)
2011-04-29 10:16

This is a problem with the lexical successor computation when there are unreachable statements. Will be fixed soon...
(0004800)
Anne (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-04-28 14:49 pascal New Issue
2011-04-28 14:49 pascal Status new => assigned
2011-04-28 14:49 pascal Assigned To => Anne
2011-04-28 14:49 pascal File Added: noterm.c
2011-04-28 14:54 pascal Summary sliced program does not terminate => sliced program does not terminate (csmith)
2011-04-28 17:12 Anne Note Added: 0001826
2011-04-28 17:22 Anne Note Added: 0001827
2011-04-28 18:01 Anne Note Added: 0001828
2011-04-29 10:16 Anne Note Added: 0001831
2011-04-29 10:41 svn Checkin
2011-04-29 10:41 svn Status assigned => resolved
2011-04-29 10:41 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 Anne Note Added: 0004800
2014-02-12 16:59 Anne Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker