Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000718Frama-CPlug-in > Evapublic2011-02-12 23:432014-02-12 16:59
Reporterregehr 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000718: possible unsoundness in r11866
DescriptionAnalyzing the attached program like this:

  ~/z/frama-c/bin/toplevel.opt -val -slevel 46 foo_pp.c

Gives this assertion:

  *(int*)&g_23 == -10

However, running the program gives value "-9" instead.
TagsNo tags attached.
Attached Filesc file icon foo_pp.c [^] (41,763 bytes) 2011-02-12 23:43 [Show Content]

- Relationships

-  Notes
(0001483)
pascal (reporter)
2011-02-13 00:14
edited on: 2011-02-13 00:16

The proper message (including the word "assert") is missing from the output, but the value analysis has found that g_23 could be 9 at some point, and has then cut that branch because it lead to guaranteed undefined behavior:


[value] computing for function func_42 <-func_1 <-main.
        Called from foo.c:71.
[value] Recording results for func_42
foo.c:140:[value] warning: local escaping the scope of func_42 through \result
[value] Done for function func_42
foo.c:71:[kernel] warning: completely undefined value in {{
                  tmp_9 -> {0; } ;}} (size:<32>).
[value] Recording results for func_1
[value] Done for function func_1

func_42 returns the address of a local variable:

int32_t ** func_42(int8_t p_43, uint32_t p_44, int32_t ** p_45, uint32_t p_46)
{
     const int64_t l_61 = 0xB4954824FF24264ALL;
    int32_t *l_64 = &g_30;
    int8_t l_120 = 0xE3L;
    uint64_t l_121 = -2L;
    uint8_t l_122 = 1L;
    int32_t **l_123 = &l_64;
    (**g_21) |= l_120;
    return l_123;
}

The address, that it is illegal to use, returned by the first call is passed as an argument on the second call to func_42. This is when the value analysis warns as above and stops propagation. We can argue about the precise place the warning should be (we do not want to stop propagation when a global has contained the address of a local but is no longer accessed after the function returns), but this program contains an undefined behavior.
I will add an explicit message with the word "assert" for the case where the variable with undefined contents is passed as an argument to another function.

(0001484)
pascal (reporter)
2011-02-13 01:14

This example now emits the warning:
foo.c:71:[kernel] warning: accessing left-value tmp_9 that contains escaping addresses; assert(Ook)

I believe this is the path that is followed by the real execution. Removing the "volatile"s would probably confirm this.
(0001486)
regehr (reporter)
2011-02-13 05:29

n1124 says: "If an object is referred to outside of its lifetime, the behavior is undefined. The value of a pointer becomes indeterminate when the object it points to reaches the end of its lifetime."

Permitting a pointer to escape doesn't constitute "referring to", which would require a dereference operation. Therefore our reading is that it's OK to permit pointers to escape as long as they are not subsequently used, and we deliberately coded Csmith to generate programs that do this.
(0001487)
regehr (reporter)
2011-02-13 05:30

Hmm, I was going to re-close this issue after making the previous comment, but I can't seem to -- perhaps only maintainers have privileges to do that?

Anyway my intent wasn't to try to keep this bug alive, but rather to add the note about our reading of the C99 standard.
(0001489)
pascal (reporter)
2011-02-13 07:13

"indeterminate" is also defined as "either an unspecified value or a trap representation".

J.2. defines a case of undefined behavior as "A trap representation is read by an lvalue expression that does not have character type (6.2.6.1).".

The words "trap representation" are more or less defined by example in 6.2.6.1.5.

This said, I thought you were going to argue for having the warning sooner, not later. The alarm had been forgotten because warning for a completely undefined lvalue as argument for a function was a separate feature. The value analysis avoids warning for partially undefined lvalues because structs (which can be passed as arguments) always contain undefined padding or fields that it does not make sense to initialize in some cases. The "warn for completely undefined argument" requirement was expressed by a user; we implemented it without an option to select the behavior, and no-one until now complained that they wanted to pass dangling pointers as parameters to functions without warning. Architecturally, it would be very easy to wait until the program does pointer arithmetic on (or of course dereferences) the dangling pointer to emit the alarm. We are emitting it early as a favor.
(0004834)
pascal (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-02-12 23:43 regehr New Issue
2011-02-12 23:43 regehr Status new => assigned
2011-02-12 23:43 regehr Assigned To => pascal
2011-02-12 23:43 regehr File Added: foo_pp.c
2011-02-13 00:14 pascal Note Added: 0001483
2011-02-13 00:16 pascal Note Edited: 0001483
2011-02-13 01:14 pascal Note Added: 0001484
2011-02-13 01:15 svn Checkin
2011-02-13 01:15 svn Status assigned => resolved
2011-02-13 01:15 svn Resolution open => fixed
2011-02-13 05:29 regehr Note Added: 0001486
2011-02-13 05:29 regehr Status resolved => feedback
2011-02-13 05:29 regehr Resolution fixed => reopened
2011-02-13 05:30 regehr Note Added: 0001487
2011-02-13 07:13 pascal Note Added: 0001489
2011-02-13 07:13 pascal Status feedback => resolved
2011-02-13 07:13 pascal Resolution reopened => 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 pascal Note Added: 0004834
2014-02-12 16:59 pascal Status closed => resolved
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker