Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002179Frama-CPlug-in > wppublic2015-10-18 17:062015-10-18 19:16
Reporterkroeckx 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002179: Unable to prove things that are provable, gets confused
DescriptionHi,

In the attached file as is using wp -wp-model Typed,cast test-final.c, the last assert can't be proven, resulting in the ensures and assigns to be valid under hypotheses. This is a minimal version that still shows the problem.

However, there are several ways to make it be able to prove it and as far as I can see should have no effect on it. The different ways are:
- Removing any of the following 3 lines:
    p[n] = 0x80; /* there is always room for one */
    HASH_BLOCK_DATA_ORDER(c, p, 1);
    c->num = 0;
- Removing the first assert
- Removing the requires \valid_read(c->data+(0 .. c->num-1));

I assume it gets confused because the \valid_read() overlaps with the \valid(c). It's not really needed. (In the full version the \valid_read() should more be something like \initialized.)
TagsNo tags attached.
Attached Filesc file icon test-final.c [^] (3,576 bytes) 2015-10-18 17:06 [Show Content]

- Relationships

-  Notes
(0006076)
kroeckx (reporter)
2015-10-18 19:16

I think I have several other cases like this, where I can't get any further while I think it should be able to prove it.

- Issue History
Date Modified Username Field Change
2015-10-18 17:06 kroeckx New Issue
2015-10-18 17:06 kroeckx Status new => assigned
2015-10-18 17:06 kroeckx Assigned To => correnson
2015-10-18 17:06 kroeckx File Added: test-final.c
2015-10-18 19:16 kroeckx Note Added: 0006076


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker