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 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 - 2019 MantisBT Team
Powered by Mantis Bugtracker