Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002244Frama-CPlug-in > wppublic2016-08-08 22:392016-08-08 22:39
Reporterjrobbins 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Aluminium 
Target VersionFixed in Version 
Summary0002244: Logic with read clauses can have their values invalidated by writes to separated memory locations
DescriptionIn some cases, axiomatic logic using reads clauses can be true for a certain memory location, and then become unknown once an unrelated memory location is assigned to. You can even prove the memory locations as separate, but it does not fix the issue.
Steps To Reproduce== File bug.c:
/*@
axiomatic Axiomatic {
    logic boolean property_of_buffer(char *buffer) reads *buffer;
}
*/

/*@
assigns *buffer;
ensures property_of_buffer(buffer);
*/
void foo(char *buffer);

/*@
requires property_of_buffer(buffer);
assigns *buffer;
ensures property_of_buffer(buffer);
*/
int bar(char *buffer);

char buf1[1];
char buf2[1];

void main() {
    foo(buf1);
    bar(buf1);
    
    foo(buf2);
    bar(buf1);
}
== Command to run:
frama-c -wp bug.c
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_main_call_bar_pre : Valid
[wp] [alt-ergo] Goal typed_main_call_bar_pre_2 : Unknown (562ms)
[wp] Proved goals: 1 / 2
     Qed: 1
     alt-ergo: 0 (unknown: 1)
== Expected behavior: For typed_main_call_bar_pre_2 to prove valid.
Additional InformationThis bug is present on both Frama-C versions Sodium and Aluminum.
TagsNo tags attached.
Attached Filesc file icon bug.c [^] (441 bytes) 2016-08-08 22:39 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2016-08-08 22:39 jrobbins New Issue
2016-08-08 22:39 jrobbins Status new => assigned
2016-08-08 22:39 jrobbins Assigned To => correnson
2016-08-08 22:39 jrobbins File Added: bug.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker