Frama-C Bug Tracking System - Frama-C
View Issue Details
0000780Frama-CPlug-in > slicingpublic2011-04-11 01:072014-02-12 16:54
pascal 
virgile 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000780: r12793: slicing generates uncompilable code (sliced function called with too few arguments) (csmith)
Bug occurred with pre-processing done on a 64-bit machine. ~/ppc/bin/toplevel.opt -val-signed-overflow-alarms noresult.11005403.1.c -cpp-command "gcc -C -E -I. -I$CSMITH/runtime " -machdep x86_64 -slice-calls printf -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -no-val -slevel 0 -print -ocode noresult.11005403.1.s.c produced the provided noresult.11005403.1.s.c file, which does not compile: gcc -I runtime noresult.11005403.1.s.c noresult.11005403.1.s.c: In function ‘func_1_slice_1’: noresult.11005403.1.s.c:466: error: too few arguments to function ‘func_28_slice_1’ noresult.11005403.1.s.c: In function ‘func_28_slice_1’: noresult.11005403.1.s.c:741: error: ‘p_29’ undeclared (first use in this function) noresult.11005403.1.s.c:741: error: (Each undeclared identifier is reported only once noresult.11005403.1.s.c:741: error: for each function it appears in.) The original compiles, although it does have some warnings: gcc -I runtime noresult.11005403.1.c noresult.11005403.1.c: In function ‘func_56’: noresult.11005403.1.c:819: warning: comparison of distinct pointer types lacks a cast noresult.11005403.1.c:879: warning: comparison of distinct pointer types lacks a cast noresult.11005403.1.c:886: warning: comparison of distinct pointer types lacks a cast noresult.11005403.1.c: In function ‘func_116’: noresult.11005403.1.c:2053: warning: comparison of distinct pointer types lacks a cast noresult.11005403.1.c:2054: warning: comparison of distinct pointer types lacks a cast
No tags attached.
related to 0000791closed pascal Cash in value analysis of sliced project 
tgz slice_missing_arg.tgz (56,651) 2011-04-11 01:07
https://bts.frama-c.com/file_download.php?file_id=190&type=bug
? frama_c_journal.ml (3,304) 2011-04-11 10:26
https://bts.frama-c.com/file_download.php?file_id=191&type=bug
Issue History
2011-04-11 01:07pascalNew Issue
2011-04-11 01:07pascalStatusnew => assigned
2011-04-11 01:07pascalAssigned To => Anne
2011-04-11 01:07pascalFile Added: slice_missing_arg.tgz
2011-04-11 09:02AnneNote Added: 0001692
2011-04-11 09:02AnneStatusassigned => acknowledged
2011-04-11 09:46AnneNote Added: 0001693
2011-04-11 10:12pascalNote Added: 0001694
2011-04-11 10:26monateFile Added: frama_c_journal.ml
2011-04-11 10:27monateNote Added: 0001695
2011-04-11 10:40AnneNote Added: 0001697
2011-04-11 10:46AnneNote Added: 0001698
2011-04-11 10:53pascalNote Added: 0001699
2011-04-11 11:05AnneNote Added: 0001700
2011-04-11 11:39svnCheckin
2011-04-11 11:41AnneNote Added: 0001702
2011-04-11 15:01AnneNote Added: 0001714
2011-04-11 15:36patrickNote Added: 0001715
2011-04-11 15:41patrickNote Edited: 0001715
2011-04-11 15:48signolesNote Added: 0001717
2011-04-11 15:50AnneNote Added: 0001719
2011-04-11 16:23AnneNote Added: 0001720
2011-04-11 17:11AnneNote Added: 0001721
2011-04-11 17:11AnneStatusacknowledged => assigned
2011-04-11 17:11AnneAssigned ToAnne => virgile
2011-04-11 17:18AnneNote Added: 0001722
2011-04-14 14:33yakobowskiRelationship addedrelated to 0000791
2011-04-14 14:34yakobowskiNote Added: 0001788
2011-04-14 14:34yakobowskiStatusassigned => resolved
2011-04-14 14:34yakobowskiFixed in Version => Frama-C GIT, precise the release id
2011-04-14 14:34yakobowskiResolutionopen => fixed
2011-10-10 14:13signolesFixed in VersionFrama-C GIT, precise the release id => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed

Notes
(0001692)
Anne   
2011-04-11 09:02   
Ok : I'll have a look. The result seems quite strange !
(0001693)
Anne   
2011-04-11 09:46   
It seems that the slicing is applied twice. The first result looks better... I have to investigate : - why the slicing is done a second time; - why is the result incorrect the second time;
(0001694)
pascal   
2011-04-11 10:12   
I noticed that the value analysis was launched a second time. I wasn't able to prevent it, so I set slevel to zero the second time. This other bug (slicing launching again on sliced project) should be investigated, and the bug occurring here may only be a consequence of the strange circumstances this causes.
(0001695)
monate   
2011-04-11 10:27   
I uploaded the generated journal. Some slicing options have probably not been reset correctly upon completion.
(0001697)
Anne   
2011-04-11 10:40   
A workaround is to use the option [-no-slice-force] in the second part of the command (after the [-then-on]).
(0001698)
Anne   
2011-04-11 10:46   
When saving the result of the first slicing, and applying the slicing again, the second result is correct (at least gcc is happy with it).
(0001699)
pascal   
2011-04-11 10:53   
Regarding the workaround, how is one supposed to use it? I have the line: ~/ppc/bin/toplevel.opt -val-signed-overflow-alarms t$N.c -cpp-command "gcc -C -E -I. -I$CSMITH/runtime " -machdep x86_64 -slice-calls printf -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -no-slice-force -no-val -print -ocode s$N.c The wrong actions are still taken on the sliced project: I can see clearly the value analysis being launched the second time, because function crc32_gentab has been renamed crc32_gentab_slice1, so "-slevel-function crc32_gentab:0 " does not apply to it and this function takes a long time. Or do I need to write a journal ?
(0001700)
Anne   
2011-04-11 11:05   
I have just added the [-no-slice-force] to the end of your first command... but I forgot that I have done a test with Patrick so that I have changed something : sorry! The modification is to move [SlicingParameters.set_off ()] before the call to [Db.Slicing.Project.extract] in [slicing/register.ml]. I don't commit it yet because I am waiting for Patrick and Julien recommendation.
(0001702)
Anne   
2011-04-11 11:41   
The initial problem is still there and can now be seen using an explicit call to the slicer on the generated project (ie. [-slice-calls printf] after [-then-on]).
(0001714)
Anne   
2011-04-11 15:01   
The initial problem disappeared ! I don't manage to reproduce it... sorry.
(0001715)
patrick   
2011-04-11 15:36   
(edited on: 2011-04-11 15:41)
I got the following error during the second slicing: [kernel] user error: Function tmp_50 invoked on a non function type [kernel] Frama-C aborted because of invalid user input. with command: frama-c -val-signed-overflow-alarms noresult.11005403.1.c -cpp-command "gcc -C -E -I. -Iruntime " -machdep x86_64 -slice-calls printf -slevel 5000 -slevel-function crc32_gentab:0 -check -then-on 'Slicing export' -slice-calls printf -check -print -slice-force
(0001717)
signoles   
2011-04-11 15:48   
Just add option "-slice-force" after "-then-on": ~/ppc/bin/toplevel.opt -val-signed-overflow-alarms noresult.11005403.1.c -cpp-command "gcc -C -E -I. -I$CSMITH/runtime " -machdep x86_64 -slice-calls printf -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -no-val -slevel 0 -print -ocode noresult.11005403.1.s.c -slice-force
(0001719)
Anne   
2011-04-11 15:50   
Ok : thanks ! I'll have a look again.
(0001720)
Anne   
2011-04-11 16:23   
The problem doesn't have the same symptom than before, but it is still there and is even more strange : a function in a call ([safe_add_func_uint32_t_u_u_slice_1]) is substituted by a variable ([tmp_50] which is detected by the [-check] option) ! While doing the exportation, the function name seems to be still there (in the debug messages) but in the result (printed by [-slice-print]) it has been substituted... It seems that it is not the only case : many [tmp_xx] variables appear in function calls.
(0001721)
Anne   
2011-04-11 17:11   
I think that the problem comes from [Filter.compute_fct_definitions] which does suspicious things about function variables. While processing the function body, everything seems ok, but when the visitor prints "Adding definition %s (vid: %d) for project %s", the definition is not ok anymore. I not sure to understand what is done here. Could you have a look Virgile ? Thanks.
(0001722)
Anne   
2011-04-11 17:18   
My command line : frama-c noresult.11005403.1.c -cpp-command "gcc -C -E -I. -Iruntime " \ -machdep x86_64 -val-signed-overflow-alarms -slevel 0 \ -slice-calls printf -slice-print \ -then-on 'Slicing export' \ -slice-calls printf -slice-print -slice-force \ -debug 1 -check \ > slice.log
(0001788)
yakobowski   
2011-04-14 14:34   
Fixed by changeset 12885. Varinfos were created by the slicing in the wrong project.