Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002309Frama-CPlug-in > wppublic2017-06-01 16:232017-06-01 16:23
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformPhosphorus-20170501-beta1OSxubuntuOS Version
Product VersionFrama-C 15 Phosphorus 
Target VersionFixed in Version 
Summary0002309: naming the default behavior influences proven obligations
DescriptionRunning "frama-c -wp ilog2_beh.c -wp-prop ilog2 -wp-prover alt-ergo -wp-prover cvc4" on the attached program proves everything except (the lemmas and) loop invariant "a".

However, when lines 16,27,30,36,41 are uncommented, i.e. the default behavior is assigned an explicit name, everything except (the lemmas and) the loop variant is proven instead.

Naming vs. not naming a behavior shouldn't have such an influence.
TagsNo tags attached.
Attached Filesc file icon ilog2_beh.c [^] (1,202 bytes) 2017-06-01 16:23 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2017-06-01 16:23 Jochen New Issue
2017-06-01 16:23 Jochen Status new => assigned
2017-06-01 16:23 Jochen Assigned To => correnson
2017-06-01 16:23 Jochen File Added: ilog2_beh.c


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker