Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000780Frama-CPlug-in > slicingpublic2011-04-11 01:072014-02-12 16:54
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000780: r12793: slicing generates uncompilable code (sliced function called with too few arguments) (csmith)
DescriptionBug 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
TagsNo tags attached.
Attached Filestgz file icon slice_missing_arg.tgz [^] (56,651 bytes) 2011-04-11 01:07
? file icon frama_c_journal.ml [^] (3,304 bytes) 2011-04-11 10:26 [Show Content]

- Relationships
related to 0000791closedpascal Cash in value analysis of sliced project 

-  Notes
(0001692)
Anne (reporter)
2011-04-11 09:02

Ok : I'll have a look. The result seems quite strange !
(0001693)
Anne (reporter)
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 (reporter)
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 (reporter)
2011-04-11 10:27

I uploaded the generated journal. Some slicing options have probably not been reset correctly upon completion.
(0001697)
Anne (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
2011-04-11 15:01

The initial problem disappeared ! I don't manage to reproduce it... sorry.
(0001715)
patrick (developer)
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 (manager)
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 (reporter)
2011-04-11 15:50

Ok : thanks ! I'll have a look again.
(0001720)
Anne (reporter)
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 (reporter)
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 (reporter)
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 (manager)
2011-04-14 14:34

Fixed by changeset 12885. Varinfos were created by the slicing in the wrong project.

- Issue History
Date Modified Username Field Change
2011-04-11 01:07 pascal New Issue
2011-04-11 01:07 pascal Status new => assigned
2011-04-11 01:07 pascal Assigned To => Anne
2011-04-11 01:07 pascal File Added: slice_missing_arg.tgz
2011-04-11 09:02 Anne Note Added: 0001692
2011-04-11 09:02 Anne Status assigned => acknowledged
2011-04-11 09:46 Anne Note Added: 0001693
2011-04-11 10:12 pascal Note Added: 0001694
2011-04-11 10:26 monate File Added: frama_c_journal.ml
2011-04-11 10:27 monate Note Added: 0001695
2011-04-11 10:40 Anne Note Added: 0001697
2011-04-11 10:46 Anne Note Added: 0001698
2011-04-11 10:53 pascal Note Added: 0001699
2011-04-11 11:05 Anne Note Added: 0001700
2011-04-11 11:39 svn Checkin
2011-04-11 11:41 Anne Note Added: 0001702
2011-04-11 15:01 Anne Note Added: 0001714
2011-04-11 15:36 patrick Note Added: 0001715
2011-04-11 15:41 patrick Note Edited: 0001715
2011-04-11 15:48 signoles Note Added: 0001717
2011-04-11 15:50 Anne Note Added: 0001719
2011-04-11 16:23 Anne Note Added: 0001720
2011-04-11 17:11 Anne Note Added: 0001721
2011-04-11 17:11 Anne Status acknowledged => assigned
2011-04-11 17:11 Anne Assigned To Anne => virgile
2011-04-11 17:18 Anne Note Added: 0001722
2011-04-14 14:33 yakobowski Relationship added related to 0000791
2011-04-14 14:34 yakobowski Note Added: 0001788
2011-04-14 14:34 yakobowski Status assigned => resolved
2011-04-14 14:34 yakobowski Fixed in Version => Frama-C GIT, precise the release id
2011-04-14 14:34 yakobowski Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version Frama-C GIT, precise the release id => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker