Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002308Frama-CPlug-in > wppublic2017-06-01 13:252017-06-01 13:25
ReporterJochen 
Assigned Tocorrenson 
PrioritylowSeverityfeatureReproducibilityN/A
StatusassignedResolutionopen 
Platformn/aOSn/aOS Version
Product VersionFrama-C 15 Phosphorus 
Target VersionFixed in Version 
Summary0002308: suggest to check (loop) assigns clauses by data flow analysis
DescriptionRunning "frama-c -wp ifft_assigns.c -wp-prop check -wp-prover cvc4" on the attached file proved \false in line 339, which was intentionally inserted as a consistency check at the file's end. The reason for the inconsistency turned out to be a missing variable in a loop assigns clause (commented out for demo purposes in line 237). The detailled argument doesn't matter here; nevertheless it is given in (*) below for convenience.

I guess it would be easy for Frama-C to perform some coarse data-flow analysis and issue a warning about "nu2" being modified in line 295, but missing in the "loop assigns" clauses for the loop in line 242-302. Such an analysis could ignore nontrivial aliases, dead code, and array subranges, thus making it straight-forward to implement.

The example shows the value of warnings that such an analysis is able to issue. Already in this tiny example, it is easy to lose overview (cf. the many experimental "asserts", most of which a probably unncessary, or even nonsensical), and any tool help that doesn't cost much additional computation time is appreciated.

As a further application, it could print suggestions for "assigns" clauses of loops and procedure contracts.

(*): In fact, property "a2" from line 214 implies "nu1!=65536", if the latter variable remained unchanged during the loop in line 242-302, then property "c2" in line 232 boild down to "nu1+l==nu", which is false after the loop since then the termination condition "nu<l" has to hold, and "nu1" is unsigned.
TagsNo tags attached.
Attached Filesc file icon ifft_assigns.c [^] (11,670 bytes) 2017-06-01 13:25 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker