2021-03-05 01:23 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002330Frama-CPlug-in > wppublic2017-10-26 12:552020-02-17 18:08
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformPhosphorus-20170501OSOS Versionxubuntu 17.04
Product Version 
Target VersionFixed in VersionFrama-C 20-Calcium 
Summary0002330: known, but inferrable, yet not inferred, property not given as precodition to provers
DescriptionRunning "frama-c -wp foo.c -wp-out wp-out -wp-prop=D" on the attached program fails to prove the property D, although it follows immediately from A and C.
A look at the generated file "foo_assert_D_Alt-Ergo.mlw" reveals that the condition "y<=15" from C is not given to Alt-Ergo, while "0<=y" is.
If the former is inserted into the mlw file, Alt-Ergo proves the goal without problems.
Probably, "y<=15" is considered a trivial consequence of "y==(x&0xf)" by Qed; however, it shouldn't, since (e.g.) Alt-Ergo is unable to to infer this: goal C cannot be proven by Alt-Ergo.
Steps To ReproduceName translation c -> mlw for convenience:

x -> i
y -> x
z -> x_1
TagsNo tags attached.
Attached Files
  • c file icon foo.c (246 bytes) 2017-10-26 12:55 - 
    extern int a[16];

/*@	requires A: \forall integer i; 0 <= i <= 15 ==> 0 <= a[i] <= 9;
	requires B: 0 <= x <= 255;
*/
void foo(int x) {
	int const y = (x & 0xf);
	//@ assert C: 0 <= y <= 15;
	int const z = a[y];
	//@ assert D: 0 <= z <= 9;
	
}
    c file icon foo.c (246 bytes) 2017-10-26 12:55 +

-Relationships
+Relationships

-Notes

~0006909

correnson (manager)

2019-10-17 17:29

 Proved under TIP by using the bit-range tactic and the instance tactic.

~0006945

signoles (manager)

2020-02-17 18:08

 Fixed in Frama-C 20.0 (Calcium).
+Notes

-Issue History
Date Modified Username Field Change
2017-10-26 12:55 Jochen New Issue
2017-10-26 12:55 Jochen Status new => assigned
2017-10-26 12:55 Jochen Assigned To => correnson
2017-10-26 12:55 Jochen File Added: foo.c
2019-10-17 17:29 correnson Note Added: 0006909
2019-10-17 17:30 correnson Status assigned => resolved
2019-10-17 17:30 correnson Resolution open => fixed
2020-02-17 18:06 signoles Fixed in Version => Frama-C 20-Calcium
2020-02-17 18:08 signoles Status resolved => closed
2020-02-17 18:08 signoles Note Added: 0006945
+Issue History